proving [${\phi,\phi\to\psi}⊢\neg(\phi\to\neg\psi)$)] only with axioms

Question

Is it possible to show

${\phi,\phi\to\psi}⊢\neg(\phi\to\neg\psi)$

only with modus ponens,deduction theorem and these three axiom?

A1: $\phi\to(\psi\to\phi)$

A2: $(\phi\to(\psi\to\pi))\to((\phi\to\psi)\to(\phi\to\pi))$

A3: $(\neg\phi\to\neg\psi)\to(\psi\to\phi)$

looks so easy but it's too hard for me to take even a step

$\neg\neg\phi\to\phi$ was quiet devastating too

Answer 1

Hint : the derivation is long and boring ...

Form Axioms above, we have to derive some preliminary results :

A) $\vdash \lnot \lnot \phi \to \phi$

B) $\vdash \phi \to \lnot \lnot \phi$

C) $\vdash (\phi \to \psi) \to (\lnot \psi \to \lnot \phi)$. The derivation needs A), B), D) and Ax.3.

D) $\phi \to \psi, \psi \to \chi \vdash \phi \to \chi$. The derivation is straightforward: it needs modus ponens twice and a final application of the Deduction Th.

Now the derivation :

1) From modus ponens, by Deduction Th twice :

$\vdash \phi \to ((\phi \to \lnot \psi) \to \lnot \psi)$.

2) From C) above :

$\vdash ((\phi \to \lnot \psi) \to \lnot \psi) \to (\lnot \lnot \psi \to \lnot (\phi \to \lnot \psi))$.

3) From 1) and 2) by D) :

$\vdash \phi \to (\lnot \lnot \psi \to \lnot (\phi \to \lnot \psi))$.

4) $\phi$ --- premise

5) $\phi \to \psi$ --- premise

6) $\psi$ --- from 4) and 5) by mp

7) $\lnot \lnot \psi$ --- from 6) and B) by mp

8) $\lnot (\phi \to \lnot \psi)$ --- from 3), 4) and 7) by mp twice.