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
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.
