Double-negation introduction ($P⊢\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.