---
tag: 0NFAGWH84K
kind: statement
role: theorem
name: Double negation law
aliases: [double-negation-elimination]
msc: [03B05]
uses: [0XR7A7RSXB, 06GYGS41JK]
sources:
  - url: https://en.wikipedia.org/wiki/Double_negation
    locator: lead section
same_as:
  wikidata: Q5300067
  wikipedia: Double negation
---

## Statement

In classical logic, for each [[proposition|0ZGC7ZESYN]] $p$, the proposition $\neg \neg p$ is [[logically equivalent|06GYGS41JK]] to $p$.
$$\neg \neg p \equiv p$$

## Remarks

The implication $p \to \neg \neg p$ is also valid in intuitionistic logic.
The other direction, $\neg \neg p \to p$, needs classical logic.
This direction is the basis of [[proof by contradiction|0J0XBKG64S]].

## Explanations

### L1 human

"It is not true that $5$ is not prime" says the same as "$5$ is prime".
Two negations cancel each other.