Baaz, Matthias, and Richard Zach. 1995. “Generalizing Theorems in Real Closed Fields.” Annals of Pure and Applied Logic 75 (1–2): 3–23. https://doi.org/10.1016/0168-0072(94)00054-7.

Jan Krajicek posed the following problem: Is there is a generalization result in the theory of real closed fields of the form: If \(A(1 + \dots + 1)\) (\(n\) occurrences of 1) is provable in length \(k\) for all \(n = 0, 1, 2, \dots\), then \((\forall x)A(x)\) is provable? It is argued that the answer to this question depends on the particular formulation of the “theory of real closed fields.” Four distinct formulations are investigated with respect to their generalization behavior. It is shown that there is a positive answer to Krajicek’s question for (1) the axiom system RCF of Artin-Schreier with Gentzen’s LK as underlying logical calculus, (2) RCF with the variant LKB of LK allowing introduction of several quantifiers of the same type in one step, (3) LKB and the first-order schemata corresponding to Dedekind cuts and the supremum principle. A negative answer is given for (4) any system containing the schema of extensionality.