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.

  • 2
    $\begingroup$ "Avoid using the deduction theorem" for a Hilbert-style calculus is a recipe for absolute misery. Why would you want that? $\endgroup$ – hmakholm left over Monica Aug 1 '18 at 10:03
  • $\begingroup$ @HenningMakholm Frege, Lukasiewicz, Russell, Hilbert, and others, as well plenty of theorem-provers avoid using the deduction theorem. $\endgroup$ – Doug Spoonwood Aug 1 '18 at 10:46


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


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)

| cite | improve this answer | |

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}

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.