Deduction theorem for first-order logic ($\Gamma ,A⊢B⟹\Gamma ⊢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.

For standard effective proof presentations, the syntactic deduction theorem and its reverse give effective transformations between proofs in a one-sentence extension and proofs of an implication in the base theory. Arithmetic can verify these transformations, yielding the displayed internal equivalence under the usual representation and proof-predicate hypotheses. It distinguishes internal proof transformations from an unlicensed reflection step taking provability to truth.