Proposition 53: Double negation introduction (inference rule)

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

Proof: By weakening, the negation \neg \phi entails \phi . By the identity rule, \neg \phi entails \neg \phi . Hence, by negation introduction, we infer \neg \neg \phi holds. \square