{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,18]],"date-time":"2024-04-18T01:50:32Z","timestamp":1713405032032},"reference-count":49,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2021,7,2]],"date-time":"2021-07-02T00:00:00Z","timestamp":1625184000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2022,12]]},"abstract":"Abstract<\/jats:title>We present a new manifestation of G\u00f6del\u2019s second incompleteness theorem and discuss its foundational significance, in particular with respect to Hilbert\u2019s program. Specifically, we consider a proper extension of Peano arithmetic (\n$\\mathbf {PA}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>) by a mathematically meaningful axiom scheme that consists of \n$\\Sigma ^0_2$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-sentences. These sentences assert that each computably enumerable (\n$\\Sigma ^0_1$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-definable without parameters) property of finite binary trees has a finite basis. Since this fact entails the existence of polynomial time algorithms, it is relevant for computer science. On a technical level, our axiom scheme is a variant of an independence result due to Harvey Friedman. At the same time, the meta-mathematical properties of our axiom scheme distinguish it from most known independence results: Due to its logical complexity, our axiom scheme does not add computational strength. The only known method to establish its independence relies on G\u00f6del\u2019s second incompleteness theorem. In contrast, G\u00f6del\u2019s theorem is not needed for typical examples of \n$\\Pi ^0_2$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-independence (such as the Paris\u2013Harrington principle), since computational strength provides an extensional invariant on the level of \n$\\Pi ^0_2$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-sentences.<\/jats:p>","DOI":"10.1017\/s1755020321000265","type":"journal-article","created":{"date-parts":[[2021,7,2]],"date-time":"2021-07-02T09:18:57Z","timestamp":1625217537000},"page":"880-906","update-policy":"http:\/\/dx.doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["A MATHEMATICAL COMMITMENT WITHOUT COMPUTATIONAL STRENGTH"],"prefix":"10.1017","volume":"15","author":[{"given":"ANTON","family":"FREUND","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"S1755020321000265_r45","first-page":"410","volume-title":"Reflections on the Foundations of Mathematics. Essays in Honor of Solomon Feferman","volume":"15","author":"Tait","year":"2002"},{"key":"S1755020321000265_r26","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71876-7"},{"key":"S1755020321000265_r47","first-page":"261","article-title":"Der Wahrheitsbegriff in den formalisierten Sprachen","volume":"1","author":"Tarski","year":"1936","journal-title":"Studia Philosophica"},{"key":"S1755020321000265_r17","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)00003-L"},{"key":"S1755020321000265_r5","doi-asserted-by":"publisher","DOI":"10.1007\/BF01621472"},{"key":"S1755020321000265_r36","unstructured":"[36] Schmidt, D . (1979). Well-Partial Orderings and Their Maximal Order Types. Habilitationsschrift, Universit\u00e4t Heidelberg."},{"key":"S1755020321000265_r8","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(77)90067-1"},{"key":"S1755020321000265_r19","doi-asserted-by":"publisher","DOI":"10.1007\/BF01564760"},{"key":"S1755020321000265_r28","first-page":"210","article-title":"Well-quasi-ordering, the tree theorem, and Vazsonyi\u2019s conjecture","volume":"95","author":"Kruskal","year":"1960","journal-title":"Transactions of the American Mathematical Society"},{"key":"S1755020321000265_r33","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90192-G"},{"key":"S1755020321000265_r38","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70156-9"},{"key":"S1755020321000265_r43","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(95)00029-G"},{"key":"S1755020321000265_r12","doi-asserted-by":"publisher","DOI":"10.1137\/0405010"},{"key":"S1755020321000265_r2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2003.11.030"},{"key":"S1755020321000265_r18","doi-asserted-by":"publisher","DOI":"10.1007\/BF01565428"},{"key":"S1755020321000265_r4","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2005.05.005"},{"key":"S1755020321000265_r27","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19680140702"},{"key":"S1755020321000265_r14","unstructured":"[14] Freund, A. , Rathjen, M. , & Weiermann, A . (2020). Minimal bad sequences are necessary for a uniform Kruskal theorem. Preprint, arXiv:2001.06380."},{"key":"S1755020321000265_r23","doi-asserted-by":"publisher","DOI":"10.1007\/BF02940602"},{"key":"S1755020321000265_r16","first-page":"229","volume-title":"Logic and Combinatorics. Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference 1985","volume":"65","author":"Friedman","year":"1987"},{"key":"S1755020321000265_r10","doi-asserted-by":"crossref","unstructured":"[10] Feferman, S . (1992). Why a little bit goes a long way: Logical foundations of scientifically applicable mathematics, PSA: Proceedings of the 1992 Biennial Meeting of the Philosophy of Science Association. Chicago: University of Chicago, pp. 442\u2013455.","DOI":"10.1086\/psaprocbienmeetp.1992.2.192856"},{"key":"S1755020321000265_r13","doi-asserted-by":"publisher","DOI":"10.1215\/00294527-2019-0031"},{"key":"S1755020321000265_r20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-22156-3"},{"key":"S1755020321000265_r25","first-page":"289","volume-title":"Proceedings of the International Congress of Mathematicians 1958","author":"Kreisel","year":"1960"},{"key":"S1755020321000265_r6","first-page":"179","volume-title":"Logic and Combinatorics. Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference 1985","volume":"65","author":"Buchholz","year":"1987"},{"key":"S1755020321000265_r3","doi-asserted-by":"publisher","DOI":"10.1070\/RM2005v060n02ABEH000823"},{"key":"S1755020321000265_r7","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1983-0687646-0"},{"key":"S1755020321000265_r15","unstructured":"[15] Friedman, H . (2018). Explicitly ${\\varPi}_1^0$ Status 4\/20\/18. Manuscript. Available from: https:\/\/cpb-us-w2.wpmucdn.com\/u.osu.edu\/dist\/1\/1952\/files\/2014\/01\/CMI_ExplicPi01042018-2ilxsqy.pdf (Accessed 31 March 2020)."},{"key":"S1755020321000265_r29","doi-asserted-by":"publisher","DOI":"10.2307\/2045318"},{"key":"S1755020321000265_r32","volume-title":"Proof Theory. The First Step into Impredicativity","author":"Pohlers","year":"2009"},{"key":"S1755020321000265_r34","doi-asserted-by":"publisher","DOI":"10.1016\/j.jctb.2004.08.001"},{"key":"S1755020321000265_r30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-21635-4"},{"key":"S1755020321000265_r35","doi-asserted-by":"publisher","DOI":"10.2307\/2272156"},{"key":"S1755020321000265_r1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1755-2567.1997.tb00744.x"},{"key":"S1755020321000265_r39","doi-asserted-by":"publisher","DOI":"10.2307\/2274585"},{"key":"S1755020321000265_r40","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511581007"},{"key":"S1755020321000265_r48","volume-title":"From Frege to G\u00f6del. A Source Book in Mathematical Logic, 1879\u20131931","author":"van Heijenoort","year":"1967"},{"key":"S1755020321000265_r37","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71815-9"},{"key":"S1755020321000265_r49","unstructured":"[49] Zach, R . Hilbert\u2019s program. In Zalta, E. N. , editor. The Stanford Encyclopedia of Philosophy (fall 2019 edition). Available from: https:\/\/plato.stanford.edu\/archives\/fall2019\/entries\/hilbert-program."},{"key":"S1755020321000265_r42","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71123-6"},{"key":"S1755020321000265_r21","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032399"},{"key":"S1755020321000265_r22","doi-asserted-by":"publisher","DOI":"10.1007\/BF01206605"},{"key":"S1755020321000265_r24","volume-title":"Applied Proof Theory. Proof Interpretations and their Use in Mathematics","author":"Kohlenbach","year":"2008"},{"key":"S1755020321000265_r31","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71130-3"},{"key":"S1755020321000265_r11","doi-asserted-by":"publisher","DOI":"10.1145\/44483.44491"},{"key":"S1755020321000265_r44","doi-asserted-by":"publisher","DOI":"10.2307\/2026089"},{"key":"S1755020321000265_r9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69444-1"},{"key":"S1755020321000265_r41","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70157-0"},{"key":"S1755020321000265_r46","volume-title":"Proof Theory","volume":"81","author":"Takeuti","year":"1987"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1755020321000265","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,17]],"date-time":"2024-04-17T10:36:59Z","timestamp":1713350219000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1755020321000265\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,2]]},"references-count":49,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["S1755020321000265"],"URL":"https:\/\/doi.org\/10.1017\/s1755020321000265","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,2]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press on behalf of The Association for Symbolic Logic","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}