Double negation elimination

Template:Transformation rules

For the theorem of propositional logic based on the same concept, see double negation.

In propositional logic, double negative elimination (also called double negation elimination, double negative introduction, double negation introduction, or simply double negation[1][2][3]) are two valid rules of replacement. They are the inferences that if A is true, then not not-A is true and its converse, that, if not not-A 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 \Leftrightarrow ¬¬P

and the double negation elimination rule is:

¬¬P \Leftrightarrow P

Where "\Leftrightarrow" 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:

P \vdash \neg \neg P

The double negation elimination rule may be written as:

\neg \neg P \vdash P

In rule form:

\frac{P}{\neg \neg P}


\frac{\neg \neg P}{P}

or as a tautology (plain propositional calculus sentence):

P \to \neg \neg P


\neg \neg P \to P

These can be combined together into a single biconditional formula:

\neg \neg P \leftrightarrow P .

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.

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

  • Gödel–Gentzen negative translation


This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.