Database: Idempotence of disjunction

Proposition 78: Forward idempotence of disjunction (inference rule)

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

Proof: (a): Since we have as a premise that \phi holds, the desired inference is made using disjunction introduction.

(b): By the identity rule, \phi entails \phi . But we have (\phi \vee \phi) as a premise, so we may infer by disjunction elimination that \phi holds. \square

This database entry builds on the following:

  1. Definition: Disjunction
  2. Terminology: Inference, entailment
  3. Terminology: Inference rule
  4. Theorem: The identity rule
  5. Theorem: Disjunction introduction
  6. Theorem: Disjunction elimination