A note on generalized generalization

The generalization rules of sequent calculi allow, under some restrictions, to derive a formula ∃χφ or ∀χφ from a formula φχ (γ), i.e. from the formula obtained by substituting a variable γ for all free occurrences of χ in φ. We introduce modified generalization rules that make it possible to derive ∃χφ or ∀χφ from φχ (t) even in some cases where t is a complex term. These modified rules were invented in connection with attempts to prove the interpolation theorem for classical predicate logic without equality but with function symbols. This theorem seems (and remains) to be an unresolved case in the literature.