On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness. (English) Zbl 0945.03088
Using methods developed in previous papers, the author finds arithmetic equivalents of higher-order systems containing arithmetical comprehension, choice and (classically incorrect) general uniform boundedness. A typical result: \(\text{EA}^2+ \text{AC}^{0,0}-\text{qf}+ \Pi^0_1- \text{AC}^-\) is conservative over \(\text{EA}+ \Sigma^0_1- \text{IA}\) for \(\Pi^0_3\)-sentences, where EA is Kalmar-elementary arithmetic and \(\text{EA}^2\) is its second-order extension.
Reviewer: G.Mints (Stanford)
MSC:
| 03F35 | Second- and higher-order arithmetic and fragments |
| 03F30 | First-order arithmetic and fragments |
| 03F10 | Functionals in proof theory |
| 03F03 | Proof theory in general (including proof-theoretic semantics) |
Keywords:
arithmetic equivalents of higher-order systems; arithmetical comprehension; choice; general uniform boundedness; Kalmar-elementary arithmeticReferences:
| [1] | Beklemishev, L. D., A proof-theoretic analysis of collection (1996), Preprint · Zbl 1026.03041 |
| [2] | Bezem, M. A., Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals, J. Symbolic Logic, 50, 652-660 (1985) · Zbl 0578.03030 |
| [3] | Clote, P.; Hájek, P.; Paris, J., On some formalized conservation results in arithmetic, Arch. Math. Logic, 30, 201-218 (1990) · Zbl 0689.03027 |
| [4] | Gödel, K., Zur intuitionistischen Arithmetik und Zahlentheorie, (Ergebnisse eines Mathematischen Kolloquiums, 4 (1933)), 34-38 · JFM 59.0865.03 |
| [5] | Gödel, K., Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, 12, 280-287 (1958) · Zbl 0090.01003 |
| [6] | Howard, W. A., Hereditarily majorizable functionals of finite type, (Troelstra, A. S., Metamathematical investigation of intuitionistic arithmetic and analysis. Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344 (1973), Springer: Springer Berlin) · Zbl 0275.02025 |
| [7] | Kay, R., Models of Peano Arithmetic, (Oxford Logic Guides, 15 (1991), Clarendon Press: Clarendon Press Oxford) · Zbl 0744.03037 |
| [8] | Kohlenbach, U., Pointwise hereditary majorization and some applications, Arch. Math. Logic, 31, 227-241 (1992) · Zbl 0729.03031 |
| [9] | Kohlenbach, U., Analysing proofs in analysis, (Hodges, W.; Hyland, M.; Steinhorn, C.; Truss, J., Logic: from Foundations to Applications. European Logic Colloquium. Logic: from Foundations to Applications. European Logic Colloquium, Keele, 1993 (1996), Oxford University Press: Oxford University Press Oxford), 225-260 · Zbl 0881.03032 |
| [10] | Kohlenbach, U., Real growth in standard parts of analysis, Habilitationsschrift, ((1995)), xv-166, Frankfurt |
| [11] | Kohlenbach, U., A note on the \(Π_2^0\)-induction rule, Arch. Math. Logic, 34, 279-283 (1995) · Zbl 0831.03032 |
| [12] | Kohlenbach, U., Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals, Arch. Math. Logic, 36, 31-71 (1996) · Zbl 0882.03050 |
| [13] | Kohlenbach, U., Elimination of Skolem functions for monotone formulas in analysis, Arch. Math. Logic, 37, 363-390 (1998) · Zbl 0916.03040 |
| [14] | U. Kohlenbach, The use of a logical principle of uniform boundedness in analysis, in: Proc. ‘Logic in Florence 1995’, to appear.; U. Kohlenbach, The use of a logical principle of uniform boundedness in analysis, in: Proc. ‘Logic in Florence 1995’, to appear. · Zbl 0954.03065 |
| [15] | U. Kohlenbach, Arithmetizing proofs in analysis, in: Proc. Logic Colloquium ’96 San Sebastian, to appear.; U. Kohlenbach, Arithmetizing proofs in analysis, in: Proc. Logic Colloquium ’96 San Sebastian, to appear. · Zbl 0919.03046 |
| [16] | U. Kohlenbach, On the no-counterexample interpretation, J. Symbolic Logic, to appear.; U. Kohlenbach, On the no-counterexample interpretation, J. Symbolic Logic, to appear. · Zbl 0960.03047 |
| [17] | Luckhardt, H., Extensional Gödel functional interpretation, A consistency proof of classical analysis, (Lecture Notes in Mathematics, vol. 306 (1973), Springer: Springer Berlin) · Zbl 0262.02031 |
| [18] | Paris, J.; Kirby, L., \(Σ_n^0\)-collection schema in arithmetic, (Logic Colloquium ’77 (1978), North-Holland: North-Holland Amsterdam), 199-209 · Zbl 0442.03042 |
| [19] | Parsons, C., On a number theoretic choice schema and its relation to induction, (Intuitionism and Proof Theory (1970), North-Holland: North-Holland Amsterdam), 459-473 · Zbl 0202.01202 |
| [20] | Parsons, C., On \(n\)-quantifier induction, J. Symbolic Logic, 37, 466-482 (1972) · Zbl 0264.02027 |
| [21] | Shoenfield, J. R., Mathematical Logic (1967), Addison-Wesley: Addison-Wesley New York · Zbl 0155.01102 |
| [22] | Sieg, W., Fragments of arithmetic, Ann. Pure Appl. Logic, 28, 33-71 (1985) · Zbl 0558.03029 |
| [23] | Simpson, S. G., Which set existence axioms are needed to prove the Cauchy/Peano theorem for ordinary differential equations, J. Symbolic Logic, 49, 783-801 (1984) · Zbl 0584.03039 |
| [24] | Spector, C., Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, (Dekker, J. C.E., Proceedings of Symposia in Pure Mathematics. Proceedings of Symposia in Pure Mathematics, Recursive Function Theory, vol. 5 (1962), American Mathmatical Society: American Mathmatical Society Providence, RI), 1-27 · Zbl 0143.25502 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
