Mathematical logic and foundations Theorem
Double negation law
Builds on NegationLogical equivalence
Statement
In classical logic, for each proposition , the proposition is logically equivalent to .
Remarks
The implication is also valid in intuitionistic logic. The other direction, , needs classical logic. This direction is the basis of proof by contradiction.
Reading path
To understand this page from the ground up, read these 11 pages in order. The foundations come first.
Show the path as a graph
- no evidence level
- Proposition concept
- Conjunction definition
- Disjunction definition
- Implication definition
- Negation definition
- Biconditional definition
- Truth table concept
- Propositional logic concept
- Tautology definition
- Logical equivalence definition
- Double negation law statement
Where this leads
29 pages build on this one.
- Russell's paradox
- Proof by contradiction
- Brouwer–Heyting–Kolmogorov interpretation
- Type theory
- Realizability
- Naive set theory
- Constructible universe
- Brouwer–Heyting–Kolmogorov interpretation
- Constructive analysis
- Curry–Howard correspondence
- Realizability
- Homotopy type theory
- Intuitionistic type theory
- Constructivism
- Constructivism
- Zero sharp
- Constructive analysis
- Homotopy type theory
- Von Neumann–Bernays–Gödel set theory
- Intuitionistic type theory
- Axiom of constructibility
- Type theory
- Gödel's consistency of CH and AC
- Jensen's covering theorem
- Von Neumann–Bernays–Gödel set theory
- Class
- Inner model
- Naive set theory
- Class
Further reading
- Web https://en.wikipedia.org/wiki/Double_negation, lead section
About this page
| Tag | 0NFAGWH84K |
|---|---|
| URI | m2://0NFAGWH84K |
| Aliases | double-negation-elimination |
| Kind | statement, theorem |
| Writing | W0 stub |
| MSC | 03B05 |
| Status | This copy of the site has no build data. Run m2 status 0NFAGWH84K. |
| Uses | Negation, Logical equivalence |
| Same as |
Markdown · JSON · Edit on GitHub
What this page needs for W1
- an inventory row: the row of the inventory that the node accounts for (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.