my axioms are (from Kleene):
1a $A \rightarrow (B \rightarrow A)$
1b $(A \rightarrow B) \rightarrow ((A \rightarrow (B \rightarrow C)) \rightarrow (A \rightarrow C))$
3 $A \rightarrow (B \rightarrow A \land B)$
4a $A \land B \rightarrow A$
4b $A \land B \rightarrow B$
5a $A \rightarrow A \lor B$
5b $B \rightarrow A \lor B$
6 $(A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow (A \lor B \rightarrow C))$
7 $(A \rightarrow B) \rightarrow ((A \rightarrow \lnot B) \rightarrow \lnot A)$
8 $\lnot \lnot A \rightarrow A$
9a $(A \rightarrow B) \rightarrow ((B \rightarrow A) \rightarrow (A \leftrightarrow B))$
10a $(A \leftrightarrow B) \rightarrow (A \rightarrow B)$
10b $(A \leftrightarrow B) \rightarrow (B \rightarrow A)$
I found this exercise in Mendelson: $$(\lnot A \rightarrow A) \rightarrow A$$
I tried to prove it this way:
- $\lnot A \rightarrow \lnot A$ (proved lemma)
- $(\lnot A \rightarrow \lnot A) \rightarrow ((\lnot A \rightarrow \lnot \lnot A) \rightarrow \lnot \lnot A$ (axiom 7)
- $(\lnot A \rightarrow \lnot \lnot A) \rightarrow \lnot \lnot A$ (modus ponens 1, 2)
I think that I could somehow use axiom number 8. Can you help, please?