Like the law of the excluded middle, this principle is considered to be a law of thought in classical logic,[1] but it is disallowed by intuitionistic logic.

[2] The principle was stated as a theorem of propositional logic by Russell and Whitehead in Principia Mathematica as: Double negation elimination and double negation introduction are two valid rules of replacement.

The rule allows one to introduce or eliminate a negation from a formal proof.

The rule is based on the equivalence of, for example, It is false that it is not raining.

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 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 well-formed formula.

This distinction also arises in natural language in the form of litotes.

We describe a proof of this theorem in the system of three axioms proposed by Jan Łukasiewicz: We use the lemma

We also use repeatedly the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.