Double Negation/Double Negation Elimination/Formulation 1/Sequent Form

Theorem

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

Formulation 1

$\neg \neg p \vdash p$

Formulation 2

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