Definition
Implication Introduction Inference Rule (Propositional Hilbert Calculus)
In the propositional Hilbert calculus, the deduction theorem provides an introduction inference rule for implication. For any theory
and formulas : Here
abbreviates ; the conclusion no longer requires as an additional assumption.