= Deduction theorem for first-order logic
{title2=$\Gamma,A\vdash B\Longrightarrow\Gamma\vdash A\to B$}
In the usual first-order Hilbert system, <logical implication> discharge requires the appropriate generalization restriction: a variable generalized in the derivation must not be free in the assumption being discharged. Equivalently use a proof system whose generalization rule already forbids variables free in open assumptions. One can first discharge a temporary assumption and then generalize if the quantified variable is not free in the remaining assumptions. Ignoring this side condition would allow deriving universal conclusions from a single arbitrary instance as an open hypothesis.
Back to article page
