Primitive recursive reverse mathematics. (English) Zbl 07748763
Summary: We use a second-order analogy \(\mathsf{PRA}^2\) of \(\mathsf{PRA}\) to investigate the proof-theoretic strength of theorems in countable algebra, analysis, and infinite combinatorics. We compare our results with similar results in the fast-developing field of primitive recursive (‘punctual’) algebra and analysis, and with results from ‘online’ combinatorics. We argue that \(\mathsf{PRA}^2\) is sufficiently robust to serve as an alternative base system below \(\mathsf{RCA}_0\) to study the proof-theoretic content of theorems in ordinary mathematics. (The most popular alternative is perhaps \(\mathsf{RCA}_0^\ast \).) We discover that many theorems that are known to be true in \(\mathsf{RCA}_0\) either hold in \(\mathsf{PRA}^2\) or are equivalent to \(\mathsf{RCA}_0\) or its weaker (but natural) analogy \(2^{\mathbb{N}}\)-\( \mathsf{RCA}_0\) over \(\mathsf{PRA}^2\). However, we also discover that some standard mathematical and combinatorial facts are incomparable with these natural subsystems.
MSC:
| 03B30 | Foundations of classical theories (including reverse mathematics) |
| 03F35 | Second- and higher-order arithmetic and fragments |
| 03D20 | Recursive functions and relations, subrecursive hierarchies |
| 03C57 | Computable structure theory, computable model theory |
| 03D78 | Computation over the reals, computable analysis |
References:
| [1] | Ash, C. J.; Knight, J., Computable Structures and the Hyperarithmetical Hierarchy, Studies in Logic and the Foundations of Mathematics, vol. 144 (2000), North-Holland Publishing Co.: North-Holland Publishing Co. Amsterdam · Zbl 0960.03001 |
| [2] | Avigad, Jeremy, Weak theories of nonstandard arithmetic and analysis, (Simpson, Stephen G., Reverse Mathematics 2001. Reverse Mathematics 2001, Lecture Notes in Logic (2005), Cambridge University Press), 19-46 · Zbl 1087.03038 |
| [3] | Baer, Reinhold, Abelian groups without elements of finite order, Duke Math. J., 3, 1, 68-122 (1937) · Zbl 0016.20303 |
| [4] | Ramil Bagaviev, Ilnur Batyrshin, Nikolay Bazhenov, Dmitry Bushtets, Marina Dorzhieva, Heer Tern Koh, Ruslan Kornev, Alexander Melnikov, Keng Meng Ng, Computably and punctually universal spaces, 2022, submitted for publication. |
| [5] | Bazhenov, N.; Downey, R.; Kalimullin, I.; Melnikov, A., Foundations of online structure theory, Bull. Symb. Log., 25, 2, 141-181 (2019) · Zbl 1477.03167 |
| [6] | Belanger, David R., Reverse mathematics of first-order theories with finitely many models, J. Symb. Log., 79, 3, 955-984 (2014) · Zbl 1353.03006 |
| [7] | Belanger, David R., \( \text{WKL}_0\) and induction principles in model theory, Ann. Pure Appl. Log., 166, 7-8, 767-799 (2015) · Zbl 1369.03099 |
| [8] | Brattka, Vasco; Gherardi, Guido, Weihrauch degrees, omniscience principles and weak computability, J. Symb. Log., 76, 1, 143-176 (2011) · Zbl 1222.03071 |
| [9] | Brattka, Vasco; Gherardi, Guido; Pauly, Arno, Weihrauch complexity in computable analysis, (Handbook of Computability and Complexity in Analysis. Handbook of Computability and Complexity in Analysis, Theory Appl. Comput. (2021), Springer: Springer Cham), 367-417 · Zbl 07464650 |
| [10] | Bazhenov, N. A.; Kalimullin, I. Sh., Punctual categoricity spectra of computably categorical structures, Algebra Log., 60, 3, 223-228 (2021) · Zbl 1515.03160 |
| [11] | Brattka, Vasco, Effective Borel measurability and reducibility of functions, Math. Log. Q., 51, 1, 19-44 (2005) · Zbl 1059.03074 |
| [12] | Brown, Douglas K.; Simpson, Stephen G., Which set existence axioms are needed to prove the separable Hahn-Banach theorem?, Bangkok, 1984. Bangkok, 1984, Ann. Pure Appl. Log., 31, 2-3, 123-144 (1986), Special issue: Second Southeast Asian logic conference (Bangkok, 1984) · Zbl 0615.03044 |
| [13] | Buss, Samuel R., Bounded Arithmetic (1986), Bibliopolis · Zbl 0649.03042 |
| [14] | Buss, Samuel R., First-order proof theory of arithmetic, (Handbook of Proof Theory, 137 (1998)), 79-147 · Zbl 0911.03029 |
| [15] | Cholak, Peter A.; Jockusch, Carl G.; Slaman, Theodore A., On the strength of Ramsey’s theorem for pairs, J. Symb. Log., 66, 1, 1-55 (2001) · Zbl 0977.03033 |
| [16] | Cook, Stephen; Nguyen, Phuong, Logical Foundations of Proof Complexity, Perspectives in Logic (2010), Cambridge University Press, Association for Symbolic Logic: Cambridge University Press, Association for Symbolic Logic Cambridge, La Jolla, CA · Zbl 1206.03051 |
| [17] | Conidis, Chris J., Infinite dimensional proper subspaces of computable vector spaces, J. Algebra, 406, 346-375 (2014) · Zbl 1338.03086 |
| [18] | Conidis, Chris J., The computability, definability, and proof theory of Artinian rings, Adv. Math., 341, 1-39 (2019) · Zbl 1454.03016 |
| [19] | Cenzer, Douglas; Remmel, Jeffrey, Polynomial-time versus recursive models, Ann. Pure Appl. Log., 54, 1, 17-58 (1991) · Zbl 0756.03021 |
| [20] | Cenzer, Douglas; Remmel, Jeffrey, Polynomial-time abelian groups, Ann. Pure Appl. Log., 56, 1-3, 313-363 (1992) · Zbl 0764.03015 |
| [21] | Cenzer, D.; Remmel, J. B., Complexity-theoretic model theory and algebra, (Handbook of Recursive Mathematics, Vol. 1. Handbook of Recursive Mathematics, Vol. 1, Stud. Logic Found. Math., vol. 138 (1998), North-Holland: North-Holland Amsterdam), 381-513 · Zbl 0941.03035 |
| [22] | Chong, C. T.; Yang, Yue, The jump of a \(\operatorname{\Sigma}_n\)-cut, J. Lond. Math. Soc. (2), 75, 3, 690-704 (2007) · Zbl 1123.03038 |
| [23] | Downey, Rodney G.; Hirschfeldt, Denis R.; Kach, Asher M.; Lempp, Steffen; Mileti, Joseph R.; Montalbán, Antonio, Subspaces of computable vector spaces, J. Algebra, 314, 2, 888-894 (2007) · Zbl 1127.03036 |
| [24] | Downey, R.; Melnikov, A. G.; Ng, K. M., Foundations of online structure theory II: the operator approach, Log. Methods Comput. Sci., 17, 3, 6:1-6:35 (2021) · Zbl 07407778 |
| [25] | Ershov, Yuri L.; Goncharov, Sergei S., Constructive Models. Siberian School of Algebra and Logic (2000), Consultants Bureau: Consultants Bureau New York · Zbl 0954.03036 |
| [26] | (Ershov, Yu. L.; Goncharov, S. S.; Nerode, A.; Remmel, J. B.; Marek, V. W., Handbook of Recursive Mathematics. Vol. 1: Recursive Model Theory. Handbook of Recursive Mathematics. Vol. 1: Recursive Model Theory, Studies in Logic and the Foundations of Mathematics, vol. 138 (1998), North-Holland: North-Holland Amsterdam) · Zbl 0905.03001 |
| [27] | (Ershov, Yu. L.; Goncharov, S. S.; Nerode, A.; Remmel, J. B.; Marek, V. W., Handbook of Recursive Mathematics. Vol. 2: Recursive Algebra, Analysis and Combinatorics. Handbook of Recursive Mathematics. Vol. 2: Recursive Algebra, Analysis and Combinatorics, Studies in Logic and the Foundations of Mathematics, vol. 139 (1998), North-Holland: North-Holland Amsterdam) · Zbl 0905.03002 |
| [28] | Enderton, Herbert B., A Mathematical Introduction to Logic (2001), Elsevier · Zbl 0992.03001 |
| [29] | Ershov, Yu. L., Existence of constructivizations, Sov. Math. Dokl., 13, 5, 779-783 (1972) · Zbl 0261.02017 |
| [30] | Ershov, Yu. L., Skolem functions and constructive models, Algebra Log., 12, 6, 368-373 (1973) · Zbl 0294.02017 |
| [31] | Ershov, Yu. L., Decidability Problems and Constructive Models (1980), “Nauka”: “Nauka” Moscow, (in Russian) · Zbl 0495.03009 |
| [32] | Fiori-Carones, Marta; Kołodziejczyk, Leszek Aleksander; Kowalik, Katarzyna W., Weaker cousins of Ramsey’s theorem over a weak base theory, Ann. Pure Appl. Log., 172, 10, Article 103028 pp. (2021) · Zbl 1490.03012 |
| [33] | Fiori-Carones, Marta; Kołodziejczyk, Leszek A.; Lok Wong, Tin; Yokoyama, Keita, An isomorphism theorem for models of Weak König’s Lemma without primitive recursion, J. Eur. Math. Soc. (2023), Accepted to |
| [34] | Fiori-Carones, Marta; Marcone, Alberto, To reorient is easier than to orient: an on-line algorithm for reorientation of graphs, Computability, 10, 3, 215-233 (2021) · Zbl 07429024 |
| [35] | Fiori-Carones, Marta; Shafer, Paul; Soldà, Giovanni, An inside/outside Ramsey theorem and recursion theory, Trans. Am. Math. Soc., 375, 03, 1977-2024 (2022) · Zbl 1505.03027 |
| [36] | Fernandes, António M.; Ferreira, Fernando; Ferreira, Gilda, Analysis in weak systems, (Caleiro, Carlos; Dionísio, Francisco; Gouveia, Paulo; Mateus, Paulo; Rasga, João, Logic and Computation: Essays in Honour of Amílcar Sernadas (2017), College Publication), 231-261 · Zbl 1418.03174 |
| [37] | Flood, Stephen, Reverse mathematics and a Ramsey-type König’s lemma, J. Symb. Log., 77, 4, 1272-1280 (2012) · Zbl 1259.03022 |
| [38] | Friedman, Harvey, Subsystems of second order arithmetic with restricted induction. I [abstract], J. Symb. Log., 41, 2, 557-558 (1976) |
| [39] | Friedman, Harvey, Subsystems of second order arithmetic with restricted induction. II [abstract], J. Symb. Log., 41, 2, 558-559 (1976) |
| [40] | Friedman, Harvey M.; Simpson, Stephen G.; Smith, Rick L., Countable algebra and set existence axioms, Ann. Pure Appl. Log., 25, 2, 141-181 (1983) · Zbl 0575.03038 |
| [41] | Gasarch, William, A survey of recursive combinatorics, (Ershov, Yu. L.; Goncharov, S. S.; Nerode, A.; Remmel, J. B.; Marek, V. W., Studies in Logic and the Foundations of Mathematics. Studies in Logic and the Foundations of Mathematics, Handbook of Recursive Mathematics, vol. 139 (1998), Elsevier), 1041-1176 · Zbl 0936.03041 |
| [42] | Gura, Kirill; Hirst, Jeffry L.; Mummert, Carl, On the existence of a connected component of a graph, Computability, 4, 2, 103-117 (2015) · Zbl 1337.03086 |
| [43] | Gherardi, Guido; Marcone, Alberto, How incomputable is the separable Hahn-Banach theorem?, Notre Dame J. Form. Log., 50, 4, 393-425 (2009) · Zbl 1223.03052 |
| [44] | Greenberg, Noam; Melnikov, Alexander, Proper divisibility in computable rings, J. Algebra, 474, 180-212 (2017) · Zbl 1370.03021 |
| [45] | Grigorieff, Serge, Every recursive linear ordering has a copy in DTIME-\( \operatorname{SPACE}(n, \log(n))\), J. Symb. Log., 55, 1, 260-276 (1990) · Zbl 0708.03015 |
| [46] | Harrington, Leo, Recursively presentable prime models, J. Symb. Log., 39, 305-309 (1974) · Zbl 0332.02055 |
| [47] | Hatzikiriakou, Kostas, Algebraic disguises of \(\operatorname{\Sigma}_1^0\) induction, Arch. Math. Log., 29, 47-51 (1989) · Zbl 0721.03042 |
| [48] | Hirst, Jeffry L., Combinatorics in Subsystems of Second Order Arithmetic (1987), The Pennsylvania State University, PhD thesis |
| [49] | Hirschfeldt, Denis R., Slicing the Truth (2015), World Scientific · Zbl 1304.03001 |
| [50] | Hirschfeldt, Denis R.; Lange, Karen; Shore, Richard A., Induction, bounding, weak combinatorial principles, and the homogeneous model theorem, Mem. Am. Math. Soc., 249, 1187 (2017), iii+101 pages · Zbl 1406.03039 |
| [51] | Harizanov, Valentina S.; Miller, Russell G., Spectra of structures and relations, J. Symb. Log., 72, 1, 324-348 (2007) · Zbl 1116.03029 |
| [52] | Hájek, Petr; Pudlák, Pavel, Metamathematics of First-Order Arithmetic, vol. 3 (2017), Cambridge University Press · Zbl 0889.03053 |
| [53] | Humphreys, A. James; Simpson, Stephen G., Separable Banach space theory needs strong set existence axioms, Trans. Am. Math. Soc., 348, 10, 4231-4255 (1996) · Zbl 0857.03036 |
| [54] | Hatzikiriakou, Kostas; Simpson, Stephen G., Reverse mathematics, Young diagrams, and the ascending chain condition, J. Symb. Log., 82, 2, 576-589 (2017) · Zbl 1422.03018 |
| [55] | Hirschfeldt, Denis; Shore, Richard; Slaman, Theodore, The atomic model theorem and type omitting, Trans. Am. Math. Soc., 361, 11, 5805-5837 (2009) · Zbl 1184.03005 |
| [56] | Jockusch, Carl G., Ramsey’s theorem and recursion theory, J. Symb. Log., 37, 268-280 (1972) · Zbl 0262.02042 |
| [57] | Kaye, Richard, Models of Peano Arithmetic (1991), Clarendon Press: Clarendon Press Oxford · Zbl 0744.03037 |
| [58] | Kierstead, H. A., An effective version of Dilworth’s theorem, Trans. Am. Math. Soc., 268, 63-77 (1981) · Zbl 0485.03019 |
| [59] | Kierstead, H. A., On line coloring k-colorable graphs, Isr. J. Math., 105, 1, 93-104 (1998) · Zbl 0908.05043 |
| [60] | Kołodziejczyk, Leszek A.; Kowalik, Katarzyna W.; Yokoyama, Keita, How strong is Ramsey’s theorem if infinity can be weak?, J. Symb. Log., 88, 2, 620-639 (2023) · Zbl 07691754 |
| [61] | Kalimullin, Iskander; Melnikov, Alexander; Montalban, Antonio, Punctual definability on structures, Ann. Pure Appl. Log., 172, 8, Article 102987 pp. (2021) · Zbl 1532.03066 |
| [62] | Kalimullin, Iskander; Melnikov, Alexander; Meng Ng, Keng, Algebraic structures computable without delay, Theor. Comput. Sci., 674, 73-98 (2017) · Zbl 1418.03151 |
| [63] | Kohlenbach, Ulrich, Theorie der majorisierbaren und stetigen Funktionale und ihre Anwendung bei der Extraktion von Schranken aus inkonstruktiven Beweisen: Effektive Eindeutigkeitsmodule bei besten Approximationen aus ineffektiven Eindeutigkeitsbeweisen (1990), J.W. Goethe Universitaet, PhD thesis · Zbl 0744.03056 |
| [64] | Kohlenbach, Ulrich, Things that can and things that cannot be done in PRA, Ann. Pure Appl. Log., 102, 3, 223-245 (2000) · Zbl 0958.03039 |
| [65] | Kohlenbach, Ulrich, Applied Proof Theory: Proof Interpretations and Their Use in Mathematics (2008), Springer Science & Business Media · Zbl 1158.03002 |
| [66] | Kierstead, H. A.; Penrice, S. G.; Trotter, W. T., On-line coloring and recursive graph theory, SIAM J. Discrete Math., 7, 72-89 (1994) · Zbl 0795.05058 |
| [67] | Kołodziejczyk, Leszek A.; Yokoyama, Keita, Categorical characterizations of the natural numbers require primitive recursion, Ann. Pure Appl. Log., 166, 2, 219-231 (2015) · Zbl 1369.03100 |
| [68] | Lovász, L.; Saks, M.; Trotter, W. T., An on-line graph coloring algorithm with sublinear performance ratio, Discrete Math., 75, 319-325 (1989) · Zbl 0679.05031 |
| [69] | Mal’tsev, A. I., Constructive algebras. I, Russ. Math. Surv., 16, 3, 77-129 (1961) · Zbl 0129.25903 |
| [70] | Mal’tsev, A. I., On recursive abelian groups, Sov. Math. Dokl., 32, 1431-1434 (1962) · Zbl 0156.01105 |
| [71] | Melnikov, Alexander G., Computable abelian groups, Bull. Symb. Log., 20, 3, 315-356 (2014) · Zbl 1345.03065 |
| [72] | Melnikov, Alexander G., Eliminating unbounded search in computable algebra, (Kari, Jarkko; Manea, Florin; Petre, Ion, Unveiling Dynamics and Complexity - 13th Conference on Computability in Europe, CiE 2017. Unveiling Dynamics and Complexity - 13th Conference on Computability in Europe, CiE 2017, Lecture Notes in Computer Science, vol. 10307 (2017), Springer), 77-87 · Zbl 1433.03117 |
| [73] | Melnikov, Alexander G.; Meng Ng, Keng, The back-and-forth method and computability without delay, Isr. J. Math., 234, 2, 959-1000 (2019) · Zbl 1508.03073 |
| [74] | Parikh, Rohit, Existence and feasibility in arithmetic, J. Symb. Log., 36, 3, 494-508 (1971) · Zbl 0243.02037 |
| [75] | Pour-El, Marian B.; Richards, J. Ian, Computability in Analysis and Physics, Perspectives in Mathematical Logic (1989), Springer-Verlag: Springer-Verlag Berlin · Zbl 0678.03027 |
| [76] | Paris, Jeff B.; Kirby, Laurence A. S., \( \sigma_n\)-Collection schemas in arithmetic, (Macintyre, Angus; Pacholski, Leszek; Paris, Jeff, Logic Colloquium ’77. Logic Colloquium ’77, Studies in Logic and the Foundations of Mathematics, vol. 96 (1978), Elsevier), 199-209 · Zbl 0442.03042 |
| [77] | Rabin, Michael O., Computable algebra, general theory and theory of computable fields, Trans. Am. Math. Soc., 95, 341-360 (1960) · Zbl 0156.01201 |
| [78] | Remmel, J. B., Graph colorings and recursively bounded \(\operatorname{\Pi}_1^0\)-classes, Ann. Pure Appl. Log., 32, 185-194 (1986) · Zbl 0625.03024 |
| [79] | Schmerl, James H., Recursive colorings of graphs, Can. J. Math., 32, 4, 821-830 (1980) · Zbl 0394.05021 |
| [80] | Invariants, Richard A. Shore, Boolean algebras and \(\operatorname{ACA}_0^+\), Trans. Am. Math. Soc., 358, 3, 989-1014 (2006) · Zbl 1111.03012 |
| [81] | (Simpson, Stephen G., Reverse Mathematics 2001. Reverse Mathematics 2001, Lecture Notes in Logic, vol. 21 (2005), Association for Symbolic Logic, A K Peters, Ltd.: Association for Symbolic Logic, A K Peters, Ltd. La Jolla, CA, Wellesley, MA) · Zbl 1075.03002 |
| [82] | Simpson, Stephen G., Subsystems of Second Order Arithmetic (2009), Association for Symbolic Logic · Zbl 1181.03001 |
| [83] | Simpson, Stephen G., Baire categoricity and \(\operatorname{\Sigma}_1^0\)-induction, Notre Dame J. Form. Log., 55, 1, 75-78 (2014) · Zbl 1331.03017 |
| [84] | Slaman, Theodore, \( \operatorname{\Sigma}_n\)-bounding and \(\operatorname{\Delta}_n\)-induction, Proc. Am. Math. Soc., 132, 8, 2449-2456 (2004) · Zbl 1053.03034 |
| [85] | Solomon, David Reed, Reverse Mathematics and Ordered Groups (1998), ProQuest LLC: ProQuest LLC Ann Arbor, MI, Thesis (Ph.D.)-Cornell University · Zbl 0973.03076 |
| [86] | Specker, E., Ramsey’s theorem does not hold in recursive set theory, (Logic Colloquium ’69, Proc. Summer School and Colloq.. Logic Colloquium ’69, Proc. Summer School and Colloq., Manchester, 1969 (1971), North-Holland: North-Holland Amsterdam), 439-442 · Zbl 0285.02038 |
| [87] | Simpson, Stephen G.; Smith, Rick L., Factorization of polynomials and \(\operatorname{\Sigma}_1^0\) induction, Ann. Pure Appl. Log., 31, 2-3, 289-306 (1986) · Zbl 0603.03019 |
| [88] | Selivanov, Victor L.; Selivanova, Svetlana, Primitive recursive ordered fields and some applications, (Boulier, François; England, Matthew; Sadykov, Timur M.; Vorozhtsov, Evgenii V., Computer Algebra in Scientific Computing - 23rd International Workshop, CASC 2021. Computer Algebra in Scientific Computing - 23rd International Workshop, CASC 2021, Lecture Notes in Computer Science, vol. 12865 (2021), Springer), 353-369 · Zbl 07497964 |
| [89] | Shioji, Naoki; Tanaka, Kazuyuki, Fixed point theory in weak second-order arithmetic, Ann. Pure Appl. Log., 47, 2, 167-188 (1990) · Zbl 0711.03026 |
| [90] | Simpson, Stephen G.; Yokoyama, Keita, Reverse mathematics and Peano categoricity, Ann. Pure Appl. Log., 164, 3, 284-293 (2013) · Zbl 1267.03030 |
| [91] | Weihrauch, Klaus, Computable Analysis. An introduction, Texts in Theoretical Computer Science. An EATCS Series (2000), Springer-Verlag: Springer-Verlag Berlin · Zbl 0956.68056 |
| [92] | Yokoyama, Keita, On the strength of Ramsey’s theorem without \(\operatorname{\Sigma}_1\)-induction, Math. Log. Q., 59, 108-111 (2013) · Zbl 1267.03031 |
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.
