Double Negation/Double Negation Introduction/Sequent Form

Theorem

The rule of Double Negation Introduction can be symbolised by the sequents:

Formulation 1

$p \vdash \neg \neg p$

Formulation 2

$\vdash p \implies \neg \neg p$