Let $(\mathscr{L},\vdash)$ be a logic and $\Gamma\subseteq\mathscr{L}$ be a set of formulas such that for some $\varphi\in\mathscr{L}$ we have $$\Gamma\vdash\varphi\to\neg\varphi$$ $$\Gamma\vdash\neg\varphi\to\varphi$$Then show that, $$\Gamma\vdash(\varphi\to\neg\varphi)\to\varphi$$using only the following,

$\color{crimson}{\text{Axiom 1.}}\ P\to (Q\to P)$

$\color{crimson}{\text{Axiom 2.}}\ (S\to (P\to Q))\to((S\to P)\to (S\to Q))$

$\color{crimson}{\text{Axiom 3.}}\ (\neg Q\to\neg P)\to(P\to Q)$

$\color{crimson}{\text{Rule of Inference.}}$ Modus Ponens.

$\color{crimson}{\text{Theorem.}}$ Deduction Theorem.

I have tried for some hours to find a proof of the claim but couldn't succeed. Can anyone help?


This may not be the fastest way, but it works:

First prove Hypothetical Syllogism ($\{A \rightarrow B, B \rightarrow C \} \vDash A \rightarrow C$) as a derived inference principle:

  1. $A \rightarrow B$ Premise

  2. $B \rightarrow C$ Premise

  3. $(B \rightarrow C) \rightarrow (A \rightarrow (B \rightarrow C))$ Axiom 1

  4. $A \rightarrow (B \rightarrow C)$ MP 2,3

  5. $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$ Axiom 2

  6. $(A \rightarrow B) \rightarrow (A \rightarrow C)$ MP 4,5

  7. $A \rightarrow C$ MP 1,6

And now:

  1. $\neg \varphi \rightarrow (\neg \neg (\varphi \rightarrow \neg \varphi) \rightarrow \neg \varphi)$ Axiom 1

  2. $(\neg \neg (\varphi \rightarrow \neg \varphi) \rightarrow \neg \varphi) \rightarrow (\varphi \rightarrow \neg (\varphi \rightarrow \neg \varphi))$ Axiom 3

  3. $\neg \varphi \rightarrow (\varphi \rightarrow \neg (\varphi \rightarrow \neg \varphi))$ Hypothetical Syllogism 1,2

  4. $(\neg \varphi \rightarrow (\varphi \rightarrow \neg (\varphi \rightarrow \neg \varphi))) \rightarrow ((\neg \varphi \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \neg (\varphi \rightarrow \neg \varphi)))$ Axiom 2

  5. $(\neg \varphi \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \neg (\varphi \rightarrow \neg \varphi))$ MP 3,4

  6. $\neg \varphi \rightarrow \varphi$ Premise

  7. $\neg \varphi \rightarrow \neg (\varphi \rightarrow \neg \varphi)$ MP 5,6

  8. $(\neg \varphi \rightarrow \neg (\varphi \rightarrow \neg \varphi)) \rightarrow (\varphi \rightarrow \neg \varphi) \rightarrow \varphi)$ Axiom 3

  9. $(\varphi \rightarrow \neg \varphi) \rightarrow \varphi$ MP 7,8

  • $\begingroup$ "This may not be the fastest way." Basically, it's possible to give Prover9 something like the axioms and the assumptions (just treat the letter $\phi$ like some constant like 'a') with no help whatsoever and there's something like a solution produced/hinted at in less than 2 one-hundreths of a second. No doubt, it took you orders of seconds longer... :) $\endgroup$ – Doug Spoonwood Dec 10 '16 at 20:55
  • $\begingroup$ @DougSpoonwood Yeah, just a little longer :) $\endgroup$ – Bram28 Dec 10 '16 at 20:56

Your Answer

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