Double negation | |
Type: | Theorem |
Statement: | If a statement is true, then it is not the case that the statement is not true, and vice versa." |
Symbolic Statement: | A\equiv\sim(\simA) |
In propositional logic, the double negation of a statement states that "it is not the case that the statement is not true". In classical logic, every statement is logically equivalent to its double negation, but this is not true in intuitionistic logic; this can be expressed 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,[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:
*4 ⋅ 13. \vdash. p \equiv \thicksim(\thicksimp)
"This is the principle of double negation, i.e. a proposition is equivalent of the falsehood of its negation."
Elimination and introductionThe double negation introduction rule is:
P
⇒
P
⇒
Where "
⇒
In logics that have both rules, negation is an involution.
The double negation introduction rule may be written in sequent notation:
P\vdash\neg\negP
The double negation elimination rule may be written as:
\neg\negP\vdashP
In rule form:
P | |
\neg\negP |
\neg\negP | |
P |
or as a tautology (plain propositional calculus sentence):
P\to\neg\negP
\neg\negP\toP
These can be combined into a single biconditional formula:
\neg\negP\leftrightarrowP
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. Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is
\neg\neg\negA\vdash\negA
In Hilbert-style deductive systems for propositional logic, double negation is not always taken as an axiom (see list of Hilbert systems), and is rather a theorem. We describe a proof of this theorem in the system of three axioms proposed by Jan Łukasiewicz:
A1.
\phi\to\left(\psi\to\phi\right)
A2.
\left(\phi\to\left(\psi → \xi\right)\right)\to\left(\left(\phi\to\psi\right)\to\left(\phi\to\xi\right)\right)
A3.
\left(lnot\phi\tolnot\psi\right)\to\left(\psi\to\phi\right)
We use the lemma
p\top
(L2)
p\to((p\toq)\toq)
We first prove
\neg\negp\top
q\to(r\toq)
(1)
\varphi0
(2)
(\neg\neg\varphi0\to\neg\negp)\to(\negp\to\neg\varphi0)
(3)
(\negp\to\neg\varphi0)\to(\varphi0\top)
(4)
(\neg\neg\varphi0\to\neg\negp)\to(\varphi0\top)
(5)
\neg\negp\to(\neg\neg\varphi0\to\neg\negp)
(6)
\neg\negp\to(\varphi0\top)
(7)
\varphi0\to((\varphi0\top)\top)
(8)
(\varphi0\top)\top
(9)
\neg\negp\top
We now prove
p\to\neg\negp
(1)
\neg\neg\negp\to\negp
(2)
(\neg\neg\negp\to\negp)\to(p\to\neg\negp)
(3)
p\to\neg\negp
And the proof is complete.