Double negative elimination

related topics
{math, number, function}
{island, water, area}

In propositional logic, the inference rules double negative elimination (also called double negation elimination, double negative introduction, double negation introduction, or simply double negation) allow deriving the double negative equivalent by adding (for double negative introduction) or removing (for double negative elimination) a pair of negation signs. This is based on the equivalence of, for example,


Formally, the rule of double negative elimination is

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

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

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

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

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 (AC)C (where AC represents the complement of A) are the same.

See also

Full article ▸

related documents
Borel-Cantelli lemma
Weierstrass–Casorati theorem
Hash collision
Nowhere dense set
Magma computer algebra system
Category (mathematics)
Dyadic rational
Calculus with polynomials
Stirling number
Algebraic number
T1 space
Cayley's theorem
Malleability (cryptography)
Real line
Regular space
Steiner system
Alternative algebra
Byte-order mark
Partial fractions in integration
Atlas Autocode
Algebraic extension
Residue (complex analysis)
GNU Octave
Euler's criterion
Decision problem
Whittaker–Shannon interpolation formula