# 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 (B \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