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

Question

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?

Answer 1

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