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

How to prove $x \vee \neg x$ using the following axioms?

1. $A \rightarrow (B \rightarrow A)$
2. $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$
3. $(A \wedge B) \rightarrow A$
4. $(A \wedge B) \rightarrow B$
5. $(A \rightarrow B) \rightarrow ((A \rightarrow C) \rightarrow (A \rightarrow B \wedge C))$
6. $A \rightarrow A \vee B$
7. $B \rightarrow A \vee B$
8. $(A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow (A \vee B \rightarrow C))$
9. $A \rightarrow \neg \neg A$
10. $\neg \neg A \rightarrow A$
11. $(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?

-
You absolutely have to use (10), because everything else is valid intuitionistically but your goal formula is not. –  Zhen Lin May 7 '12 at 14:12

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 think I can do 2, but I don't see 1 at all. Could you give a hint? Thanks. –  Karolis Juodelė May 7 '12 at 16:11
@KarolisJuodelė: What you should prove is $(p \land (p \to q)) \to q$, and if you're willing to use the deduction theorem, it's the same as showing $p \land (p \to q)$ implies $q$. –  Zhen Lin May 7 '12 at 17:05

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
-
Lemma 2, 1. seems wrong: You seem to state $(A\rightarrow (B\rightarrow C))\rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow C))$ –  Julian Kuelshammer Oct 19 '12 at 22:05
Ow! My eyes hurt! –  Douglas S. Stones Oct 20 '12 at 2:55
I don't buy sub-lemma 12 of Lemma 3. I don't know the algorithm here to parse it also. At certain parts also ">" appears instead of →. That said, the author clearly put in a significant amount of work here (if it's a human or human generated proof, and not a program/human rewriting a machine-generated proof... "Axiomatica" hasn't written anything else on this site). Also, the author here seems to lack the knowledge that everything that gets proved axiomatically qualifies as a schema (or "equivalently" the rule of uniform substitution can get applied on every well-formed formula). –  Doug Spoonwood Aug 21 '13 at 2:16
I say that, because (p→p) gets proved. But then later in lemma 3 there exist sub-lemmas to prove ((p→q)→(p→q)). So, I guess the author doesn't realize that everything that gets proved axiomatically in a propositional calculus within the object logic qualifies as a schema... or at least can get thought of as a schema. –  Doug Spoonwood Aug 21 '13 at 2:19
@JulianKuelshammer - you are right, but the Ax2 used by Axiomatica is the right one : $\vdash (A→(B→C))→((A→B)→(A→C))$. The formula of the OP's question, i.e. $(A→(B→C))→((A→B)→(B→C))$, is wrong : it is not a tautology; I've corrected it. –  Mauro ALLEGRANZA Mar 28 '14 at 15:22

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.

-