I'm trying to prove:
$\phi\to\neg\neg\phi$
$(\neg\phi\to\neg\psi)\to((\neg\phi\to\psi)\to\phi)$
Using these axioms with modus ponens and the deduction theorem:
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)$
I have already found how to prove $\neg\neg\phi\to\phi$ following Theorem 6, but I can't see how to prove the reverse.
Thanks for your help!
A)
1) $\lnot \lnot \lnot \phi \to \lnot \phi$ --- from $\lnot \lnot \phi \to \phi$
2) $(\lnot \lnot \lnot \phi \to \lnot \phi) \to (\phi \to \lnot \lnot \phi)$ --- Ax.3
3) $\phi \to \lnot \lnot \phi$ --- from 1) and 2) by modus ponens.
B)
With Ax.1 and Ax.2 we can easily prove:
$\vdash \phi \to \phi$ --- (*).
With the Deduction Th we can prove the useful "derived rule" of Syllogism:
$\phi \to \psi, \ \psi \to \chi \vdash \phi \to \chi$.
Now for the proof:
1) $\lnot \phi \to (\lnot \psi \to \lnot \phi)$ --- Ax.1
2) $(\lnot \psi \to \lnot \phi) \to (\phi \to \psi)$ --- Ax.3
3) $\vdash \lnot \phi \to (\phi \to \psi)$ -- from 1) and 2) by Syll
4) $\lnot \phi \to (\phi \to \lnot \psi)$ --- from 3)
5) $(\lnot \phi \to (\phi \to \lnot \psi)) \to ((\lnot \phi \to \phi) \to (\lnot \phi \to \lnot \psi))$ --- Ax.2
6) $(\lnot \phi \to \phi) \to (\lnot \phi \to \lnot \psi)$ --- from 4) and 5) by mp
7) $(\lnot \phi \to \lnot \psi) \to (\psi \to \phi)$ --- Ax.3
8) $\vdash (\lnot \phi \to \phi) \to (\psi \to \phi)$ --- from 6) and 7) by Syll
9) $(\lnot \phi \to \phi) \to ((\lnot \phi \to \phi) \to \phi)$ --- from 8)
10) $((\lnot \phi \to \phi) \to ((\lnot \phi \to \phi) \to \phi)) \to (((\lnot \phi \to \phi) \to (\lnot \phi \to \phi)) \to ((\lnot \phi \to \phi) \to \phi))$ --- Ax.2
11) $((\lnot \phi \to \phi) \to (\lnot \phi \to \phi)) \to ((\lnot \phi \to \phi) \to \phi)$ --- from 9) and 10) by modus ponens
12) $(\lnot \phi \to \phi) \to (\lnot \phi \to \phi)$ --- from (*)
13) $\vdash (\lnot \phi \to \phi) \to \phi$ --- from 11) and 12) by modus ponens.
Having proved the three lemmata above, we can prove:
a) $(¬ϕ→¬ψ)$ --- premise
b) $(¬ϕ→ψ)$ --- premise
c) $\lnot \phi$ --- premise
d) $\psi$ --- from b) and c) by mp
e) $\lnot \psi$ --- from a) and c) by mp
f) $\phi$ --- from 3), d) and e) by mp twice
g) $\lnot \phi \to \phi$ --- from c) and f) by Ded Th
h) $\phi$ --- from 13) and g) by mp
$(¬ϕ→¬ψ) \to ((¬ϕ→ψ) \to ϕ)$ --- from a), b) and h) by Ded Th twice.
