Database: Disjunctive syllogism

Theorem 80: Disjunctive syllogism (inference rules)

(a) Given that the disjunction \phi \vee \psi holds and 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 the disjunction \phi \vee \psi holds and the negation \neg \phi holds, we may infer that \psi 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: Inference, entailment
  4. Terminology: Inference rule
  5. Theorem: The identity rule
  6. Theorem: Negation elimination
  7. Theorem: Disjunction elimination
  8. Proposition: Commutativity of disjunction