How can we prove $(P \to \neg P) \to \neg P$ in this system? 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.
 A: 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:


*

*$(\neg \neg P \to \neg P) \to \neg P$ (Axiom 4)

*$P \to \neg P$ (hypothesis)

*$\neg \neg P \to P$ (lemma 2)

*$(P \to \neg P) \to (\neg \neg P \to (P \to \neg P)) $ (Axiom 2)

*$\neg \neg P \to (P \to \neg P)$ (modus ponens, lines 4 and 2)

*$(\neg \neg P \to (P \to \neg P)) \to ((\neg \neg P \to P) \to (\neg \neg P \to \neg P))$ (Axiom 1)

*$(\neg \neg P \to P) \to (\neg \neg P \to \neg P)$ (modus ponens, lines 5 and 6)

*$\neg \neg P \to \neg P$ (modus ponens, lines 3 and 7)

*$\neg P$ (modus ponens, lines 1 and 8)

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:


*

*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)$ 

*your Ax2 (Axiom ax-1 (5)):
$\phi\to\left(\psi\to\phi\right)$

*the axiom of contraposition (Axiom ax-3 (7)):
$\left(\neg\phi\to\neg\psi\right)\to\left(\psi\to\phi\right)$
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.
