{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T15:40:13Z","timestamp":1737128413018,"version":"3.33.0"},"reference-count":34,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2023,12,12]],"date-time":"2023-12-12T00:00:00Z","timestamp":1702339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,1,17]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>We study numeral forms of completeness and consistency for $\\mathsf {S}^1_2$ and other weak theories, like $\\mathsf {EA}$. This gives rise to an exploration of the derivability conditions needed to establish the mentioned results; a presentation of a weak form of G\u00f6del\u2019s Second Incompleteness Theorem without using \u2018provability implies provable provability\u2019; a provability predicate that satisfies the mentioned derivability condition for weak theories; and a completeness result via consistency statements. Moreover, the paper includes characterizations of the provability predicates for which the numeral results hold, having $\\mathsf {EA}$ as the surrounding theory, and results on functions that compute finitist consistency statements.<\/jats:p>","DOI":"10.1093\/logcom\/exad075","type":"journal-article","created":{"date-parts":[[2023,12,14]],"date-time":"2023-12-14T22:37:40Z","timestamp":1702593460000},"page":"172-193","source":"Crossref","is-referenced-by-count":0,"title":["Numeral completeness of weak theories of arithmetic"],"prefix":"10.1093","volume":"35","author":[{"given":"Reinhard","family":"Kahle","sequence":"first","affiliation":[{"name":"Theorie und Geschichte der Wissenschaften , Universit\u00e4t T\u00fcbingen, Doblerstr. 33, D-72074 T\u00fcbingen,","place":["Germany"]}]},{"given":"Isabel","family":"Oitavem","sequence":"additional","affiliation":[{"name":"Center for Mathematics and Applications (NOVA Math) and Department of Mathematics , NOVA FCT,","place":["Portugal"]}]},{"given":"Paulo Guilherme","family":"Santos","sequence":"additional","affiliation":[{"name":"Section of Mathematics , ISCAL, IPL and Department of Mathematics, NOVA FCT; CMAFcIO, UL,","place":["Portugal"]}]}],"member":"286","published-online":{"date-parts":[[2023,12,12]]},"reference":[{"key":"2025011715020755100_ref1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/S0168-0072(96)00045-0","article-title":"Induction rules, reflection principles, and provably recursive functions","volume":"85","author":"Beklemishev","year":"1997","journal-title":"Annals of Pure and Applied Logic"},{"key":"2025011715020755100_ref2","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/s001530050099","article-title":"A proof-theoretic analysis of collection","volume":"37","author":"Beklemishev","year":"1998","journal-title":"Archive for Mathematical Logic"},{"key":"2025011715020755100_ref3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1462179.1462186","article-title":"On the proof complexity of deep inference","volume":"10","author":"Bruscoli","year":"2009","journal-title":"ACM Transactions on Computational Logic (TOCL)"},{"volume-title":"Bounded Arithmetic","year":"1986","author":"Buss","key":"2025011715020755100_ref4"},{"key":"2025011715020755100_ref5","doi-asserted-by":"crossref","first-page":"737","DOI":"10.2307\/2275906","article-title":"On G\u00f6del\u2019s theorems on lengths of proofs I: number of lines and speedup for Arithmetics","volume":"59","author":"Buss","year":"1994","journal-title":"Journal of Symbolic Logic"},{"volume-title":"Handbook of Proof Theory","year":"1998","author":"Buss","key":"2025011715020755100_ref6"},{"key":"2025011715020755100_ref7","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/3-540-16486-3_94","article-title":"Exponential time and bounded arithmetic","volume-title":"Structure in Complexity Theory","author":"Clote","year":"1986"},{"key":"2025011715020755100_ref8","first-page":"135","article-title":"On the lengths of proofs in the propositional calculus (preliminary version)","volume-title":"Proceedings of the Sixth Annual ACM Symposium on Theory of Computing","author":"Cook","year":"1974"},{"key":"2025011715020755100_ref9","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","article-title":"The relative efficiency of propositional proof systems","volume":"44","author":"Cook","year":"1979","journal-title":"Journal of Symbolic Logic"},{"key":"2025011715020755100_ref10","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/BF01977641","article-title":"Representability op recursively enumerable sets in formal theories","volume":"5","author":"Ehrenfeucht","year":"1960","journal-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforschung"},{"key":"2025011715020755100_ref11","doi-asserted-by":"crossref","first-page":"35","DOI":"10.4064\/fm-49-1-35-92","article-title":"Arithmetization of metamathematics in a general setting","volume":"49","author":"Feferman","year":"1960","journal-title":"Fundamenta Mathematicae"},{"key":"2025011715020755100_ref12","article-title":"Metamathematics of first-order arithmetic","volume-title":"Perspectives in Logic","author":"H\u00e1jek","year":"1998"},{"key":"2025011715020755100_ref13","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1007\/s00153-017-0557-4","article-title":"Interpretability suprema in Peano arithmetic","volume":"56","author":"Henk","year":"2017","journal-title":"Archive for Mathematical Logic"},{"key":"2025011715020755100_ref14","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1090\/S0002-9939-1969-0250878-2","article-title":"A new hierarchy of elementary functions","volume":"20","author":"Herman","year":"1969","journal-title":"Proceedings of the American Mathematical Society"},{"key":"2025011715020755100_ref15","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1023\/A:1005657917054","article-title":"The interpretability logic of all reasonable arithmetical theories","volume":"53","author":"Joosten","year":"2000","journal-title":"Erkenntnis"},{"key":"2025011715020755100_ref16","doi-asserted-by":"crossref","first-page":"603","DOI":"10.1017\/S1755020317000235","article-title":"Generalizations of G\u00f6del\u2019s incompleteness theorems for ${\\varSigma }\\_n$-definable theories of arithmetic","volume":"10","author":"Kikuchi","year":"2017","journal-title":"Review of Symbolic Logic"},{"key":"2025011715020755100_ref17","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/0168-0072(89)90012-2","article-title":"On the number of steps in proofs","volume":"41","author":"Kraj\u00ed\u010dek","year":"1989","journal-title":"Annals of Pure and Applied Logic"},{"key":"2025011715020755100_ref18","doi-asserted-by":"crossref","first-page":"1063","DOI":"10.2307\/2274765","article-title":"Propositional proof systems, the consistency of first order theories and the complexity of computations","volume":"54","author":"Kraj\u00ed\u010dek","year":"1989","journal-title":"Journal of Symbolic Logic"},{"key":"2025011715020755100_ref19","doi-asserted-by":"crossref","first-page":"1181","DOI":"10.1007\/s11225-017-9782-4","article-title":"Arithmetical soundness and completeness for ${\\varSigma }\\_2$ numerations","volume":"106","author":"Kurahashi","year":"2018","journal-title":"Studia Logica"},{"key":"2025011715020755100_ref20","doi-asserted-by":"crossref","first-page":"1229","DOI":"10.1017\/jsl.2018.27","article-title":"Provability logics relative to a fixed extension of Peano arithmetic","volume":"83","author":"Kurahashi","year":"2018","journal-title":"Journal of Symbolic Logic"},{"key":"2025011715020755100_ref21","doi-asserted-by":"crossref","DOI":"10.1017\/9781316716854","volume-title":"Aspects of Incompleteness","author":"Lindstr\u00f6m","year":"2017"},{"key":"2025011715020755100_ref22","first-page":"165","article-title":"On the length of proofs of finitistic consistency statements in first order theories","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Pudl\u00e1k","year":"1986"},{"key":"2025011715020755100_ref23","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/978-3-7091-9461-4_5","article-title":"On the lengths of proofs of consistency","volume-title":"Collegium Logicum","author":"Pudl\u00e1k","year":"1996"},{"key":"2025011715020755100_ref24","first-page":"1391","article-title":"G\u00f6del\u2013Rosser\u2019s incompleteness theorem, generalized and optimized for definable theories","volume":"27","author":"Salehi","year":"2016","journal-title":"Journal of Logic and Computation"},{"key":"2025011715020755100_ref25","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-658-29111-2","volume-title":"Diagonalization in Formal Mathematics","author":"Santos","year":"2020"},{"journal-title":"Journal of Logic and Computation","article-title":"A new perspective on completeness and finitist consistency","author":"Santos","key":"2025011715020755100_ref26"},{"key":"2025011715020755100_ref27","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/BF01621477","article-title":"Herbrand analyses","volume":"30","author":"Sieg","year":"1991","journal-title":"Archive for Mathematical Logic"},{"key":"2025011715020755100_ref28","first-page":"821","article-title":"The incompleteness theorems","volume-title":"Handbook of Mathematical Logic","author":"Smorynski","year":"1993"},{"volume-title":"Efficient Metamathematics","year":"1993","author":"Verbrugge","key":"2025011715020755100_ref29"},{"key":"2025011715020755100_ref30","doi-asserted-by":"crossref","first-page":"785","DOI":"10.2307\/2275908","article-title":"A small reflection principle for bounded arithmetic","volume":"59","author":"Verbrugge","year":"1994","journal-title":"Journal of Symbolic Logic"},{"key":"2025011715020755100_ref31","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1002\/malq.201200102","article-title":"Peano Corto and Peano Basso: a study of local induction in the context of weak theories","volume":"60","author":"Visser","year":"2014","journal-title":"Mathematical Logic Quarterly"},{"key":"2025011715020755100_ref32","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1017\/S1755020319000248","article-title":"Another look at the second incompleteness theorem","volume":"13","author":"Visser","year":"2020","journal-title":"Review of Symbolic Logic"},{"key":"2025011715020755100_ref33","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/s00153-020-00752-5","article-title":"The absorption law or: How to Kreisel a Hilbert\u2013Bernays\u2013L\u00f6b","volume":"60","author":"Visser","year":"2020","journal-title":"Archive for Mathematical Logic"},{"article-title":"Friedman-reflexivity: interpreters as consistoids","year":"2021","author":"Visser","key":"2025011715020755100_ref34"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/1\/172\/54429390\/exad075.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/1\/172\/54429390\/exad075.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T15:02:25Z","timestamp":1737126145000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/35\/1\/172\/7471583"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,12]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,1,17]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exad075","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2025,1]]},"published":{"date-parts":[[2023,12,12]]}}}