How do I prove $x \vee \neg x$ in Hilbert system?

1. 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.

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

3. Put the above two steps together to get $\lnot x \lor \lnot \lnot x$, then apply double negation elimination.

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.

Lemma 1: $(P \rightarrow Q) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q))$

1. $(R \rightarrow (P \rightarrow Q)) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q))$ Axiom 2
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
3. $(P \rightarrow Q) \rightarrow ((R \rightarrow (P \rightarrow Q)) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q)))$ 1,2 MP
4. $((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
5. $((P \rightarrow Q) \rightarrow (R \rightarrow (P \rightarrow Q))) \rightarrow ((P \rightarrow Q) \rightarrow ((R \rightarrow P) \rightarrow (R \rightarrow Q)))$ 3,4 MP
6. $(P \rightarrow Q) \rightarrow (R \rightarrow (P \rightarrow Q))$ Axiom 1
7. $(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)$

1. $((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
2. $(P \rightarrow (P \rightarrow Q)) \rightarrow ((P \rightarrow P) \rightarrow (P \rightarrow Q))$ Axiom 2
3. $((P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow P)) \rightarrow ((P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q))$ 1,2 MP
4. $P \rightarrow ((P \rightarrow P) \rightarrow P)$ Axiom 1
5. $(P \rightarrow ((P \rightarrow P) \rightarrow P)) \rightarrow ((P \rightarrow (P \rightarrow P)) \rightarrow(P \rightarrow P))$ Axiom 2
6. $(P \rightarrow (P \rightarrow P)) \rightarrow (P \rightarrow P)$ 4,5 MP
7. $P \rightarrow (P \rightarrow P)$ Axiom 1
8. $P \rightarrow P$ 6,7 MP
9. $(P \rightarrow P) \rightarrow ((P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow P))$ Axiom 1
10. $(P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow P)$ 8,9 MP
11. $(P \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q)$ 3,10 MP

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

1. $(P \rightarrow Q) \rightarrow (((P \rightarrow Q) \rightarrow (P \rightarrow Q)) \rightarrow (P \rightarrow Q))$ Axiom 1
2. $((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
3. $((P \rightarrow Q) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow Q))) \rightarrow ((P\rightarrow Q)\rightarrow (P \rightarrow Q))$ 1,2 MP
4. $(P\rightarrow Q) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow Q))$ Axiom 1
5. $(P \rightarrow Q) \rightarrow (P \rightarrow Q)$ 3,4 MP
6. $((P \rightarrow Q) \rightarrow (P \rightarrow Q)) \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P\rightarrow Q) \rightarrow Q))$ Axiom 2
7. $((P\rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)$ 5,6 MP
8. $P \rightarrow ((P\rightarrow Q) \rightarrow P)$ Axiom 1
9. $((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
10. $(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
11. $(((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
12. $((((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
13. $((((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
14. $(((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
15. $(((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
16. $(P\rightarrow ((P \rightarrow Q) \rightarrow P)) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q))$ 7,15 MP
17. $P \rightarrow ((P \rightarrow Q) \rightarrow Q)$ 8,16 MP

Main Theorem: $P \vee \neg P$

1. $P \rightarrow (P \vee \neg P)$ Axiom 6
2. $(P \rightarrow (P \vee \neg P)) \rightarrow (\neg (P \vee \neg P) \rightarrow \neg P)$ Axiom 11
3. $\neg (P \vee \neg P) \rightarrow \neg P$ 1,2 MP
4. $\neg P \rightarrow (P \vee \neg P)$ Axiom 7
5. $(\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
6. $(\neg (P \vee \neg P) \rightarrow \neg P) \rightarrow (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))$ 4,5 MP
7. $\neg (P \vee \neg P) \rightarrow (P \vee \neg P)$ 3,6 MP
8. $\neg (P \vee \neg P) \rightarrow ((\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow (P \vee \neg P))$ Lemma 3
9. $((\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
10. $(((\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
11. $(~(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
12. $\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
13. $(\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
14. $~(P \vee \neg P) \rightarrow \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))$ 12,13 MP
15. $(\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
16. $\neg\neg(\neg (P \vee \neg P) \rightarrow (P \vee \neg P)) \rightarrow \neg\neg(P \vee \neg P)$ 14,15 MP
17. $(\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
18. $\neg \neg (\neg (P \vee \neg P) \rightarrow (P \vee \neg P))$ 7,17 MP
19. $\neg\neg (P \vee \neg P)$ 16,18 MP
20. $\neg\neg (P \vee \neg P) \rightarrow (P \vee \neg P)$ Axiom 10
21. $P \vee \neg P$ 19,20 MP