Database: Double negation of entailment

Proposition 54: 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 [51], we infer the negation \psi entails \neg \phi . Using [51] again, we then get that \neg \neg \phi entails \neg \neg \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