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

Question

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.

Answer 1

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).