It's been days that I'm stuck in a simple proof of $(P \to \neg P) \to \neg P$ using an axiomatic system, and, whenever I think I'm closer to it, I just found I'm walking in circles.

The system goes as follow:

  • Ax1: $(\varphi_1 \to (\varphi_2 \to \varphi_3)) \to ((\varphi_1 \to \varphi_2)\to(\varphi_1 \to \varphi_3))$
  • Ax2: $\varphi_1 \to (\varphi_2 \to \varphi_1)$
  • Ax3: $\varphi_1 \to ((\neg \varphi_1) \to \varphi_2)$
  • Ax4: $((\neg \varphi_1) \to \varphi_1) \to \varphi_1$
  • Ax5: $(\neg \varphi_1) \to (\varphi_1 \to \varphi_2)$
  • Ax6: $\varphi_1 \to ((\neg \varphi_2) \to (\neg (\varphi_1 \to \varphi_2)))$

  • Rules: Modus Ponens (Deduction theorem is also acceptable).

  • Language: $\neg$ and $\to$ as primitives.

Is it provable at all?

Any help will be highly appreciated.

  • $\begingroup$ These axioms are not independent (well... actually I mean what I believe are the intended axioms, since there are no well-formed formulas above). Axiom 5 (or axiom 3) follows from axioms 1, 2, and 3 (or 5 respectively). Additionally, axiom 6 can get derived from axioms 1, 2, 3, and 4, or from axioms 1, 2, 4, and 5. $\endgroup$ – Doug Spoonwood Sep 23 '15 at 0:32
  • $\begingroup$ @DougSpoonwood I never claimed they were independent. :) $\endgroup$ – StudentType Oct 3 '15 at 14:35
  • $\begingroup$ Indeed, you didn't. That said, that such axioms are not independent, I think, still worthy of mentioning. $\endgroup$ – Doug Spoonwood Oct 3 '15 at 19:25

We wish to prove the following: $$\vdash (P \to \neg P) \to \neg P$$

Notice how similar this is to your Axiom 4 - we just need to replace all instances of $P$ with $\neg P$ and then $\neg \neg P$ with $P$. This gives us a clue about where to start. If your language doesn't define $\neg P$ as $P \to \bot$ (or if it doesn't even have a symbol for $\bot$) then you can just skip Lemma 1.

Lemma 1: $P \to \neg \neg P$.
Proof: Axiom 3 states that $P \to ((\neg P) \to \bot)$, which is longhand for $P \to \neg \neg P$.

Lemma 2: $\neg \neg P \to P$.
Proof: by deduction theorem, we may assume $\neg \neg P$ and try to prove $P$. Axiom 5 gives $\neg \neg P \to (\neg P \to Q)$; modus ponens gives $\neg P \to Q$. Axiom 4 gives $(\neg P \to P) \to P$, so letting $Q = P$ and modus ponens gives $P$, as required.

That is, we have shown that $\neg \neg P$ is equivalent to $P$.

Therefore, a proof of $(P \to \neg P) \vdash \neg P$ (which is equivalent by the deduction theorem) is as follows:

  1. $(\neg \neg P \to \neg P) \to \neg P$ (Axiom 4)
  2. $P \to \neg P$ (hypothesis)
  3. $\neg \neg P \to P$ (lemma 2)
  4. $(P \to \neg P) \to (\neg \neg P \to (P \to \neg P)) $ (Axiom 2)
  5. $\neg \neg P \to (P \to \neg P)$ (modus ponens, lines 4 and 2)
  6. $(\neg \neg P \to (P \to \neg P)) \to ((\neg \neg P \to P) \to (\neg \neg P \to \neg P))$ (Axiom 1)
  7. $(\neg \neg P \to P) \to (\neg \neg P \to \neg P)$ (modus ponens, lines 5 and 6)
  8. $\neg \neg P \to \neg P$ (modus ponens, lines 3 and 7)
  9. $\neg P$ (modus ponens, lines 1 and 8)
  • 2
    $\begingroup$ +1 - good job ! The only concern is about $\bot$ and the def of $\lnot P$ as $P \to \bot$. Is $\bot$ part of the original language ? $\endgroup$ – Mauro ALLEGRANZA Sep 20 '15 at 10:31
  • $\begingroup$ @Mauro Ugh, I hope so - if OP would care to be more specific about the definition of $\neg$ (if it's different), then I'd be happy to update the answer. Took me a while to find this one, though :P $\endgroup$ – Patrick Stevens Sep 20 '15 at 10:33
  • 2
    $\begingroup$ @Mauro - Actually, I don't think it's needed. I only use $\neg P = (P \to \bot)$ in the proof of Lemma 1, which I don't end up using at all. I just put it in because it demonstrated how I approached the problem. Answer edited to reflect this - thanks. $\endgroup$ – Patrick Stevens Sep 20 '15 at 10:34
  • $\begingroup$ Patrick, thanks for your excellent post! The problem is, as @MauroALLEGRANZA pointed out, $\neg$ is primitive in the system. Which means we cannot proceed as in your lemma 1. Otherwise that would be a pretty elegant proof.. $\endgroup$ – StudentType Sep 20 '15 at 13:21

Prover9 produced a fully automated proof using hyperresolution quickly. The use of hyperresolution comes as similar to using condensed detachment (which can get said to find the most general result of substitution instances of two well-formed formulas using modus ponens by finding the least amount of substitution in the antecedent of the longer substitution instance of the two wffs, and the most amount of substitution in the consequent of that same substitution instance of the longer wff). To learn how to follow this proof I'll suggest that you look here.

% -------- Comments from original proof --------

% Proof 1 at 3.78 (+ 0.47) seconds.

% Length of proof is 32.

% Level of proof is 13.

% Maximum clause weight is 14.

% Given clauses 1206.

1 P(C(C(x,N(x)),N(x))) # label(non_clause) # label(goal). [goal].

2 -P(C(x,y)) | -P(x) | P(y). [assumption].

3 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))). [assumption].

4 P(C(x,C(y,x))). [assumption].

5 P(C(x,C(N(x),y))). [assumption].

6 P(C(C(N(x),x),x)). [assumption].

7 -P(C(C(c1,N(c1)),N(c1))). [deny(1)].

9 P(C(x,C(y,C(z,y)))). [hyper(2,a,4,a,b,4,a)].

10 P(C(C(x,y),C(x,x))). [hyper(2,a,3,a,b,4,a)].

13 P(C(x,C(y,C(N(y),z)))). [hyper(2,a,4,a,b,5,a)].

18 P(C(x,C(C(N(y),y),y))). [hyper(2,a,4,a,b,6,a)].

26 P(C(x,x)). [hyper(2,a,10,a,b,9,a)].

29 P(C(C(C(x,y),x),C(C(x,y),y))). [hyper(2,a,3,a,b,26,a)].

38 P(C(C(x,y),C(x,C(N(y),z)))). [hyper(2,a,3,a,b,13,a)].

46 P(C(C(x,C(N(y),y)),C(x,y))). [hyper(2,a,3,a,b,18,a)].

167 P(C(x,C(N(C(y,x)),z))). [hyper(2,a,38,a,b,4,a)].

177 P(C(C(x,N(C(y,x))),C(x,z))). [hyper(2,a,3,a,b,167,a)].

510 P(C(C(N(x),N(C(y,N(x)))),x)). [hyper(2,a,46,a,b,177,a)].

575 P(C(x,C(C(N(y),N(C(z,N(y)))),y))). [hyper(2,a,4,a,b,510,a)].

588 P(C(x,C(C(C(y,z),y),C(C(y,z),z)))). [hyper(2,a,4,a,b,29,a)].

608 P(C(C(C(x,C(y,x)),z),z)). [hyper(2,a,29,a,b,9,a)].

652 P(C(x,C(C(C(y,C(z,y)),u),u))). [hyper(2,a,4,a,b,608,a)].

1597 P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))). [hyper(2,a,3,a,b,652,a)].

16656 P(C(C(x,C(C(y,x),z)),C(x,z))). [hyper(2,a,1597,a,b,3,a)].

16759 P(C(x,C(C(x,y),y))). [hyper(2,a,16656,a,b,588,a)].

16760 P(C(N(C(x,N(y))),y)). [hyper(2,a,16656,a,b,575,a)].

16865 P(C(x,C(y,C(C(y,z),z)))). [hyper(2,a,4,a,b,16759,a)].

17384 P(C(C(C(N(C(x,N(y))),y),z),z)). [hyper(2,a,16759,a,b,16760,a)].

20169 P(C(C(x,y),C(x,C(C(y,z),z)))). [hyper(2,a,3,a,b,16865,a)].

25974 P(C(N(C(x,N(y))),C(C(y,z),z))). [hyper(2,a,17384,a,b,20169,a)].

27812 P(C(C(x,N(x)),N(x))). [hyper(2,a,6,a,b,25974,a)].


I think I showed that it can be provable in your formal system. Let me explain.

We rely on the formal proofs in the site "Metamath Proof Explorer". The site possesses the proof of $\left(\phi \to \neg\phi\right) \to \neg\phi$ (Theorem pm2.01 (158)). We assume that the proofs of this formula and relevant lemmas are all correct, for they are computer-checked :)

However, there is a big gap remaining. The proof linked above is not based on your formal system. In fact, the formal system used in the above site has the following three axioms:

  1. your Ax1 (Axiom ax-2 (6)):

    $\left(\phi \to \left(\psi \to \chi\right)\right)\to\left(\left(\phi\to\psi\right)\to\left(\phi\to\chi\right)\right)$

  2. your Ax2 (Axiom ax-1 (5)):


  3. the axiom of contraposition (Axiom ax-3 (7)):


In addition, it has exactly the same inference rule as yours, i.e. the rule of Modus Ponens (Axiom ax-mp (8)).

So, The only axiom lacking in your formal system is ax-3 in the list above. The problem has been reduced to proving ax-3 in your system. Let's meta-prove that the system has such proof.

Under the assumptions $\neg\phi\to\neg\psi$, $\psi$ and $\neg\phi$, you have $\psi$ and $\neg\psi$, and therefore $\phi$ by Ax3 and the inference rule. By Deduction Theorem, you have $\neg\phi\to\phi$ assuming $\neg\phi\to\neg\psi$ and $\psi$; thus by Ax4 there is a proof of $\phi$ with the same assumption. Again by Deduction theorem, there is a formal proof of ax-3 in your formal system, without any assumption.

I did not directly give the proof of $\left(\phi \to \neg\phi\right) \to \neg\phi$; however from the above we showed that there is some proof of $\left(\phi \to \neg\phi\right) \to \neg\phi$, in your system. That is, firstly retrieve the proof of $\left(\phi \to \neg\phi\right) \to \neg\phi$ in the Metamath, in which the used axioms are ax-1, 2, and 3. It is not a proof in your system, but you can substitute every single occurrence of ax-3 by the proof of ax-3 in your system, obtained above. Then the resulting sequence of well-formed formulas is a proof in your system, for it has no longer has an occurrence of ax-3 as an axiom; instead ax-3 is only an intermediate result proved using ax1, 2, 3 and 4. Of course, ax-1 and 2 are no problem at all, as they are your ax2 and 1.

  • $\begingroup$ But the issue is exactly to prove in the system above... $\endgroup$ – StudentType Sep 19 '15 at 13:23
  • 1
    $\begingroup$ @StudentType I added the last paragraph. As in there, if you just want to know if there is a formal proof for $\left(\phi\to\neg\phi\right)\to\neg\phi$ in your system ("Is it provable at all?"), my answer should suffice. If you want to know the actual formal proof, you can actually work with the Metamath proof, but it would be a elephant job. If you want a simpler way, then you might want to re-ask a refined question, or modify this question (I don't know which is the better habit in Stack Overflow... I'm new here). $\endgroup$ – gksato Sep 20 '15 at 9:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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