# Double negative elimination

Template:Transformation rules {{ safesubst:#invoke:Unsubst||$N=Merge to |date=__DATE__ |$B= Template:MboxTemplate:DMCTemplate:Merge partner }}

*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**, **double negation**, or **negation elimination**^{[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:

and the *double negation elimination* rule is:

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

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

In rule form:

and

or as a tautology (plain propositional calculus sentence):

and

These can be combined together into a single biconditional formula:

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 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.) Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is .

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

## References

- ↑ Copi and CohenTemplate:Full
- ↑ Moore and ParkerTemplate:Full
- ↑ HurleyTemplate:Full