# Double negation

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:

$\mathbf {*4\cdot 13} .\ \ \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 A is true, then not not-A is true and its converse, that, if not not-A is true, then A is true. 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 $\Rightarrow$ $\neg$ $\neg$ P

and the double negation elimination rule is:

$\neg$ $\neg$ P $\Rightarrow$ P

Where "$\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:

$P\vdash \neg \neg P$ The double negation elimination rule may be written as:

$\neg \neg P\vdash P$ In rule form:

${\frac {P}{\neg \neg P}}$ and

${\frac {\neg \neg P}{P}}$ or as a tautology (plain propositional calculus sentence):

$P\to \neg \neg P$ and

$\neg \neg P\to P$ These can be combined together into a single biconditional formula:

$\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 $\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.