I'm trying to prove:



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!


1 Answer 1



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.


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.

  • $\begingroup$ Can't believe I didn't realize that just adding another negation and using contraposition again was enough to show double negation introduction. Thanks! $\endgroup$ May 2, 2016 at 14:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.