Proving double negation from an axiomatization of classical logic

Question

Suppose we have the following axiomatic representation of classical logic :

1. φ → (ψ → φ)
2. (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))
3. (φ ∧ ψ) → φ
4. (φ ∧ ψ) → ψ
5. (φ → ψ) → ((φ → χ) → (φ → (ψ ∧ χ)))
6. φ → (φ ∨ ψ)
7. ψ → (φ ∨ ψ)
8. (φ → χ) → ((ψ → χ) → ((φ ∨ ψ) → χ))
9. (φ → ψ) → ((φ → ¬ψ) → ¬φ)
10. ¬φ → (φ → ψ)
11. φ ∨ ¬φ

How can double negation : ¬¬φ → φ be proven using the above axioms?

Answer 1

Borrowing from Kevin's answer, but working around the second point that is not motivated:

1. $\phi\rightarrow(\neg\neg\phi\rightarrow\phi)\tag{axiom 1}$
2. $\neg\neg\neg\phi\rightarrow(\neg\neg\phi\rightarrow\phi)\tag{axiom 10}$

Now to use axiom 8 we will need the $\phi\lor\neg\neg\neg\phi$ instead of axiom 11. To do that we will need $\neg\phi\rightarrow\neg\neg\neg\phi$ to prove that $\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi)$ that will together with axiom 6 prove that.

3. $\neg\neg\phi\rightarrow(\neg\phi\rightarrow\neg\neg\neg\phi)\tag{axiom 10}$
4. $(\neg\neg\phi\rightarrow(\neg\phi\rightarrow\neg\neg\neg\phi))\rightarrow\\((\neg\neg\neg\phi\rightarrow(\neg\phi\rightarrow\neg\neg\neg\phi)\rightarrow((\neg\neg\phi\lor\neg\neg\neg\phi)\rightarrow(\neg\phi\rightarrow\neg\neg\neg\phi))\tag{axiom 8}$
5. $(\neg\neg\neg\phi\rightarrow(\phi\rightarrow\neg\neg\neg\phi)\rightarrow((\neg\neg\phi\lor\neg\neg\neg\phi)\rightarrow(\neg\phi\rightarrow\neg\neg\neg\phi)\tag{MP(3+4)}$
6. $\neg\neg\neg\phi\rightarrow(\neg\phi\rightarrow\neg\neg\neg\phi)\tag{axiom 1}$
7. $(\neg\neg\phi\lor\neg\neg\neg\phi)\rightarrow(\neg\phi\rightarrow\neg\neg\neg\phi)\tag{MP(6+5)}$
8. $\neg\neg\phi\lor\neg\neg\neg\phi\tag{axiom 12}$
9. $\neg\phi\rightarrow\neg\neg\neg\phi\tag{MP(8+7)}$

Now we can use this to do a deduction-proof-like reasoning by assuming $\neg\phi$ we have $\neg\neg\neg\phi$ and therefore $\phi\lor\neg\neg\neg\phi$ and concluding the implication:

10. $\neg\neg\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi)\tag{axiom 7}$
11. $(\neg\neg\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi))\rightarrow\\ (\neg\phi\rightarrow(\neg\neg\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi))\tag{axiom 1}$
12. $\neg\phi\rightarrow(\neg\neg\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi))\tag{MP(11+10)}$
13. $(\neg\phi\rightarrow(\neg\neg\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi)))\rightarrow\\((\neg\phi\rightarrow\neg\neg\neg\phi)\rightarrow(\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi)))\tag{axiom 2}$
14. $((\neg\phi\rightarrow\neg\neg\neg\phi)\rightarrow(\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi))\tag{MP(12+13)}$
15. $\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi)\tag{MP(14+9)}$
16. $\phi\rightarrow(\phi\lor\neg\neg\neg\phi)\tag{axiom 6}$

The rest is to use axiom 8 to conclude that $\phi\lor\neg\neg\neg\phi$ and then again axiom 8 to reach the conclusion:

17. $(\phi\rightarrow(\phi\lor\neg\neg\neg\phi))\rightarrow((\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi))\rightarrow((\phi\lor\neg\phi)\rightarrow(\phi\lor\neg\neg\neg\phi))\tag{axiom 8}$
18. $\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi))\rightarrow((\phi\lor\neg\phi)\rightarrow(\phi\lor\neg\neg\neg\phi))\tag{MP(17+16)}$
19. $((\phi\lor\neg\phi)\rightarrow(\phi\lor\neg\neg\neg\phi))\tag{MP(18+15)}$
20. $\phi\lor\neg\phi\tag{axiom 12}$
21. $\phi\lor\neg\neg\neg\phi\tag{MP(19+20)}$
22. $(\phi\rightarrow(\neg\neg\phi\rightarrow\phi))\rightarrow\\ ((\neg\neg\neg\phi\rightarrow(\neg\neg\phi\rightarrow\phi))\rightarrow((\phi\lor\neg\neg\neg\phi)\rightarrow(\neg\neg\phi\rightarrow\phi)))\tag{axiom 8}$
23. $((\neg\neg\neg\phi\rightarrow(\neg\neg\phi\rightarrow\phi))\rightarrow((\phi\lor\neg\neg\neg\phi)\rightarrow(\neg\neg\phi\rightarrow\phi))\tag{MP(1+22)}$
24. $(\phi\lor\neg\neg\neg\phi)\rightarrow(\neg\neg\phi\rightarrow\phi)\tag{MP(2+23)}$
25. $\neg\neg\phi\rightarrow\phi\tag{MP(21+24)}$

Answer 2

Apply 8. with $\varphi = \varphi$, $\psi = \lnot\varphi$ and $\chi = \lnot\lnot\varphi \to \varphi$.

By modus ponens, you have to show three things

• $\varphi \to (\lnot\lnot\varphi \to \varphi)$ : that is axiom 1.
• $\lnot\varphi \to (\lnot\lnot\varphi \to \varphi)$ : that is a kind of 10, where the negation is on second term instead of first.
• $\varphi\lor\lnot\varphi$ : that is axiom 11.

Edit : skyking is right. We need to show that for any $A,B,C$, $(A \to (B \to C)) \leftrightarrow (B \to (A \to C))$, but that doesn't seem to be as easy as I first thought.