Generalizing theorems in real closed fields Export

@article{citeulike:130231, abstract = {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 + ... + 1) (n occurrences of 1) is provable in length k for all n [epsi] [omega], 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. (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 for4. (4) any system containing the schema of extensionality.}, author = {Baaz, Matthias and Zach, Richard}, citeulike-article-id = {130231}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/0168-0072(94)00054-7}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B6TYB-41MJ4DT-1/2/f5a945cbb6b9d9253b347379921691c8}, day = {12}, doi = {10.1016/0168-0072(94)00054-7}, journal = {Annals of Pure and Applied Logic}, keywords = {generalization\_of\_proofs, kreisel, proof\_theory}, month = {September}, number = {1-2}, pages = {3--23}, posted-at = {2005-03-16 17:59:12}, priority = {0}, title = {Generalizing theorems in real closed fields}, url = {http://dx.doi.org/10.1016/0168-0072(94)00054-7}, volume = {75}, year = {1995} }

TY - JOUR ID - citeulike:130231 L3 - citeulike-article-id:130231 N2 - 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 + ... + 1) (n occurrences of 1) is provable in length k for all n [epsi] [omega], 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. (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 for4. (4) any system containing the schema of extensionality. IS - 1-2 JF - Annals of Pure and Applied Logic EP - 23 TI - Generalizing theorems in real closed fields VL - 75 SP - 3 KW - generalization_of_proofs KW - kreisel KW - proof_theory AU - Baaz, Matthias AU - Zach, Richard PY - 1995/09/12/ UR - http://dx.doi.org/10.1016/0168-0072(94)00054-7 ER -