Double Negation

Definition

Double Negation Introduction

Law of Double Negation Introduction:

If we can conclude $p$, then we may infer $\neg \neg p$:

$p \vdash \neg \neg p$

where $\neg$ denotes the negation operator.

It can be written:

$\displaystyle {p \over \neg \neg p} \neg \neg_i$

Its abbreviation in a tableau proof is $\neg \neg \mathcal I$.

Double Negation Elimination

When we allow the Law of the Excluded Middle, we can demonstrate the converse:

Law of Double Negation Elimination:

If we can conclude $\neg \neg p$, then we may infer $p$:

$\neg \neg p \vdash p$

It can be written:

$\displaystyle {\neg \neg p \over p} \neg \neg_e$

Its abbreviation in a tableau proof is $\neg \neg \mathcal E$.

The Law of Double Negation Elimination may be taken as an axiom instead of the Law of the Excluded Middle. Thus the LEM may be proved from $\neg \neg \mathcal E$.

Alternative Renditions

These can alternatively be rendered as:

• $\vdash \neg \neg p \implies p$

• $\vdash p \implies \neg \neg p$

or:

• $\vdash p \iff \neg \neg p$

They can be seen to be logically equivalent to the forms above by application of the Extended Rule of Implication.

Proofs

Proof by Natural deduction

These are proved by the Tableau method.

$p \vdash \neg \neg p$

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$p$	P	(None)
2		2	$\neg p$	A	(None)
3		1, 2	$\bot$	$\neg \mathcal E$	1, 2
4		1	$\neg \neg p$	$\neg \mathcal I$	2-3

$\blacksquare$

$\neg \neg p \vdash p$

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$\neg \neg p$	P	(None)
2		(None)	$p \lor \neg p$	LEM	(None)
3		3	$p$	A	(None)
4		4	$\neg p$	A	(None)
5		1, 4	$\bot$	$\neg \mathcal E$	4, 1
6		1, 4	$p$	$\bot \mathcal E$	5
7		1	$p$	$\lor \mathcal E$	2, 3-3, 4-6

$\blacksquare$

Deriving the Law of the Excluded Middle from the Rule of Double Negation Elimination:

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$\neg \left({p \lor \neg p}\right)$	P	(None)
2		2	$p$	A	(None)
3		2	$p \lor \neg p$	$\lor \mathcal I_1$	2
4		1, 2	$\bot$	$\neg \mathcal E$	3, 1
5		1	$\neg p$	$\neg \mathcal I$	2, 4
6		1	$p \lor \neg p$	$\lor \mathcal I_2$	5
7		1	$\bot$	$\neg \mathcal E$	6, 1
8			$\neg \neg \left({p \lor \neg p}\right)$	P	1, 7
9			$p \lor \neg p$	$\neg \neg \mathcal E$ (from above)	8

$\blacksquare$

Proof by Truth Table

We apply the Method of Truth Tables to the proposition.

As can be seen by inspection, appropriate truth values match for both models.

$\begin{array}{|c||ccc|} \hline p & \neg & \neg & p \\ \hline F & F & T & F \\ T & T & F & T \\ \hline \end{array}$

Hence $p \dashv \vdash \neg \neg p$.

$\blacksquare$

Comment

As we see, the use of the Law of the Excluded Middle invalidates the Law of Double Negation Elimination from the intuitionist system.

Notice the difference between Double Negation Elimination and Double Negation Introduction, whereby it can be seen to be "intuitively obvious" that if a statement is true, then it is not the case that it is not true. However, if all we know is that a statement is not "not-true", we can not be certain that it is true without accepting that there are only two possible truth values. Such distinctions may be important when considering, for example, multi-value logic.

However, when analysing logic from a purely classical standpoint, it is common and acceptable to make the simplification of taking just one Double Negation rule:

$p \dashv \vdash \neg \neg p$

Sources

• Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{I}: \S 3, \ \text{I}: \S 5$: Theorem $\text{T11, T12}$
• Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{II}: \S 5$: Theorem $\text{T110}$
• E.J. Lemmon: Beginning Logic (1965): $\S 1.2$
• Alan G. Hamilton: Logic for Mathematicians (1978): $\S 1.2$: Definition $1.5 \ \text{(c)}$
• Thomas A. Whitelaw: An Introduction to Abstract Algebra (1978)... (previous)... (next): $\S 3$
• H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability (1996): Exercise $1.14: 12 \ (1)$
• Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems (2000): $\S 1.2.1, \ \S 1.2.2$