How do I prove double negation elimination in a propositional logic axiom system? Here are my axioms:


*

*$X \rightarrow (Y \rightarrow X)$

*$(X \rightarrow (Y \rightarrow Z)) \rightarrow ((X \rightarrow Y) \rightarrow (X \rightarrow Z))$

*$(\lnot Y \rightarrow \lnot X) \rightarrow ((\lnot Y \rightarrow X) \rightarrow Y)$


You can use any uniform substitution of these axioms, and you can use Modus Ponens.
Need to prove $\lnot \lnot P \vdash P$.
 A: Here is the proof [ref.to Theodore Sider, Logic for Philosophy (2009), Exercise 2.4, page 60] :
Lemma 1 : $\vdash P \rightarrow P$
(1) $P → ((P \rightarrow P) → P)$ --- Ax.1
(2) $(P → ((P \rightarrow P) → P)) → ((P → (P \rightarrow P)) → (P \rightarrow P))$ --- Ax.2
(3) $(P → (P \rightarrow P)) → (P \rightarrow P)$ --- from (1) and (2) by modus ponens
(4) $P → (P \rightarrow P)$ --- Ax.1

(5) $P \rightarrow P$ --- from (3) and (4) by modus ponens.


Lemma 2 : $P \to Q, Q \to R \vdash P \to R$ [we call this "derived rule" : Hypothetical Syllogism]
(1) $P \to Q$ --- premise
(2) $Q \to R$ --- premise
(3) $(Q \to R) \to (P \to (Q \to R))$ --- Ax.1
(4) $P \to (Q \to R)$ --- from (2) and (3) by mp
(5) $(P \to (Q \to R)) \to ((P \to Q) \to (P \to R))$ --- Ax.2
(6) $(P \to Q) \to (P \to R)$ --- from (4) and (5) by modus ponens

(7) $P \to R$ --- from (1) and (6) by modus ponens.


Lemma 3 : $\vdash \lnot P \to (P \to P)$
(1) $(P \to P) \to (\lnot P \to (P \to P))$ --- Ax.1
(2) $P \to P$ --- Lemma 1

(3) $\lnot P \to (P \to P)$ --- from (1) and (2) by mp.


Proposition : $\vdash \lnot \lnot P \to P$
(1) $(\lnot P \rightarrow \lnot \lnot P) \rightarrow ((\lnot P \rightarrow \lnot P) \rightarrow P)$ --- from Ax.3 with $\lnot P$ in place of $X$
(2) $\lnot \lnot P \to (\lnot P \to \lnot \lnot P)$ --- Ax.1
(3) $\lnot \lnot P \to ((\lnot P \rightarrow \lnot P) \rightarrow P)$ --- from (1) and (2) by HS (Lemma 2)
(4)  $\lnot \lnot P \to (\lnot P \to \lnot P)$ --- from Lemma 3 with $\lnot P$ in place of $P$
(5) $(\lnot \lnot P \to ((\lnot P \rightarrow \lnot P) \rightarrow P)) \to ((\lnot \lnot P \to (\lnot P \rightarrow \lnot P)) \to (\lnot \lnot P \to P))$ --- Ax.2

(6) $\lnot \lnot P \to P$ --- from (5), (3) and (4) by modus ponens twice.

