Double negation

Type	Theorem
Field	Propositional calculus Classical logic
Statement	If a statement is true, then it is not the case that the statement is not true, and vice versa."
Symbolic statement	${\displaystyle A\equiv \sim (\sim A)}$

Inpropositional logic, thedouble negation of a statement states that "it is not the case that the statement is not true". Inclassical logic, every statement islogically equivalent to its double negation, but this is not true inintuitionistic logic; this can be expressed by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign~ expressesnegation.

Like thelaw of the excluded middle, this principle is considered to be alaw of thought in classical logic,^[1] but it is disallowed byintuitionistic logic.^[2] The principle was stated as a theorem ofpropositional logic byRussell andWhitehead inPrincipia Mathematica as:

${\displaystyle \mathbf{\ast }\mathbf{4}\cdot \mathbf{13}.⊢.p\equiv \sim (\sim p)}$^[3]

"This is the principle of double negation,i.e. a proposition is equivalent of the falsehood of its negation."

Double negation elimination anddouble negation introduction are twovalidrules of replacement. They are theinferences that, ifnot not-A is true, thenA is true, and itsconverse, that, ifA is true, thennot not-A is true, respectively. The rule allows one to introduce or eliminate anegation from aformal proof. The rule is based on the equivalence of, for example,It is false that it is not raining. andIt is raining.

Thedouble negation introduction rule is:

P${\displaystyle \Rightarrow }$${\displaystyle \mathrm{\neg }}$${\displaystyle \mathrm{\neg }}$P

and thedouble negation elimination rule is:

${\displaystyle \mathrm{\neg }}$${\displaystyle \mathrm{\neg }}$P${\displaystyle \Rightarrow }$ P

Where "${\displaystyle \Rightarrow }$" is ametalogicalsymbol representing "can be replaced in a proof with."

In logics that have both rules, negation is aninvolution.

Thedouble negation introduction rule may be written insequent notation:

${\displaystyle P⊢\mathrm{\neg }\mathrm{\neg }P}$

Thedouble negation elimination rule may be written as:

${\displaystyle \mathrm{\neg }\mathrm{\neg }P⊢P}$

Inrule form:

${\displaystyle \frac{P}{\mathrm{\neg }\mathrm{\neg }P}}$

and

${\displaystyle \frac{\mathrm{\neg }\mathrm{\neg }P}{P}}$

or as atautology (plain propositional calculus sentence):

${\displaystyle P\to \mathrm{\neg }\mathrm{\neg }P}$

and

${\displaystyle \mathrm{\neg }\mathrm{\neg }P\to P}$

These can be combined into a single biconditional formula:

${\displaystyle \mathrm{\neg }\mathrm{\neg }P\leftrightarrow P}$.

Since biconditionality is anequivalence relation, any instance of ¬¬A in awell-formed formula can be replaced byA, leaving unchanged thetruth-value of the well-formed formula.

Double negative elimination is a theorem ofclassical logic, but not of weaker logics such asintuitionistic logic andminimal logic. Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is${\displaystyle \mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A⊢\mathrm{\neg }A}$.

Because of their constructive character, a statement such asIt's not the case that it's not raining is weaker thanIt'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 oflitotes.

InHilbert-style deductive systems for propositional logic, double negation is not always taken as an axiom (seelist of Hilbert systems), and is rather a theorem. We describe a proof of this theorem in the system of three axioms proposed byJan Łukasiewicz:

A1.${\displaystyle \varphi \to \left(\psi \to \varphi \right)}$

A2.${\displaystyle \left(\varphi \to \left(\psi \to \xi \right)\right)\to \left(\left(\varphi \to \psi \right)\to \left(\varphi \to \xi \right)\right)}$

A3.${\displaystyle \left(\mathrm{\neg }\varphi \to \mathrm{\neg }\psi \right)\to \left(\psi \to \varphi \right)}$

We use the lemma${\displaystyle p\to p}$ provedhere, which we refer to as (L1), and use the following additional lemma, provedhere:

(L2)${\displaystyle p\to ((p\to q)\to q)}$

We first prove${\displaystyle \mathrm{\neg }\mathrm{\neg }p\to p}$. For shortness, we denote${\displaystyle q\to (r\to q)}$ by φ₀. We also use repeatedly the method of thehypothetical syllogism metatheorem as a shorthand for several proof steps.

(1)${\displaystyle {\phi }_0}$       (instance of (A1))

(2)${\displaystyle (\mathrm{\neg }\mathrm{\neg }{\phi }_0\to \mathrm{\neg }\mathrm{\neg }p)\to (\mathrm{\neg }p\to \mathrm{\neg }{\phi }_0)}$       (instance of (A3))

(3)${\displaystyle (\mathrm{\neg }p\to \mathrm{\neg }{\phi }_0)\to ({\phi }_0\to p)}$       (instance of (A3))

(4)${\displaystyle (\mathrm{\neg }\mathrm{\neg }{\phi }_0\to \mathrm{\neg }\mathrm{\neg }p)\to ({\phi }_0\to p)}$       (from (2) and (3) by the hypothetical syllogism metatheorem)

(5)${\displaystyle \mathrm{\neg }\mathrm{\neg }p\to (\mathrm{\neg }\mathrm{\neg }{\phi }_0\to \mathrm{\neg }\mathrm{\neg }p)}$       (instance of (A1))

(6)${\displaystyle \mathrm{\neg }\mathrm{\neg }p\to ({\phi }_0\to p)}$       (from (4) and (5) by the hypothetical syllogism metatheorem)

(7)${\displaystyle {\phi }_0\to (({\phi }_0\to p)\to p)}$       (instance of (L2))

(8)${\displaystyle ({\phi }_0\to p)\to p}$       (from (1) and (7) by modus ponens)

(9)${\displaystyle \mathrm{\neg }\mathrm{\neg }p\to p}$       (from (6) and (8) by the hypothetical syllogism metatheorem)

We now prove${\displaystyle p\to \mathrm{\neg }\mathrm{\neg }p}$.

(1)${\displaystyle \mathrm{\neg }\mathrm{\neg }\mathrm{\neg }p\to \mathrm{\neg }p}$       (instance of the first part of the theorem we have just proven)

(2)${\displaystyle (\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }p\to \mathrm{\neg }p)\to (p\to \mathrm{\neg }\mathrm{\neg }p)}$       (instance of (A3))

(3)${\displaystyle p\to \mathrm{\neg }\mathrm{\neg }p}$       (from (1) and (2) by modus ponens)

And the proof is complete.

• Gödel–Gentzen negative translation

• William Hamilton, 1860,Lectures on Metaphysics and Logic, Vol. II. Logic; Edited by Henry Mansel and John Veitch, Boston, Gould and Lincoln.
• Christoph Sigwart, 1895,Logic: The Judgment, Concept, and Inference; Second Edition, Translated by Helen Dendy, Macmillan & Co. New York.
• Stephen C. Kleene, 1952,Introduction to Metamathematics, 6th reprinting with corrections 1971, North-Holland Publishing Company, Amsterdam NY,ISBN 0-7204-2103-9.
• Stephen C. Kleene, 1967,Mathematical Logic, Dover edition 2002, Dover Publications, Inc, Mineola N.Y.ISBN 0-486-42533-9
• Alfred North Whitehead andBertrand Russell,Principia Mathematica to *56, 2nd edition 1927, reprint 1962, Cambridge at the University Press.

• Theorems in propositional logic
• Classical logic
• Rules of inference

• Articles with short description
• Short description is different from Wikidata