Definition
Negation Introduction Inference Rule (Propositional Hilbert Calculus)
In the propositional Hilbert calculus, negation has the following derived introduction inference rule, for any theory
and formulas : Here
abbreviates : deriving a contradiction under the additional assumption allows us to discharge and conclude .