Database: Disjunctive syllogism

Theorem 95: Disjunctive syllogism (inference rules)

(a) Given that the disjunction \phi \vee \psi holds and that the negation \neg \phi holds, we may infer that \psi holds: \cfrac{\vdash (\phi \vee \psi) \quad \vdash \neg \phi}{\vdash \psi}. (b) Given that \phi \vee \psi holds and \neg \psi holds, we may infer that \phi holds: \cfrac{\vdash (\phi \vee \psi) \quad \vdash \neg \psi}{\vdash \phi}.

Proof: (a): By negation elimination, we infer that \phi entails \psi . By the identity rule, \psi entails \psi . Thus, by disjunction elimination, \psi holds.

(b): By commutativity of disjunction, \psi \vee \phi holds. By (a), \phi holds. \square

This database entry builds on the following:

  1. Definition: Negation
  2. Definition: Disjunction
  3. Terminology: Entailment
  4. Terminology: Inference rule
  5. Theorem: The identity rule
  6. Theorem: Negation elimination
  7. Theorem: Disjunction elimination
  8. Proposition: Commutativity of disjunction