negation introduction
From a subproof that assumes A and reaches ⊥, write ¬A.
Negation introduction (¬I) lets you write ¬A after a subproof that begins with the assumption A and ends with ⊥. It shows a sentence false by showing it leads to a contradiction.
Examples
Assume P, derive ⊥, close the subproof, write ¬P (¬I).
See also