Law of Excluded Middle/Proof Rule

From ProofWiki
Jump to navigation Jump to search

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}$      


The law of (the) excluded middle can be expressed in natural language as:

Every statement is either true or false.

This is one of the Aristotelian principles upon which rests the whole of classical logic, and the majority of mainstream mathematics.

Also known as

The law of (the) excluded middle is otherwise known as:

Also see

Technical Note

When invoking Law of Excluded Middle in a tableau proof, use the {{ExcludedMiddle}} template:





line is the number of the line on the tableau proof where the Law of Excluded Middle is to be invoked
statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters
comment is the (optional) comment that is to be displayed in the Notes column.