Database: Law of Excluded Middle

Theorem: Law of Excluded Middle (inference rule)

We may (from no premises at all) infer that the disjunction \phi \vee \neg \phi of \phi and its negation \neg \phi holds: \cfrac{}{\vdash (\phi \vee \neg \phi)}.

Proof: Assume \neg (\phi \vee \neg \phi) . By, (b) in [90], the conjunction \neg \phi \wedge \neg \neg \phi holds. Thus, \neg (\phi \vee \neg \phi) entails this conjunction.

We know by the Law of Noncontradiction that \neg (\neg \phi \wedge \neg \neg \phi) holds. Thus, by weakening, \neg (\phi \vee \neg \phi) entails this negation. Using negation introduction, we can therefore infer that \neg \neg (\phi \vee \neg \phi) holds. By double negation elimination, we conclude that \phi \vee \neg \phi holds. \square

This database entry builds on the following:

  1. Definition: Conjunction
  2. Definition: Negation
  3. Definition: Disjunction
  4. Terminology: Inference rule
  5. Theorem: The weakening rule
  6. Inference rule: Negation introduction
  7. Theorem: Law of Noncontradiction
  8. Inference rule: Double negation elimination
  9. Theorem: De Morgan’s laws for conjuncted negations and negated disjunctions