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

Double negative

A double negative occurs when two forms of negation are used in the same sentence. Multiple negation is the more general term referring to the occurrence of more than one negative in a clause....

 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,

It is false that it is not raining.

and

It is raining.

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

Sequent

In proof theory, a sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction. In the sequent calculus, the name sequent is used for the construct which can be regarded as a specific kind of judgment, characteristic to this deduction system.-...

 notation):
,
.

Applying the deduction theorem

Deduction theorem

In mathematical logic, the deduction theorem is a metatheorem of first-order logic. It is a formalization of the common proof technique in which an implication A → B is proved by assuming A and then proving B from this assumption. The deduction theorem explains why proofs of conditional...

 to each of these two inference rules

Rule of inference

In logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...

 produces the pair of valid conditional formulas
,
,

which can be combined together into a single biconditional formula
.

Since biconditionality is an equivalence relation

Equivalence relation

In mathematics, an equivalence relation is a relation that, loosely speaking, partitions a set so that every element of the set is a member of one and only one cell of the partition. Two elements of the set are considered equivalent if and only if they are elements of the same cell...

, any instance of ¬¬A in a well-formed formula

Well-formed formula

In mathematical logic, a well-formed formula, shortly wff, often simply formula, is a word which is part of a formal language...

 can be replaced by A, leaving unchanged the truth-value of the well-formed formula.

Double negative elimination is a theorem of classical logic

Classical logic

Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...

, but not of weaker logics such as intuitionistic logic

Intuitionistic logic

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...

 and minimal logic

Minimal logic

Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson. It is a variant of intuitionistic logic that rejects not only the classical law of excluded middle , but also the principle of explosion .Just like intuitionistic logic, minimal logic can be...

. 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

Litotes

In rhetoric, litotes is a figure of speech in which understatement is employed for rhetorical effect when an idea is expressed by a denial of its opposite, principally via double negatives....

.) Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is .

In set theory

Naive set theory

Naive set theory is one of several theories of sets used in the discussion of the foundations of mathematics. The informal content of this naive set theory supports both the aspects of mathematical sets familiar in discrete mathematics , and the everyday usage of set theory concepts in most...

 also we have the negation operation of the complement

Complement (set theory)

In set theory, a complement of a set A refers to things not in , A. The relative complement of A with respect to a set B, is the set of elements in B but not in A...

 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
  Negation
  In logic and mathematics, negation, also called logical complement, is an operation on propositions, truth values, or semantic values more generally. Intuitively, the negation of a proposition is true when that proposition is false, and vice versa. In classical logic negation is normally identified...
  
  
• Gödel–Gentzen negative translation
  Gödel–Gentzen negative translation
  In proof theory, the Gödel–Gentzen negative translation is a method for embedding classical first-order logic into intuitionistic first-order logic. It is one of a number of double-negation translations that are of importance to the metatheory of intuitionistic logic...