// laws and rules · Fundamental law
Double negation law_
Double negation states that negating a proposition twice returns the original proposition. It is one of the simplest laws of classical logic and, at the same time, one of the most debated: intuitionistic logic rejects it precisely because of its philosophical consequences.
Example
¬¬p ⇔ p
What the variables mean
- ▸ p: “The train arrived on time”
In plain words
“It is not true that the train did not arrive on time” is equivalent to “the train arrived on time”.
Truth table
| p | ¬p | ¬¬p | ¬¬p ⇔ p★ |
|---|---|---|---|
| T | F | T | T |
| F | T | F | T |
Classification: Tautology · 2 rows
Statement
The law states that ¬¬p ≡ p. With a single variable the table has two rows, and both sides agree in each, so the biconditional is a tautology.
It says that negation is an involution: applying it twice is the same as not applying it at all. In set terms, the complement of the complement of a set is the original set.
Why it holds: reading the table
Row 1 (p = T): ¬p is F and ¬¬p is T again, matching p. Row 2 (p = F): ¬p is T and ¬¬p is F, which also matches.
The reasoning rests on the principle of bivalence: in classical logic every proposition is either true or false with nothing in between, so ruling out falsity amounts to asserting truth.
How it is used
It is a mandatory clean-up step after applying De Morgan's laws, which tend to produce nested negations. Without it, formulas would grow without bound.
It also underpins proof by contradiction in its classical form: if assuming ¬p leads to a contradiction, you conclude ¬¬p and, by this law, p.
Examples
Everyday: “it is not false that I will pass” simply means “I will pass”. In natural language, though, double negation is sometimes used to hedge (“not bad” is not exactly “good”), which never happens in formal logic.
Programming: `!!value` in JavaScript is a common idiom to coerce anything to a boolean, and `!(!active)` is just `active`.
Intuitionistic logic
In intuitionistic logic, where proving something requires constructing it, ¬¬p ⇒ p is not accepted in general: knowing that non-existence is impossible is not enough to exhibit an example.
The other direction, p ⇒ ¬¬p, is accepted in both systems. This asymmetry is what separates classical from constructive logic and is closely related to the rejection of excluded middle.
Try it yourself
Edit the expression in the calculator and watch how every step of the table changes.
Open in the calculator →Related operators
Frequently asked questions
Do three negations equal one? ▼
Yes: ¬¬¬p ≡ ¬p. Negations cancel in pairs, so an even number equals none and an odd number equals a single one.
Why does intuitionistic logic reject it? ▼
Because it demands that a proof construct the asserted object. Ruling out that p is impossible does not construct p, so ¬¬p is not enough to conclude p.
Is it used when applying De Morgan? ▼
Constantly: pushing a negation across a conjunction or disjunction produces double negations that this law removes.