11
$\begingroup$

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?

  • 6
    You absolutely have to use (10), because everything else is valid intuitionistically but your goal formula is not.2012-05-07

3 Answers 3

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

  • 1
    @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$.2012-05-07
2

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.

1

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
  • 0
    @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.2014-03-28