Database: The contraction rule

Theorem 59: The contraction rule (inference rule)

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

Proof: (a): Assume \psi . By conjunction introduction, infer \psi \wedge \psi holds. By the cut rule, infer \xi . We have thus showed \psi entails \xi .

(b): Assume \phi \wedge \psi . By conjunction elimination, infer \psi holds. By conjunction introduction, infer (\phi \wedge \psi) \wedge \psi holds. By the cut rule, we may infer \xi holds. Thus, \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 introduction
  5. Inference rule: Conjunction elimination
  6. Theorem: The cut rule