### Double negative elimination

Template:Transformation rules

It has been suggested that this article be merged into Double negation. (Discuss) Proposed since March 2012. |

*For the theorem of propositional logic based on the same concept, see double negation*.

In propositional logic, **double negative elimination** (also called **double negation elimination**, **double negative introduction**, **double negation introduction**, or simply **double negation**^{[1]}^{[2]}^{[3]}) 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 logical 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 $\backslash Leftrightarrow$ ¬¬P*

and the *double negation elimination* rule is:

*¬¬P $\backslash Leftrightarrow$ P*

Where "$\backslash Leftrightarrow$" is a metalogical symbol representing "can be replaced in a proof with."

## Formal notation

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

- $P\; \backslash vdash\; \backslash neg\; \backslash neg\; P$

The *double negation elimination* rule may be written as:

- $\backslash neg\; \backslash neg\; P\; \backslash vdash\; P$

In rule form:

- $\backslash frac\{P\}\{\backslash neg\; \backslash neg\; P\}$

and

- $\backslash frac\{\backslash neg\; \backslash neg\; P\}\{P\}$

or as a tautology (plain propositional calculus sentence):

- $P\; \backslash to\; \backslash neg\; \backslash neg\; P$

and

- $\backslash neg\; \backslash neg\; P\; \backslash to\; P$

These can be combined together into a single biconditional formula:

- $\backslash neg\; \backslash neg\; P\; \backslash 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. Because of their constructive flavor, 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.) Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is $\backslash neg\; \backslash neg\; \backslash neg\; A\; \backslash vdash\; \backslash neg\; A$.

In set theory also we have the negation operation of the complement which obeys this property: a set A and a set (A^{C})^{C} (where A^{C} represents the complement of A) are the same.

## See also

- Gödel–Gentzen negative translation