Database: Negation of entailment

Proposition 51: 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: Inference, entailment
  2. Terminology: Inference rule
  3. Definition: Negation
  4. Theorem: The weakening rule
  5. Inference rule: Negation introduction