The notL proof rule handles a negation ¬P among the assumptions by instead showing its opposite P. In the case of an empty Δ, if P can be shown, then the fact that ¬P was assumed leads to a contradiction to finish the proof.

See also