Database: Weakening of assumption

Proposition 60: Weakening of assumption (inference rule)

(a) Given that \phi entails \xi , we may infer the conjunction \phi \wedge \psi entails \xi: \cfrac{\phi \vdash \xi }{(\phi \wedge \psi) \vdash \xi }. (b) Given that \psi entails \xi , we may infer the conjunction \phi \wedge \psi entails \xi: \cfrac{\psi \vdash \xi }{(\phi \wedge \psi) \vdash \xi }.

Proof: (a): Assume \phi \wedge \xi . By conjunction elimination, infer \phi holds. Since \phi entails \xi , infer by the cut rule that \xi holds. Thus, \phi \wedge \psi entails \xi .

(b): By (a), infer \psi \wedge \phi entails \xi . By exchange, infer \phi \wedge \psi entails \xi . \square

This database entry builds on the following:

  1. Terminology: Inference, entailment
  2. Terminology: Inference rule
  3. Definition: Conjunction
  4. Inference rule: Conjunction elimination
  5. Theorem: The cut rule
  6. Theorem: The exchange rule