I have to prove the following statement : (A -> B) <-> ~A \/ B which is the decomposition of implication. I can use the ~~A -> A axiom as it is given in the exercise, but I'm stuck pretty early in the demonstration.
I start by splitting then introducing, then I've tried a bit of everything (right, left, apply the absurd axiom then introducing) but nothing looks convincing and I don't really know where to go from there...
Any suggestions ?
From the axiom forall A, ~~A -> A that you were given, you can prove the law of the excluded middle, forall A, A \/ ~A. They are actually logically equivalent.
If you do that, then it is easy for you to solve your assignment.
I don't give the full solution here because it is not good to give solutions to course exercises, and I promise you will learn from doing it.
But as a small hint, when trying to prove
Goal (forall A, ~ ~ A -> A) -> (forall A, A \/ ~ A).
the first steps are intros H A. apply H. intros C.