Double negation
Transformation rules 

Propositional calculus 
Rules of inference 
Rules of replacement 

Predicate logic 
In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition A is logically equivalent to not (notA), or by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign ~ expresses negation.^{}
Like the law of the excluded middle, this principle is considered to be a law of thought in classical logic,^{} but it is disallowed by intuitionistic logic.^{} The principle was stated as a theorem of propositional logic by Russell and Whitehead in Principia Mathematica as:

 ^{}
 "This is the principle of double negation, i.e. a proposition is equivalent of the falsehood of its negation."
This section may be confusing or unclear to readers. In particular, the following part of the lead is extremely difficult to read. (July 2015) 
The principium contradictiones of modern logicians (particularly Leibnitz and Kant) in the formula A is not notA, differs entirely in meaning and application from the Aristotelian proposition [ i.e. Law of Contradiction: not (A and notA) i.e. ~(A & ~A), or not (( B is A) and (B is notA))]. This latter refers to the relation between an affirmative and a negative judgment.
According to Aristotle, one judgment [B is judged to be an A] contradicts another [B is judged to be a notA]. The later proposition [ A is not notA ] refers to the relation between subject and predicate in a single judgment; the predicate contradicts the subject. Aristotle states that one judgment is false when another is true; the later writers [Leibniz and Kant] state that a judgment is in itself and absolutely false, because the predicate contradicts the subject. What the later writers desire is a principle from which it can be known whether certain propositions are in themselves true. From the Aristotelian proposition we cannot immediately infer the truth or falsehood of any particular proposition, but only the impossibility of believing both affirmation and negation at the same time.^{}
Double negative elimination
Double negative elimination (also called double negation elimination, double negative introduction, double negation introduction, double negation, or negation elimination^{}^{}^{}) are two valid rules of replacement. They are the inferences that if A is true, then not notA is true and its converse, that, if not notA 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.
The double negation introduction rule is:
 P ¬¬P
and the double negation elimination rule is:
 ¬¬P P
Where "" is a metalogical symbol representing "can be replaced in a proof with."
Formal notation
The double negation introduction rule may be written in sequent notation:
The double negation elimination rule may be written as:
In rule form:
and
or as a tautology (plain propositional calculus sentence):
and
These can be combined together into a single biconditional formula:
 .
Since biconditionality is an equivalence relation, any instance of ¬¬A in a wellformed formula can be replaced by A, leaving unchanged the truthvalue of the wellformed 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 character, 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 .
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
 Gödel–Gentzen negative translation
References
Bibliography
 William Hamilton, 1860, Lectures on Metaphysics and Logic, Vol. II. Logic; Edited by Henry Mansel and John Veitch, Boston, Gould and Lincoln. Available online from googlebooks.
 Christoph Sigwart, 1895, Logic: The Judgment, Concept, and Inference; Second Edition, Translated by Helen Dendy, Macmillan & Co. New York. Available online from googlebooks.
 Stephen C. Kleene, 1952, Introduction to Metamathematics, 6th reprinting with corrections 1971, NorthHolland Publishing Company, Amsterdam NY, ISBN 0 7204 2103 9.
 Stephen C. Kleene, 1967, Mathematical Logic, Dover edition 2002, Dover Publicastions, Inc, Mineola N.Y. ISBN 0486425339 (pbk.)
 Alfred North Whitehead and Bertrand Russell, Principia Mathematica to *56, 2nd edition 1927, reprint 1962, Cambridge at the University Press, London UK, no ISBN or LCCCN.