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
¬,∧,∨,→,↔