Double-negation introduction
= Double-negation introduction
{title2=$P\vdash\neg\neg P$}
From $P$, temporarily assume $\neg P$. <Negation elimination rule> gives <logical falsity>; discharge that temporary assumption by <negation introduction> to obtain $\neg\neg P$. This is valid in <Intuitionistic propositional logic>, unlike unrestricted <double-negation elimination>.