Database: The exchange rule

Theorem 58: The exchange rule (inference rule)

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

Proof: Assume \psi \wedge \phi . By commutativity of conjunction, we infer that \phi \wedge \psi holds. But then, using the cut rule, we infer that \xi holds. We have thus showed that \psi \wedge \phi entails \xi . \square

This database entry builds on the following:

  1. Terminology: Inference, entailment
  2. Terminology: Inference rule
  3. Definition: Conjunction
  4. Proposition: Commutativity of conjunction
  5. Theorem: The cut rule