# 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). Jan 27, 2015 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. Jan 27, 2015 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$. Jan 27, 2015 at 9:58
• @MauroALLEGRANZA ah, I see. Thanks for editing it. Jan 27, 2015 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. Mar 11, 2016 at 11:26