Double Negative Elimination - Formal Notation

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

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