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: Logic (from Classical Greek λόγος (logos), originally meaning the word, or what is spoken, but coming to mean thought or reason) is most often said to be the study of arguments, although the exact definition of logic is a matter of controversy amongst philosophers (see below). ... The propositional calculus is a formal deduction system whose atomic formulas are propositional variables. ... A double negative occurs when two or more ways to express negation are used in the same sentence. ...

It is not the case that it is not raining.

means the same as:

It is raining.

Formally:

 ¬ ¬ 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): In proof theory, a sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction. ...

,

.

Applying the Deduction Theorem to each of these two inference rules produces the pair of valid conditional formulas In mathematical logic, the deduction theorem states that if a conclusion can be inferred (by means of some inference rule) from a premise, then it is possible to assert that the premise implies the conclusion. ... In logic, especially in mathematical logic, a rule of inference is a scheme for constructing valid inferences. ...

,

,

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. In mathematics, an equivalence relation on a set X is a binary relation on X that is reflexive, symmetric and transitive, i. ...

Double negative elimination is a theorem of classical logic, but not intuitionistic logic. Because of the constructive flavor of intuitionistic logic, 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 intuitionistic logic, as is . Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. ... Intuitionistic logic, or constructivist logic, is the logic used in mathematical intuitionism and other forms of mathematical constructivism. ... In rhetoric, litotes is a figure of speech in which the speaker emphasizes the magnitude of a statement by denying its opposite. ...

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. Naive set theory1 is distinguished from axiomatic set theory by the fact that the former regards sets as collections of objects, called the elements or members of the set, whereas the latter regards sets only as that which satisfies certain axioms. ... In set theory and other branches of mathematics, two kinds of complements are defined, the relative complement and the absolute complement. ...