 Negation introduction rule

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.