Database: Triple negation elimination

Proposition 68: 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 . Assume \phi . By double negation introduction, we infer that the double negation \neg \neg \phi holds. This shows that \phi entails \neg \neg \phi . We thus conclude using negation introduction that \neg \phi holds. \square

This database entry builds on the following:

  1. Terminology: Class, statement
  2. Definition: Negation
  3. Terminology: Inference
  4. Terminology: Inference rule
  5. Theorem: The weakening rule
  6. Inference rule: Negation introduction
  7. Proposition: Double negation introduction