As stated in the title, I am asked to give a proof that:


Using a system with the Modus Ponens rule, and the following axioms:

  • A1: a→(b→a)
  • A2: (a→(b→c))→((a→b)→(a→c))
  • A3: (¬b→¬a)→(a→b)

According to the deduction theorem, it is sufficient to prove:

{(a→b), ¬b} ⊢ ¬a

Using the A3 I am managing at "removing" ¬'s, but cannot think of a way to add ¬'s.

Thank you very much for you help.

  • $\begingroup$ Can you prove $a\to b\vdash \neg b\to \neg a$? Have you learned the deduction theorem? $\endgroup$ – Git Gud Dec 1 '16 at 11:19
  • $\begingroup$ @gitgud I have learned the deduction theorem, and I have tried proving that statement, but also to no avail. $\endgroup$ – superstav Dec 1 '16 at 11:36
  • $\begingroup$ It is instructive to use the constructive proof of the deduction theorem to find proofs like the one you asked about. $\endgroup$ – Git Gud Dec 1 '16 at 15:02
  • 1
    $\begingroup$ @GitGud OK, I'll remove it. $\endgroup$ – Bram28 Dec 1 '16 at 15:04

We have to prove some preliminary results :

0) $\vdash a \to a$

1) $a \to b, b \to c \vdash a \to c$ (use Deduction Th)

2) $\vdash \lnot \lnot a \to a$ (use 1. and axiom A3)

3) $\vdash a \to \lnot \lnot a$ (use 2. and axiom A3).

Now :

i) $a \to b$

ii) $\vdash b \to \lnot \lnot b$

iii) $a \to \lnot \lnot b$ (with 1. above)

iv) $\vdash \lnot \lnot a \to a$

v) $\lnot \lnot a \to \lnot \lnot b$ (with 1. above)

vi) $\lnot b \to \lnot a$ (with A3)

$\vdash (a \to b) \to (\lnot b \to \lnot a)$ (from i. and vi. by Ded Th).

Proof of 2) :

i) $\vdash \lnot a \to (\lnot b \to \lnot a)$ (axiom A1)

ii) $\vdash (\lnot b \to \lnot a) \to (a \to b)$ (axiom A3)

iii) $\vdash \lnot a \to (a \to b)$ (with 1.)

iv) $\vdash \lnot \lnot a \to (\lnot a \to \lnot \lnot \lnot a)$ (from iii.)

v) $\vdash (\lnot a \to \lnot \lnot \lnot a) \to (\lnot \lnot a \to a)$ (axiom A3)

vi) $\vdash \lnot \lnot a \to (\lnot \lnot a \to a)$ (with 1.)

vii) $\vdash (\lnot \lnot a \to (\lnot \lnot a \to a)) \to ((\lnot \lnot a \to \lnot \lnot a) \to (\lnot \lnot a \to a))$ (axiom A2)

viii) $\vdash (\lnot \lnot a \to a)$ (with vi. and 0. above, by modus ponens twice).

Proof of 3) :

i) $\vdash \lnot \lnot \lnot a \to \lnot a$ (from 1.)

ii) $\vdash (\lnot \lnot \lnot a \to \lnot a) \to (a \to \lnot \lnot a)$ (axiom A3)

iii) $\vdash (a \to \lnot \lnot a)$ (by modus ponens).

  • $\begingroup$ Nice! But I don't quite see how to do $\neg \neg A\rightarrow A$...can you please show? Thanks! $\endgroup$ – Bram28 Dec 1 '16 at 13:41
  • $\begingroup$ OK, I found a proof of $\neg \neg a \rightarrow a$ but I had to use $\neg \neg a \rightarrow (\neg \neg \neg \neg a \rightarrow \neg \neg a)$ (an instance of axiom 1) as a starting point. So, in addition to axiom 3, do you indeed need axiom 1 as well to prove $\neg \neg a \rightarrow a$? $\endgroup$ – Bram28 Dec 1 '16 at 13:57
  • $\begingroup$ Thank you very much! I didn't quite understand how you proved (1), but nevertheless I managed to prove it myself. Cheers! $\endgroup$ – superstav Dec 1 '16 at 14:57
  • $\begingroup$ @MauroAllegranza Thanks! That is what I found too, with $\neg \neg \neg a$ for $b$ right from the start. So we do indeed need axiom 1. $\endgroup$ – Bram28 Dec 1 '16 at 15:07
  • $\begingroup$ You may prove such results as preliminary, but they are not all necessary. Is even 0) necessary? As I recall, it holds in classical logic that if a theorem does not have any instance of '$\lnot$$\lnot$' in the formula, then there exists a proof P of that formula such that '$\lnot$$\lnot$' does not appear in any step of P. $\lnot$$\lnot$-free proofs gets investigated more in this paper: michaelbeeson.com/research/papers/dn.pdf $\endgroup$ – Doug Spoonwood Dec 1 '16 at 17: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.