Negation introduction rule ($\frac{[P]⋮\perp }{\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.