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 ∨ ¬p

Comments

It is easy to see that any formula of the form A ∨ ¬A 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} EP

⊢   p ∨ ¬p

α1 (1) ¬(p ∨ ¬p) A α2 (2) p A α2 (3) p ∨ ¬p 2 ∨I α1 (4) ¬p 1, 3 [α2] RAA α1 (5) p ∨ ¬p 4 ∨I (6) ¬¬(p ∨ ¬p) 1, 5 [α1] RAA (7) p ∨ ¬p 6 ¬¬E

This 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:

Links

• Negation
• A constructive view of truth