\ Glossary Excluded middle | Logic Notes - ANU

THE LOGIC NOTES

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

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:
  ⊢   p OR NOTp ⊢ OR   ⊢   p,  NOTp ⊢ NOT p   ⊢   p

Links