Database: Double negation elimination for entailment

Proposition 62: Double negation elimination for entailment (rule)

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

Proof: Assume \phi . By double negation introduction, \neg \neg \phi holds. By the cut rule, this means \neg \neg \psi holds. We then get by double negation elimination that \psi holds, meaning we have showed \phi entails \psi . \square

This database entry builds on the following:

  1. Terminology: Inference, entailment
  2. Terminology: Inference rule
  3. Definition: Negation
  4. Proposition: Double negation introduction
  5. Inference rule: Double negation elimination
  6. Theorem: The cut rule