Double 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{\ast }\mathbf{4}\cdot \mathbf{13}.⊢.p\equiv \sim (\sim 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 \mathrm{\neg }}$${\displaystyle \mathrm{\neg }}$P

and the double negation elimination rule is:

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

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⊢\mathrm{\neg }\mathrm{\neg }P}$$

The double negation elimination rule may be written as: $${\displaystyle \mathrm{\neg }\mathrm{\neg }P⊢P}$$

In rule form: $${\displaystyle \frac{P}{\mathrm{\neg }\mathrm{\neg }P}}$$ and $${\displaystyle \frac{\mathrm{\neg }\mathrm{\neg }P}{P}}$$

or as a tautology (plain propositional calculus sentence): $${\displaystyle P\to \mathrm{\neg }\mathrm{\neg }P}$$ and $${\displaystyle \mathrm{\neg }\mathrm{\neg }P\to P}$$

These can be combined into a single biconditional formula: $${\displaystyle \mathrm{\neg }\mathrm{\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 \mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A⊢\mathrm{\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.