Database: Negation elimination for entailment

Proposition 64: Negation of entailment (inference rule)

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

Proof: By [51], we infer the double negation \neg \neg \phi entails \neg \neg \psi . Thus, we may infer using [62] that \phi entails \psi . \square

This database entry builds on the following:

  1. Terminology: Inference, entailment
  2. Terminology: Inference rule
  3. Definition: Negation
  4. Proposition: Negation of entailment
  5. Proposition: Double negation elimination for entailment