Tell me more ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.
up vote 7 down vote favorite

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?

share|improve this question
5  
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

2 Answers

up vote 2 down vote accepted

  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.

share|improve this answer
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
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$. – Zhen Lin May 7 '12 at 17:05
up vote 0 down vote

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
share|improve this answer
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

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.