# Prove ⊢(a→b)→(¬b→¬a) in HPC proof system

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

⊢(a→b)→(¬b→¬a)

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.

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

• Nice! But I don't quite see how to do $\neg \neg A\rightarrow A$...can you please show? Thanks! – Bram28 Dec 1 '16 at 13:41
• 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$? – Bram28 Dec 1 '16 at 13:57
• Thank you very much! I didn't quite understand how you proved (1), but nevertheless I managed to prove it myself. Cheers! – superstav Dec 1 '16 at 14:57
• @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. – Bram28 Dec 1 '16 at 15:07
• 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 – Doug Spoonwood Dec 1 '16 at 17:39