# How do I prove double negation elimination in a propositional logic axiom system?

Here are my axioms:

1. $X \rightarrow (Y \rightarrow X)$
2. $(X \rightarrow (Y \rightarrow Z)) \rightarrow ((X \rightarrow Y) \rightarrow (X \rightarrow Z))$
3. $(\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$.

• You can see in the answer to this post the proof of $\lnot \lnot P \vdash P$ (see Lemma 1). – Mauro ALLEGRANZA Jan 27 '15 at 8:51
• @MauroALLEGRANZA check the edit history; I merely replaced each '->' with '\rightarrow'. My guess is that if the axiom is incorrect now, it was incorrect to begin with. – daOnlyBG Jan 27 '15 at 9:54
• @daOnlyBG - the problem is that the "tilde" (~) when enclosed in the dollar sign disappear; thus, we have to replace it with the appropriate negeation sign : $\lnot$. – Mauro ALLEGRANZA Jan 27 '15 at 9:58
• @MauroALLEGRANZA ah, I see. Thanks for editing it. – daOnlyBG Jan 27 '15 at 9:59

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.

• Strictly speaking your using Hypothetical Syllogism in step 6 of the proof of Hypothetical Syllogism, because you use MP to establish 4. By saying "premise" your implicitly assuming some additional meta-mathematical mechanism of constructing a formal proof above and beyond that in the OP, which states you must only use those axioms plus substitution. All other steps in your proofs are valid, that is they really do only require substitution with the axioms. – samthebest Mar 11 '16 at 11:26