Law of Excluded Middle/Proof Rule
Proof Rule
The law of (the) excluded middle is a valid argument in certain types of logic dealing with disjunction $\lor$ and negation $\neg$.
This includes classical propositional logic and predicate logic, and in particular natural deduction, but for example not intuitionistic propositional logic.
As a proof rule it is expressed in the form:
- $\phi \lor \neg \phi$ for all statements $\phi$.
It can be written:
- $\ds {{} \over \phi \lor \neg \phi} \textrm{LEM} \qquad \text { or } \qquad {\top \over \phi \lor \neg \phi} \textrm{LEM}$
where the symbol $\top$ (top) signifies tautology.
Tableau Form
Let $\phi$ be a well-formed formula.
The Law of Excluded Middle is invoked in the following manner:
Pool: | None | ||||||||
Formula: | $\phi \lor \neg \phi$ | ||||||||
Description: | Law of Excluded Middle | ||||||||
Depends on: | Nothing | ||||||||
Abbreviation: | $\text{LEM}$ |
Explanation
The law of (the) excluded middle can be expressed in natural language as:
This is one of the Aristotelian principles upon which rests the whole of classical logic, and the majority of mainstream mathematics.
The LEM is rejected by the intuitionistic school, which rejects the existence of an object unless it can be constructed within an axiomatic framework which does not include the LEM.
Also known as
The law of (the) excluded middle is otherwise known as:
- (Principium) tertium non datur, Latin for third not given, that is, a third possibility is not possible
- Principium tertii exclusi, Latin for the Principle of the Excluded Third (PET).
Also see
- This is a rule of inference of the following proof systems:
Technical Note
When invoking Law of Excluded Middle in a tableau proof, use the {{ExcludedMiddle}}
template:
{{ExcludedMiddle|line|statement}}
or:
{{ExcludedMiddle|line|statement|comment}}
where:
line
is the number of the line on the tableau proof where the Law of Excluded Middle is to be invokedstatement
is the statement of logic that is to be displayed in the Formula column, without the$ ... $
delimiterscomment
is the (optional) comment that is to be displayed in the Notes column.
Sources
- 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.2.2$: Derived rules