Database: Negation of entailment

Proposition 69: Negation of entailment (inference rule)

Given that \phi entails \psi , we may infer that the negation \neg \psi entails \neg \phi : \cfrac{\phi \vdash \psi}{\neg \psi \vdash \neg \phi}.

Proof: Assume \neg \psi . Using weakening, we infer that \phi entails \neg \psi . But our premise is that \phi entails \psi , so we get by negation introduction that \neg \phi holds. Thus we have showed \neg \psi entails \neg \phi . \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