Negation introduction rule
= Negation introduction rule
{title2=$\dfrac{[P]\ \vdots\ \bot}{\neg P}$}
If a <natural deduction> subproof derives <logical falsity> from a temporary assumption $P$, discharge that assumption to conclude $\neg P$. Other undischarged assumptions remain available. This gives a constructive proof of a <negation> and does not require <double-negation elimination>.