# How to show that $\Gamma\vdash (\varphi\to\neg\varphi)\to\varphi$?

Problem.

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

• "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... :) – Doug Spoonwood Dec 10 '16 at 20:55
• @DougSpoonwood Yeah, just a little longer :) – Bram28 Dec 10 '16 at 20:56