Definition
Weak Negation Elimination Inference Rule (Propositional Hilbert Calculus)
In the propositional Hilbert calculus, weak negation elimination is the following derived elimination inference rule, for arbitrary formulas
: This is the principle of explosion (ex falso sequitur quodlibet): a formula and its negation allow any conclusion.