Double negative elimination

Transformation rules
Propositional calculus
Rules of inference Modus ponens Modus tollens Modus ponendo tollens Biconditional introduction Biconditional elimination Conjunction introduction Simplification Disjunction introduction Disjunction elimination Disjunctive syllogism Hypothetical syllogism Constructive dilemma Destructive dilemma Absorption Rules of replacement Associativity Commutativity Distributivity Double negation De Morgan's laws Transposition Material implication Exportation Tautology
Predicate logic
Universal generalization Universal instantiation Existential generalization Existential instantiation

In propositional logic, double negative elimination (also called double negation elimination, double negative introduction, double negation introduction, or simply double negation) is a valid rule of replacement. It is the inference that if A is true, then not not-A is true. The rule also refers to the 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.

Formally, the rule of double negative elimination is

$\frac{\neg\neg A}{\therefore A}.$

The rule of double negative introduction states the converse, that double negatives can be added without changing the meaning of a proposition. Formally, the rule of double negative introduction is

$\frac A{\therefore\neg\neg A}.$

These two rules — double negative elimination and introduction — can be restated as follows (in sequent notation):

$\neg \neg A \vdash A$,

$A \vdash \neg \neg A$.

Applying the deduction theorem to each of these two inference rules produces the pair of valid conditional formulas

$\vdash \neg \neg A \rightarrow A$,

$\vdash A \rightarrow \neg \neg A$,

which can be combined together into a single biconditional formula

$\neg \neg A \leftrightarrow A$.

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 $\neg \neg \neg A \vdash \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

• Negation
• Gödel–Gentzen negative translation