How do I prove $x \vee \neg x$ in Hilbert system? How to prove $x \vee \neg x$ using the following axioms?  


*

*$A \rightarrow (B \rightarrow A)$   

*$(A \rightarrow (B \rightarrow
    C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$

*$(A \wedge B) \rightarrow A$

*$(A \wedge B) \rightarrow B$

*$(A \rightarrow B) \rightarrow ((A \rightarrow C) \rightarrow (A \rightarrow B \wedge C))$

*$A \rightarrow A \vee B$

*$B \rightarrow A \vee B$

*$(A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow (A \vee B \rightarrow C))$

*$A \rightarrow \neg \neg A$

*$\neg \neg A \rightarrow A$

*$(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$


What I'm thinking is that using 6 or 7, I'd first have to prove $x$, which is not a tautology and using 8, I could prove $x \vee \neg x \rightarrow C$ but no matter what I put instead of $C$, I won't be able to reverse the arrow. Can some statement be impossible to prove? Is it a bad set of axioms that I'm using?
 A: *

*Prove $\lnot (x \land \lnot x)$. This is easy in natural deduction but in a Hilbert system somewhat more effort is required. (Or, cheat and use the deduction theorem.) You will not need to use double negation elimination here.

*Prove de Morgan's law in the form $\lnot (p \land q)$ implies $\lnot p \lor \lnot q$.

*Put the above two steps together to get $\lnot x \lor \lnot \lnot x$, then apply double negation elimination.
A: I would like to give a new proof, I hope a little bit "more readable".
I refer to Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997).
The 11-axioms OP's axiom sytem is like the 10-axioms system $\mathsf L_4$ discussed in Mendelson [page 46], derived from Kleene  [1952 - Introduction to Metamathematics] with a "variant" in Ax5, and Ax9 and Ax11 in place of the Kleene's 10th axiom : $\vdash (B \rightarrow C) \rightarrow ((B \rightarrow \lnot C) \rightarrow \lnot C)$.
Ax1 and Ax2 are also used in Mendelson [as (A1) and (A2)].

Lemma 0 : $\vdash A \rightarrow A$ [Self-Imp - see Mendelson : Lemma 1.8, page 36]

(1) $\vdash [A \rightarrow ((B \rightarrow A) \rightarrow A)] \rightarrow [(A \rightarrow (B \rightarrow A)) \rightarrow (A \rightarrow A)]$ --- Ax2
(2) $\vdash A \rightarrow ((B \rightarrow A) \rightarrow A)$ --- Ax1 
(3) $\vdash (A \rightarrow (B \rightarrow A)) \rightarrow (A \rightarrow A)$ --- from (1) and (2) by modus ponens
(4) $\vdash A \rightarrow (B \rightarrow A)$ --- Ax1
(5) $\vdash A \rightarrow A$ --- from (3) and (4) by modus ponens.
With Ax1, Ax2 and Lemma 0, we may prove the Deduction Theorem [see Mendelson : Prop 1.9, page 37].

Lemma 1 : $A \rightarrow B, B \rightarrow C \vdash A \rightarrow C$ [Syllogism - see Mendelson : Coroll 1.10a, page 38]

(1) $A \rightarrow B$ --- assumed
(2) $B \rightarrow C$ --- assumed
(3) $\vdash (B \rightarrow C) \rightarrow (A \rightarrow (B \rightarrow C))$ --- Ax1
(4) $A \rightarrow (B \rightarrow C)$ --- from (2) and (3) by modus ponens
(5) $\vdash [A \rightarrow (B \rightarrow C)] \rightarrow [(A \rightarrow B) \rightarrow (A \rightarrow C)]$ --- Ax2
(6) $(A \rightarrow B) \rightarrow (A \rightarrow C)$ --- from (4) and (5) by modus ponens
(7) $A \rightarrow C$ --- from (1) and (6) by modus ponens.

Lemma 2 : $\vdash (\lnot A \rightarrow \lnot B) \rightarrow (B \rightarrow A)$ [Transposition]

(1) $\vdash (\lnot A \rightarrow \lnot B) \rightarrow (\lnot \lnot B \rightarrow \lnot \lnot A)$ --- Ax11
(2) $\lnot A \rightarrow \lnot B$ --- assumed
(3) $\lnot \lnot B \rightarrow \lnot \lnot A$ --- from (1) and (2) by modus ponens
(4) $\vdash B \rightarrow \lnot \lnot B$ --- Ax9
(5) $B \rightarrow \lnot \lnot A$ --- from (3) and (4) by Syll
(6) $\vdash \lnot \lnot A \rightarrow A$ --- Ax10
(7) $B \rightarrow A$ --- from (5) and (6) by Syll
(8) $\vdash (\lnot A \rightarrow \lnot B) \rightarrow (B \rightarrow A)$ --- by Deduction Theorem, discharging (2).

Lemma 3 : $\vdash \lnot A \rightarrow (A \rightarrow B)$

(1) $\vdash \lnot A \rightarrow (\lnot B \rightarrow \lnot A)$ --- Ax1
(2) $\vdash (\lnot B \rightarrow \lnot A) \rightarrow (A \rightarrow B)$ --- Lemma 2
(3) $\vdash \lnot A \rightarrow (A \rightarrow B)$ --- from (1) and (2) by Syll.

Lemma 4 : $\vdash (\lnot A \rightarrow A) \rightarrow (B \rightarrow A)$

(1) $\vdash \lnot A \rightarrow (A \rightarrow \lnot B)$ --- Lemma 3
(2) $\vdash [\lnot A \rightarrow (A \rightarrow \lnot B)] \rightarrow [(\lnot A \rightarrow A) \rightarrow (\lnot A \rightarrow \lnot B)]$ --- Ax2
(3) $\vdash (\lnot A \rightarrow A) \rightarrow (\lnot A \rightarrow \lnot B)$ --- from (1) and (2) by modus ponens
(4) $\vdash (\lnot A \rightarrow \lnot B) \rightarrow (B \rightarrow A)$ --- Lemma 2
(5) $\vdash (\lnot A \rightarrow A) \rightarrow (B \rightarrow A)$ --- from (3) and (4) by Syll.

Lemma 5 : $\vdash (\lnot A \rightarrow A) \rightarrow A$

(1) $\vdash (\lnot A \rightarrow A) \rightarrow ((\lnot A \rightarrow A) \rightarrow A)$ --- Lemma 4
(2) $\vdash [(\lnot A \rightarrow A) \rightarrow ((\lnot A \rightarrow A) \rightarrow A)] \rightarrow [ ((\lnot A \rightarrow A) \rightarrow (\lnot A \rightarrow A)) \rightarrow ((\lnot A \rightarrow A) \rightarrow A) ]$ --- Ax2
(3) $\vdash ((\lnot A \rightarrow A) \rightarrow (\lnot A \rightarrow A)) \rightarrow ((\lnot A \rightarrow A) \rightarrow A)$ --- from (1) and (2) by modus ponens
(4) $\vdash (\lnot A \rightarrow A) \rightarrow (\lnot A \rightarrow A)$ --- Lemma 0 
(5) $\vdash (\lnot A \rightarrow A) \rightarrow A$ --- from (3) and (4) by modus ponens.

Lemma 6 : $A \rightarrow B, \lnot A \rightarrow B \vdash B$

(1) $A \rightarrow B$ --- assumed
(2) $\vdash (A \rightarrow B) \rightarrow (\lnot B \rightarrow \lnot A)$ --- Ax11
(3) $\lnot B \rightarrow \lnot A$ --- from (1) and (2) by modus ponens
(4) $\lnot A \rightarrow B$ --- assumed
(5) $\lnot B \rightarrow B$ --- from (3) and (4) by Syll
(6) $\vdash (\lnot B \rightarrow B) \rightarrow B$ --- Lemma 5
(7) $B$ --- from (5) and (6) by modus ponens.
Finally, we have our main result :


Theorem [Excluded Middle] : $\vdash A \lor \lnot A$


(1) $\vdash A \rightarrow (A \lor \lnot A)$ --- Ax6
(2) $\vdash \lnot A \rightarrow (A \lor \lnot A)$ --- Ax7

(3) $\vdash A \lor \lnot A$ --- from (1) and (2) by Lemma 6.


Notes
(A) We have used the Deduction Theorem only in the proof of Lemma 2; with a little additional effort we may avoid it at all.
(B) We have used only Ax1, Ax2, Ax6, Ax7, Ax9, Ax10, Ax11.
A: Lemma 1: $(P \rightarrow Q) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q))$


*

*$(R \rightarrow (P \rightarrow Q)) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q))$  Axiom 2

*$((R \rightarrow (P \rightarrow Q))\rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q))) \rightarrow ((P \rightarrow Q) \rightarrow ((R \rightarrow (P \rightarrow Q)) \rightarrow ((R \rightarrow P) \rightarrow (R\rightarrow Q))))$  Axiom 1

*$(P \rightarrow Q) \rightarrow ((R \rightarrow (P \rightarrow Q)) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q)))$  1,2 MP

*$((P \rightarrow Q) \rightarrow ((R \rightarrow (P \rightarrow Q)) \rightarrow ((R \rightarrow P) \rightarrow (R\rightarrow Q))))\rightarrow (((P \rightarrow Q) \rightarrow (R \rightarrow (P \rightarrow Q))) \rightarrow ((P \rightarrow Q) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q))))$  Axiom 2

*$((P \rightarrow Q) \rightarrow (R \rightarrow (P \rightarrow Q))) \rightarrow ((P \rightarrow Q) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q)))$  3,4 MP

*$(P \rightarrow Q) \rightarrow (R \rightarrow (P \rightarrow Q))$  Axiom 1

*$(P \rightarrow Q) \rightarrow ((R\rightarrow P) \rightarrow (R \rightarrow Q))$  5,6 MP


Lemma 2: $(P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q)$


*

*$((P \rightarrow (P \rightarrow Q)) \rightarrow ((P \rightarrow P) \rightarrow (P \rightarrow Q))) \rightarrow (((P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow P)) \rightarrow ((P\rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q)))$  Axiom 2

*$(P \rightarrow (P \rightarrow Q)) \rightarrow ((P \rightarrow P) \rightarrow (P \rightarrow Q))$  Axiom 2

*$((P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow P)) \rightarrow ((P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q))$  1,2 MP

*$P \rightarrow ((P \rightarrow P) \rightarrow P)$  Axiom 1

*$(P \rightarrow ((P \rightarrow P) \rightarrow P)) \rightarrow ((P \rightarrow (P \rightarrow P)) \rightarrow(P \rightarrow P))$  Axiom 2

*$(P \rightarrow (P \rightarrow P)) \rightarrow (P \rightarrow P)$  4,5 MP

*$P \rightarrow (P \rightarrow P)$  Axiom 1

*$P \rightarrow P$  6,7 MP

*$(P \rightarrow P) \rightarrow ((P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow P))$  Axiom 1

*$(P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow P)$  8,9 MP

*$(P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q)$  3,10 MP


Lemma 3: $P \rightarrow ((P \rightarrow Q) \rightarrow Q)$


*

*$(P \rightarrow Q) \rightarrow (((P \rightarrow Q) \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q))$  Axiom 1

*$((P \rightarrow Q) \rightarrow (((P\rightarrow Q) \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q))) \rightarrow (((P \rightarrow Q) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow Q))) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow Q)))$  Axiom 2

*$((P \rightarrow Q) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow Q))) \rightarrow ((P\rightarrow Q)\rightarrow (P \rightarrow Q))$  1,2 MP

*$(P\rightarrow Q) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow Q))$  Axiom 1

*$(P \rightarrow Q) \rightarrow (P \rightarrow Q)$  3,4 MP

*$((P \rightarrow Q) \rightarrow (P \rightarrow Q)) \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P\rightarrow Q) \rightarrow Q))$  Axiom 2

*$((P\rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)$  5,6 MP

*$P \rightarrow ((P\rightarrow Q) \rightarrow P)$  Axiom 1

*$((P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) > Q))) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))) \rightarrow ((((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q))) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))))$  Axiom 1

*$(P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q))) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))$  Axiom 2

*$(((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q))) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q))))$  9,10 MP

*$((((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P\rightarrow Q) \rightarrow Q))) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q))))) \rightarrow (((((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow (P \rightarrow (((P\rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)))) \rightarrow ((((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))))$  Axiom 2

*$((((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow (P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)))) \rightarrow ((((P \rightarrow Q) \rightarrow P) > ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q))))$  11,12 MP

*$(((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow (P \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)))$  Axiom 1

*$(((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)) \rightarrow ((P \rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))$  13,14 MP

*$(P\rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q))$  7,15 MP

*$P \rightarrow ((P \rightarrow Q) \rightarrow Q)$  8,16 MP


Main Theorem: $P \vee \neg P$


*

*$P \rightarrow (P \vee \neg P)$  Axiom 6

*$(P \rightarrow (P \vee \neg P)) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg P)$  Axiom 11

*$\neg (P \vee \neg P) \rightarrow \neg P$  1,2 MP

*$\neg P \rightarrow (P \vee \neg P)$  Axiom 7

*$(\neg P \rightarrow (P \vee \neg P)) \rightarrow ((\neg (P \vee \neg P) \rightarrow \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))$  Lemma 1

*$(\neg (P \vee \neg P) \rightarrow \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))$  4,5 MP

*$\neg (P \vee \neg P) \rightarrow (P \vee \neg P)$  3,6 MP

*$\neg (P \vee \neg P) \rightarrow ((\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow (P \vee \neg P))$  Lemma 3

*$((\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow (P \vee \neg P)) \rightarrow (\neg (P \vee  \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))$  Axiom 11

*$(((\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow (P \vee \neg P)) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))) \rightarrow ((\neg (P \vee \neg P) \rightarrow ((\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow (P \vee \neg P))) \rightarrow (\neg (P \vee \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))))$  Lemma 1

*$(~(P \vee \neg P) \rightarrow ((\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow (P \vee \neg P))) \rightarrow (\neg (P \vee \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))))$  9,10 MP

*$\neg (P \vee \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))$  8,11 MP

*$(\neg (P \vee \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P)))$  Lemma 2

*$~(P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))$  12,13 MP

*$(\neg (P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))) \rightarrow (\neg\neg(\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow \neg \neg(P \vee \neg P)) $ Axiom 11

*$\neg\neg(\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow \neg\neg(P \vee \neg P)$  14,15 MP

*$(\neg (P \vee\neg P) \rightarrow (P \vee \neg P)) \rightarrow \neg\neg (\neg(P \vee \neg P) \rightarrow (P \vee \neg P))$  Axiom 9

*$\neg \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))$  7,17 MP

*$\neg\neg (P \vee \neg P)$  16,18 MP

*$\neg\neg (P \vee \neg P) \rightarrow (P \vee \neg P)$  Axiom 10

*$P \vee \neg P$  19,20 MP

