Negation elimination rule ($\frac{P\neg P}{\perp }$)

From a propositional formula and its negation, infer logical falsity. This identifies a contradiction inside a natural deduction derivation; a later negation introduction rule may discharge the assumption that led to it.