Database: Double negation of entailment

Proposition 70: Double negation of entailment (inference rule)

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

Proof: By [69], we infer the negation \neg \psi entails \neg \phi . Using [69] once again, we then get that \neg \neg \phi entails \neg \neg \psi . \square

This database entry builds on the following:

  1. Definition: Negation
  2. Terminology: Entailment
  3. Terminology: Inference rule
  4. Proposition: Negation of entailment