Generalizing theorems in real closed fields Original Research Article

Jan Krajíček posed the following problem: Is there is a generalization result in the theory of real closed fields of the form: If A(1 + … + 1) (n occurrences of 1) is provable in length k for all nϵω, then (∀ 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 Krajíčekʹs question for 1. (1) the axiom system RCF of Artin-Schreier with Gentzenʹs LK as underlying logical calculus, 2. (2) RCF with the variant LKB of LK allowing introduction of several quantifiers of the same type in one step, 3. (3) LKB and the first-order schemata corresponding to Dedekind cuts and the supremum principle. A negative answer is given for 4. (4) any system containing the schema of extensionality.