Database: Triple negation elimination

Proposition 55: Triple negation elimination (inference rule)

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

Proof: By the weakening rule, \phi entails \neg \neg \neg \phi . We know, by double negation introduction, that \phi entails the double negation \neg \neg \phi . We may therefore infer using negation introduction that \neg \phi holds. \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. Inference rule: Negation introduction
  6. Proposition: Double negation introduction