Database: The cut rule

Theorem 80: 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 [69], 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: Class, statement
  2. Definition: Negation
  3. Terminology: Inference
  4. Terminology: Entailment
  5. Terminology: Inference rule
  6. Theorem: The weakening rule
  7. Inference rule: Negation introduction
  8. Proposition: Negation of entailment
  9. Inference rule: Double negation elimination