Excluded Middle Glossary
Definition
The "law" of the excluded middle is the logical principle amounting to the bivalence of truth: that every proposition is either true or false.
Formally, the expression of this principle is the theorem:
⊢ p OR NOTp
Comments
It is easy to see that any formula of the form A OR NOTA is a tautology: if A is true for an interpretation then the disjunction is true, while if A if false then its negation NOTA is true and so again the disjunction is true. Either way, the disjunction is true, so it holds on every interpretation.
It is a little harder to find a proof in the natural deduction calculus. Here is the simplest proof:
SP {⊢ p OR NOTp} PL {1} {1} {NOT(p OR NOTp)} {A} PL {2} {2} {p} {A} PL {2} {3} {p OR NOTp} {2 ORI} PL {1} {4} {NOTp} {1, 3 [2] RAA} PL {1} {5} {p OR NOTp} {4 ORI} PL { } {6} {NOTNOT(p OR NOTp)} {1, 5 [1] RAA} PL { } {7} {p OR NOTp} {6 NOTNOTE} EPThis proof is fine in relevant logic, but it is not accepted in fuzzy logic, because there is an implicit contraction at line 6. It is also not a correct proof in intuitionistic logic because of the double negation elimination move at the end.
By contrast, the sequent calculus proof is delightfully simple: