Hilbert style proof of double negation introduction and reductio ab adsurdum

Question

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!

Answer 1

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.