Proving double negation from an axiomatization of classical logic Suppose we have the following axiomatic representation of classical logic :


*

*φ → (ψ → φ)

*(φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))

*(φ ∧ ψ) → φ

*(φ ∧ ψ) → ψ

*(φ → ψ) → ((φ → χ) → (φ → (ψ ∧ χ)))

*φ → (φ ∨ ψ)

*ψ → (φ ∨ ψ)

*(φ → χ) → ((ψ → χ) → ((φ ∨ ψ) → χ))

*(φ → ψ) → ((φ → ¬ψ) → ¬φ)

*¬φ → (φ → ψ)

*φ ∨ ¬φ 


How can double negation :  ¬¬φ → φ  be proven using the above axioms?
 A: Borrowing from Kevin's answer, but working around the second point that is not motivated:


*

*$\phi\rightarrow(\neg\neg\phi\rightarrow\phi)\tag{axiom 1}$

*$\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.


*$\neg\neg\phi\rightarrow(\neg\phi\rightarrow\neg\neg\neg\phi)\tag{axiom 10}$

*$(\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}$ 

*$(\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)}$

*$\neg\neg\neg\phi\rightarrow(\neg\phi\rightarrow\neg\neg\neg\phi)\tag{axiom 1}$

*$(\neg\neg\phi\lor\neg\neg\neg\phi)\rightarrow(\neg\phi\rightarrow\neg\neg\neg\phi)\tag{MP(6+5)}$

*$\neg\neg\phi\lor\neg\neg\neg\phi\tag{axiom 12}$

*$\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:


*$\neg\neg\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi)\tag{axiom 7}$

*$(\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}$

*$\neg\phi\rightarrow(\neg\neg\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi))\tag{MP(11+10)}$

*$(\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}$

*$((\neg\phi\rightarrow\neg\neg\neg\phi)\rightarrow(\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi))\tag{MP(12+13)}$

*$\neg\phi\rightarrow(\phi\lor\neg\neg\neg\phi)\tag{MP(14+9)}$

*$\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:


*$(\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}$

*$\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)}$

*$((\phi\lor\neg\phi)\rightarrow(\phi\lor\neg\neg\neg\phi))\tag{MP(18+15)}$

*$\phi\lor\neg\phi\tag{axiom 12}$

*$\phi\lor\neg\neg\neg\phi\tag{MP(19+20)}$

*$(\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}$

*$((\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)}$

*$(\phi\lor\neg\neg\neg\phi)\rightarrow(\neg\neg\phi\rightarrow\phi)\tag{MP(2+23)}$

*$\neg\neg\phi\rightarrow\phi\tag{MP(21+24)}$

A: 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.
