Database: The cut rule

Theorem 57: The cut rule (inference rule)
Given that \phi holds and that \phi entails \psi , we may infer that \psi holds: \cfrac{\vdash \phi \quad \phi \vdash \psi}{\vdash \psi}.

Proof: By [51], we infer that the negation \neg \psi entails \neg \phi . Using weakening, we then infer that \neg \psi entails \phi . Thus, by negation introduction, we infer that the double negation \neg \neg \psi holds. Finally, using double negation elimination, we conclude \psi holds. \square

This database entry builds on the following:

  1. Terminology: Inference, entailment
  2. Terminology: Inference rule
  3. Definition: Negation
  4. Theorem: The weakening rule
  5. Inference rule: Negation introduction
  6. Proposition: Negation of entailment
  7. Inference rule: Double negation elimination