Double negative elimination - Definition and Overview

In logic and the propositional calculus, double negative elimination is a rule that states that double negatives can be removed from a proposition without changing its meaning:

It's not the case that it's not raining.

means the same as:

It's raining.

Formally:

  ¬ ¬ A
  ∴ A

Also:

  ¬ ¬ ¬ A
  ∴ ¬ A

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

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

<math> \neg \neg A \vdash A <math>,

<math> A \vdash \neg \neg A <math>.

Applying the Deduction Theorem to each of these two inference rules produces the pair of valid conditional formulas

<math> \vdash \neg \neg A \rightarrow A <math>,

<math> \vdash A \rightarrow \neg \neg A <math>,

which can be combined together into a single biconditional formula

<math> \neg \neg A \leftrightarrow A <math>.

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

The double negative elimination rule is true in classical logic, but in intuitionistic logic, the statement, It's not the case that it's not raining is weaker than It's raining, and the rule is not true. As a slightly clearer example, It's not unreasonable is slightly less direct than It's reasonable. On the other hand, double negative introduction is also true in intuitionistic logic.

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.