If the sequent (Gamma entails forall x exists y A) is provable in first order constructive natural deduction, then the theory (Gamma, forall x (f (x)/y)A), where f is a new function symbol, is a conservative extension of Gamma.
翻译:如果一阶构造自然演绎中可证以下矢列(Γ推出∀x∃y A),则理论(Γ, ∀x (f (x)/y)A)(其中f为新函数符号)是Γ的保守扩充。