Mathematical logic and foundations Constructive mathematics Theorem
Law of excluded middle
Builds on DisjunctionNegation
Statement
In classical logic, for each proposition , the proposition is true.
Remarks
The formula is a tautology. Some systems take the law as an axiom. Intuitionistic logic does not accept the law in general. The law is the basis of proof by cases on and .
Reading path
To understand this page from the ground up, read these 4 pages in order. The foundations come first.
Show the path as a graph
- no evidence level
- Proposition concept
- Disjunction definition
- Negation definition
- Law of excluded middle statement
Where this leads
15 pages build on this one.
- Brouwer–Heyting–Kolmogorov interpretation
- Realizability
- Intuitionistic logic
- Diaconescu's theorem
- Brouwer–Heyting–Kolmogorov interpretation
- Constructive analysis
- Cut-elimination theorem
- Realizability
- Constructivism
- Constructivism
- Constructive analysis
- Sequent calculus
- Double-negation translation
- Heyting arithmetic
- Dialectica interpretation
Further reading
- Web https://en.wikipedia.org/wiki/Law_of_excluded_middle, lead section
About this page
| Tag | 0RYYK8PG4S |
|---|---|
| URI | m2://0RYYK8PG4S |
| Aliases | excluded-middle, tertium-non-datur |
| Kind | statement, theorem |
| Writing | W1 stated |
| MSC | 03B05 |
| Status | This copy of the site has no build data. Run m2 status 0RYYK8PG4S. |
| Uses | Disjunction, Negation |
| Same as |
Markdown · JSON · Edit on GitHub
What this page needs for W2
- edge about out: the concepts that the statement is about (0 of 1)
- edge proves in: at least one proof node (0 of 1)
- edge instance_of or illustrates in: one example that shows the statement at work (0 of 1)
- explanation L2 (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.
What links here
Used by
- Intuitionistic logic
- Diaconescu's theorem
- Constructive analysis
- Constructivism
- Constructivism
- Sequent calculus
- Double-negation translation
- Heyting arithmetic