# Double negation

Short description: Propositional logic theorem
Type Theorem If a statement is true, then it is not the case that the statement is not true."

In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition A is logically equivalent to not (not-A), or by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign ~ expresses negation.

Like the law of the excluded middle, this principle is considered to be a law of thought in classical logic, but it is disallowed by intuitionistic logic. The principle was stated as a theorem of propositional logic by Russell and Whitehead in Principia Mathematica as:

$\displaystyle{ \mathbf{*4\cdot13}. \ \ \vdash.\ p \ \equiv \ \thicksim(\thicksim p) }$
"This is the principle of double negation, i.e. a proposition is equivalent of the falsehood of its negation."

## Elimination and introduction

Double negation elimination and double negation introduction are two valid rules of replacement. They are the inferences that, if not not-A is true, then A is true, and its converse, that, if A is true, then not not-A is true, respectively. The rule allows one to introduce or eliminate a negation from a formal proof. The rule is based on the equivalence of, for example, It is false that it is not raining. and It is raining.

The double negation introduction rule is:

P $\displaystyle{ \Rightarrow }$ $\displaystyle{ \neg }$$\displaystyle{ \neg }$P

and the double negation elimination rule is:

$\displaystyle{ \neg }$$\displaystyle{ \neg }$P $\displaystyle{ \Rightarrow }$ P

Where "$\displaystyle{ \Rightarrow }$" is a metalogical symbol representing "can be replaced in a proof with."

In logics that have both rules, negation is an involution.

### Formal notation

The double negation introduction rule may be written in sequent notation:

$\displaystyle{ P \vdash \neg \neg P }$

The double negation elimination rule may be written as:

$\displaystyle{ \neg \neg P \vdash P }$

In rule form:

$\displaystyle{ \frac{P}{\neg \neg P} }$

and

$\displaystyle{ \frac{\neg \neg P}{P} }$

or as a tautology (plain propositional calculus sentence):

$\displaystyle{ P \to \neg \neg P }$

and

$\displaystyle{ \neg \neg P \to P }$

These can be combined into a single biconditional formula:

$\displaystyle{ \neg \neg P \leftrightarrow P }$.

Since biconditionality is an equivalence relation, any instance of ¬¬A in a well-formed formula can be replaced by A, leaving unchanged the truth-value of the well-formed formula.

Double negative elimination is a theorem of classical logic, but not of weaker logics such as intuitionistic logic and minimal logic. Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is $\displaystyle{ \neg \neg \neg A \vdash \neg A }$.

Because of their constructive character, a statement such as It's not the case that it's not raining is weaker than It's raining. The latter requires a proof of rain, whereas the former merely requires a proof that rain would not be contradictory. This distinction also arises in natural language in the form of litotes.

## Proofs

### In classical propositional calculus system

In Hilbert-style deductive systems for propositional logic, double negation is not always taken as an axiom (see list of Hilbert systems), and is rather a theorem. We describe a proof of this theorem in the system of three axioms proposed by Jan Łukasiewicz:

A1. $\displaystyle{ \phi \to \left( \psi \to \phi \right) }$
A2. $\displaystyle{ \left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right) }$
A3. $\displaystyle{ \left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right) }$

We use the lemma $\displaystyle{ p \to p }$ proved here, which we refer to as (L1), and use the following additional lemma, proved here:

(L2) $\displaystyle{ p \to ((p \to q) \to q) }$

We first prove $\displaystyle{ \neg \neg p \to p }$. For shortness, we denote $\displaystyle{ q \to ( r \to q ) }$ by φ0. We also use repeatedly the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.

(1) $\displaystyle{ \varphi_0 }$       (instance of (A1))
(2) $\displaystyle{ (\neg \neg \varphi_0 \to \neg \neg p ) \to (\neg p \to \neg \varphi_0) }$       (instance of (A3))
(3) $\displaystyle{ (\neg p \to \neg \varphi_0) \to (\varphi_0 \to p ) }$       (instance of (A3))
(4) $\displaystyle{ (\neg \neg \varphi_0 \to \neg \neg p ) \to (\varphi_0 \to p ) }$       (from (2) and (3) by the hypothetical syllogism metatheorem)
(5) $\displaystyle{ \neg \neg p \to ( \neg \neg \varphi_0 \to \neg \neg p ) }$       (instance of (A1))
(6) $\displaystyle{ \neg \neg p \to (\varphi_0 \to p ) }$       (from (4) and (5) by the hypothetical syllogism metatheorem)
(7) $\displaystyle{ \varphi_0 \to ((\varphi_0 \to p) \to p) }$       (instance of (L2))
(8) $\displaystyle{ (\varphi_0 \to p) \to p }$       (from (1) and (7) by modus ponens)
(9) $\displaystyle{ \neg \neg p \to p }$       (from (6) and (8) by the hypothetical syllogism metatheorem)

We now prove $\displaystyle{ p \to \neg \neg p }$.

(1) $\displaystyle{ \neg\neg\neg p \to \neg p }$       (instance of the first part of the theorem we have just proven)
(2) $\displaystyle{ (\neg\neg\neg p \to \neg p) \to (p \to \neg\neg p) }$       (instance of (A3))
(3) $\displaystyle{ p \to \neg \neg p }$       (from (1) and (2) by modus ponens)

And the proof is complete.