Formal knowledge
Law of excluded middle
The principle that P or not P holds for every proposition P.
Definition
Law of excluded middle
The law of excluded middle states that every proposition is true or its negation is true.
Classical logic accepts the law for arbitrary propositions. Constructive systems accept it for decidable propositions but do not derive the unrestricted form from the core rules.
Notation P ∨ ¬P
01
Example
For equality of two natural numbers, a program can decide which side holds, so excluded middle is constructively available for that proposition.
02
Important distinction
The law does not provide a practical decision procedure for an arbitrary mathematical statement.
After reading this article, you should be able to
- Define Law of excluded middle in the sense used on this site.
- Explain why decidable instances of excluded middle differ from the unrestricted axiom.