Prove the following theorem in propositional calculus

Question

I have the following Hilbert-style propositional calculus, having the logical connectives $\{\neg,\rightarrow\}$ of arity one and two respectively, and the following axioms:

A1: $A\rightarrow(B\rightarrow A)$

A2: $(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))$

A3: $(\neg A\rightarrow \neg B)\rightarrow (B\rightarrow A).$

$A,B,C$ are any well-formed formulas (wffs). The only inference rule is modus ponens. I want to prove the following theorem:

$\vdash (\neg A\rightarrow A)\rightarrow A$ for any wff $A$.

You may use any or all of the following theorems without proof:

$\vdash A\rightarrow A$ for any wff $A$.

$A\rightarrow B, B\rightarrow C\vdash A\rightarrow C$ for any wffs $A,B,C$.

$A\rightarrow (B\rightarrow C), B\vdash A\rightarrow C$ for any wffs $A,B,C$.

$\vdash \neg A\rightarrow (A\rightarrow B)$ for any wffs $A,B$.

Please avoid using the deduction theorem unless absolutely necessary.

Answer 1

Lemma

1) $\vdash \lnot A \to (A \to B)$ --- Th.4

2) $\vdash (\lnot A \to (A \to B)) \to ((\lnot A \to A) \to (\lnot A \to \lnot B))$ --- Ax.2

3) $\vdash (\lnot A \to A) \to (\lnot A \to \lnot B)$ --- from 1) and 2)

4) $\vdash (\lnot A \to \lnot B) \to (B \to A)$ --- Ax.3

5) $\vdash (\lnot A \to A) \to (B \to A)$ --- from 3) and 4) by Th.2

Proof

1) $\vdash (\lnot A \to A) \to ((\lnot A \to A) \to A)$ --- from Lemma

2) $\vdash ((\lnot A \to A) \to ((\lnot A \to A) \to A)) \to (((\lnot A \to A) \to (\lnot A \to A)) \to ((\lnot A \to A) \to A))$ --- Ax.2

3) $\vdash ((\lnot A \to A) \to (\lnot A \to A)) \to ((\lnot A \to A) \to A)$ --- from 1) and 2)

4) $\vdash (\lnot A \to A) \to (\lnot A \to A)$ --- from Th.1

5) $\vdash (\lnot A \to A) \to A$ --- from 3) and 4)

Answer 2

I use Polish notation. Thus, instead I'll translate every wff of the form $\lnot$$\alpha$ into the form N$\alpha$. Also, I'll translate every wff of the form ($\alpha$$\rightarrow$$\beta$) into the form C$\alpha$$\beta$. Thus, the axioms can get translated to

A1 CxCyx

A2 CCxCyzCCxyCxz

A3 CCNxNyCxy

I'll also use spacing to help to indicate where a substitution of an axiom or previously proved theorem took place.

1 CxCyx

2 CCxCyzCCxyCxz

3 CCNxNyCyx

4 C CxCyx C z CxCyx from 1

5 CzCxCyx from {4, 1}

6 CC CxCyz C Cxy Cxz CC CxCyz Cxy C CxCyz Cxz from 2

7 CCCxCyzCxyCCxCyzCxz from {6, 2}

8 C CCNxNyCyx C z CCNxNyCyx from 1

9 CzCCNxNyCyx from {8, 3}

10 C CxCCyxz C x C y x from 5

11 CCC x C Cyx z C x Cyx CC x C Cyx z C x z from 7

12 CCxCCyxzCxz from {11, 10}

13 CC z C CNxNy Cyx CC z CNxNy C z Cyx from 2

14 CCzCNxNyCzCyx from {13, 9}

15 CC Nz CC Ny Nz Czy C Nz Czy from 12

16 C Nz CC Ny Nz C z y from 9

17 CNzCzy from {15, 16}

18 CC Nz C z y CC Nz z C Nz y from 2

19 CCNzzCNzy from {18, 17}

20 CC CNzz CN z N y C CNzz C y z from 14

21 CCN z z CN z Ny from 19

22 CCNzzCyz from {20, 21}

23 CC CNxx CC y CNxx x C CNxx x from 12

24 CCN x x C CyCNxx x from 22

25 CCNxxx from {23, 24}