Database: Negation elimination

Theorem 63: Negation elimination/Principle of explosion (inference rule)

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

Proof: By weakening, we infer \neg \psi entails \neg \phi . Using [51], we then infer the double negation \neg \neg \phi entails \neg \neg \psi . By [62], we conclude \phi entails \psi . \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. Proposition: Negation of entailment
  6. Inference rule: Double negation elimination
  7. Proposition: Double negation elimination for entailment