Prove that contrapositive rule is equivalent to the rule of double negation

Question

Many deduction systems I see at various places (for example here includes the following two axioms $$ a \Rightarrow (b \Rightarrow a),\\ [a \Rightarrow (b \Rightarrow c)]\Rightarrow [(a\Rightarrow b) \Rightarrow ( a \Rightarrow c)]. $$ Now we need a third axiom. I see two versions of the third axiom: $(\neg \neg p) \Rightarrow p$ and $[(\neg p) \Rightarrow (\neg q) ]\Rightarrow (q\Rightarrow p).$

How could we prove using natural deduction that these two versions of "third" axioms are equivalent?

The page in the above link provides one direction of the implication, but I could not find the other direction.

Answer 1

Part 1): this is the part not provided by Wiki's page above.

1. $¬¬p \to p$ --- Premise

2. $(¬p \to ¬q)$ assumption [a]

3. $q$ --- assumption [b]

4. $¬p$ --- assumption [c]

5. $¬q$ --- from 4) and 2) by $(\to \text E$) (MP)

6. $\bot$ --- contradiction from 3) and 5)

7. $¬¬p$ --- from $(\lnot \text I)$, discharging assumption [c]

8. $p$ --- from 7) and 1) by $(\to \text E$)

$(q \to p)$ --- from 3) and 8) by $(\to \text I)$, discharging assumption [b].

Note: the Natural Deduction derivation above uses the Neg-Intro rule: "if we have derived $\varphi \vdash \bot$, then conclude with $\vdash \lnot \varphi$", i.e. the derivation of a contradiction allow us to negate a premise (see steps 3)-7) above).

With axioms and MP, the derivation requires the following tautology: $(p \to q) \to ((p \to \lnot q) \to \lnot p)$. Using it with $\lnot p$ in place of $p$ will get $\lnot \lnot p$ (step 7) above).

---

A different approach is the following, using a couple of preliminary results:

L1) $p \to p$ --- from (Ax.1) and (Ax.2)

L2) Deduction (meta-)Theorem, proved with (Ax.1), (Ax.2) and L1).

L3) $p \to q, q \to r \vdash p \to r$ (aka: Syllogism), using DT.

Now we have:

1. $\lnot p \to (\lnot q \to \lnot p)$ --- (Ax.1)

2. $(\lnot q \to \lnot p) \to (p \to q)$ --- Contraposition

3. $\lnot p \to (p \to q)$ --- from 1) and 2) by Syll.

4. $\lnot \lnot p \to (\lnot p \to \lnot \lnot \lnot p)$ --- instance of 3)

5. $(\lnot p \to \lnot \lnot \lnot p) \to (\lnot \lnot p \to p)$ --- Contraposition

6. $\lnot \lnot p \to (\lnot \lnot p \to p)$ --- from 4) and 59 by Syll

7. a suitable instance of (Ax.2) with $\lnot \lnot p \to (\lnot \lnot p \to p)$in place of $[a \to (b \to c)]$

8. $(\lnot \lnot p \to \lnot \lnot p) \to (\lnot \lnot p \to p)$ --- from 6) and 7) by MP

$\lnot \lnot p \to p$ --- from 8) and L1) by MP.

---

---

Part 2): the proof provided by Wiki's page above uses a sort of trick. Here is the versione for Natural Deduction.

From Contraposition we derive:$(¬¬ \phi \to ¬¬ \psi) \to (\phi \to \psi)$ and we instantiate it with $p$ as $\psi$ and some provable formula (e.g. $p \to p$ or $\top$) as $\phi$, to get:

1. $(¬¬ \top \to ¬¬ p) \to (\top \to p)$.

Then assume 2) $¬¬p$ and from it and $(\to \text I)$ we have:

3. $(¬¬\top \to ¬¬p)$, and

4. $(\top \to p)$ --- from 1) and 3) by $(\to \text E)$.

Now, using 5) $\vdash \top$, we derive:

$p$ --- from 4) and 5) by $(\to \text E)$.