How can I prove $(\lnot A \rightarrow A) \rightarrow A$?

105 Views Asked by At

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:

  1. $\lnot A \rightarrow \lnot A$ (proved lemma)
  2. $(\lnot A \rightarrow \lnot A) \rightarrow ((\lnot A \rightarrow \lnot \lnot A) \rightarrow \lnot \lnot A$ (axiom 7)
  3. $(\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?