Database: Law of Excluded Middle

Theorem 82: 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 [81], the conjunction \neg \phi \wedge \neg \neg \phi holds. Thus, \neg (\phi \vee \neg \phi) entails this conjunction. But \neg (\neg \phi \wedge \neg \neg \phi) holds by the Law of Noncontradiction; using weakening, \neg (\phi \vee \neg \phi) entails this negation. By negation introduction, we can therefore infer that \neg \neg (\phi \vee \neg \phi) holds. We conclude using double negation elimination 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