{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T18:10:15Z","timestamp":1726251015732},"reference-count":42,"publisher":"Oxford University Press (OUP)","issue":"6","license":[{"start":{"date-parts":[[2023,4,24]],"date-time":"2023-04-24T00:00:00Z","timestamp":1682294400000},"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":[[2024,9,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>In this paper, we study the metamathematics of consistent arithmetical theories $T$ (containing $\\textsf {I}\\varSigma _{1}$); we investigate numerical properties based on proof predicates that depend on numerations of the axioms. Numeral Completeness. For every true (in $\\mathbb {N}$) sentence $\\vec {Q}\\vec {x}.\\varphi (\\vec {x})$, with $\\varphi (\\vec {x})$ a $\\varSigma _{1}(\\textsf {I}\\varSigma _1)$-formula, there is a numeration $\\tau $ of the axioms of $T$ such that $\\textsf {I}\\varSigma _1\\vdash \\vec {Q}\\vec {x}. \\texttt {Pr}_{\\tau }(\\ulcorner \\varphi (\\overset {\\text{.} }{\\vec {x}})\\urcorner )$, where $\\texttt {Pr}_{\\tau }$ is the provability predicate for the numeration $\\tau $.<\/jats:p>\n               <jats:p>Numeral Consistency. If $T$ is consistent, there is a $\\varSigma _{1}(\\textsf {I}\\varSigma _1)$-numeration $\\tau $ of the axioms of $\\textsf {I}\\varSigma _{1}$ such that $\\textsf {I}\\varSigma _1\\vdash \\forall\\, x. \\texttt {Pr}_{\\tau }(\\ulcorner \\neg \\textit {Prf}(\\ulcorner \\perp \\urcorner , \\overset {\\text{.}}{x})\\urcorner )$, where $\\textit {Prf}(x,y)$ denotes a $\\varDelta _{1}(\\textsf {I}\\varSigma _1)$-definition of \u2018$y$ is a $T$-proof of $x$\u2019. Finitist consistency is addressed by generalizing a result of Artemov:<\/jats:p>\n               <jats:p>Partial finitism. If $T$ is consistent, there is a primitive recursive function $f$ such that, for all $n\\in \\mathbb {N}$, $f(n)$ is the code of an $\\textsf {I}\\varSigma _{1}$-proof of $\\neg\\, \\textit{Prf}(\\ulcorner \\perp \\urcorner ,\\overline {n})$.<\/jats:p>\n               <jats:p>These results are not in conflict with G\u00f6del\u2019s Incompleteness Theorems. Rather, they allow to extend their usual interpretation and show a deep connection to reflections in Hilbert\u2019s last papers of 1931.<\/jats:p>","DOI":"10.1093\/logcom\/exad021","type":"journal-article","created":{"date-parts":[[2023,4,24]],"date-time":"2023-04-24T18:59:08Z","timestamp":1682362748000},"page":"1179-1198","source":"Crossref","is-referenced-by-count":0,"title":["A new perspective on completeness and finitist consistency"],"prefix":"10.1093","volume":"34","author":[{"given":"Paulo Guilherme","family":"Santos","sequence":"first","affiliation":[{"name":"NovaMath , NOVA School of Science and Technology, P-2829-516 Caparica, Portugal"}]},{"given":"Wilfried","family":"Sieg","sequence":"additional","affiliation":[{"name":"Department of Philosophy , Carnegie Mellon University, Pittsburgh, PA 15213, USA"}]},{"given":"Reinhard","family":"Kahle","sequence":"additional","affiliation":[{"name":"Theorie und Geschichte der Wissenschaften , Universit\u00e4t T\u00fcbingen, Doblerstr. 33, D-72074 T\u00fcbingen, Germany"}]}],"member":"286","published-online":{"date-parts":[[2023,4,24]]},"reference":[{"article-title":"The provability of consistency","year":"2020","author":"Artemov","key":"2024091304303776600_ref1"},{"key":"2024091304303776600_ref2","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1070\/RM2005v060n02ABEH000823","article-title":"Reflection principles and provability algebras in formal arithmetic","volume":"60","author":"Beklemishev","year":"2005","journal-title":"Russian Mathematical Surveys"},{"volume-title":"Handbook of Proof Theory","year":"1998","author":"Buss","key":"2024091304303776600_ref3"},{"key":"2024091304303776600_ref4","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1017\/bsl.2020.9","article-title":"Finding the limit of incompleteness I","volume":"26","author":"Cheng","year":"2020","journal-title":"Bulletin of Symbolic Logic"},{"key":"2024091304303776600_ref5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-69444-1","volume-title":"David Hilbert\u2019s Lectures on the Foundations of Arithmetic and Logic 1917\u20131933","author":"Ewald","year":"2013"},{"volume-title":"From Kant to Hilbert Volume 2: A Source Book in the Foundations of Mathematics","year":"1996","author":"Ewald","key":"2024091304303776600_ref6"},{"key":"2024091304303776600_ref7","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":"2024091304303776600_ref8","doi-asserted-by":"crossref","first-page":"259","DOI":"10.2307\/2964649","article-title":"Transfinite recursive progressions of axiomatic theories","volume":"27","author":"Feferman","year":"1962","journal-title":"Journal of Symbolic Logic"},{"key":"2024091304303776600_ref9","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1305\/ndjfl\/1107220675","article-title":"A simple proof of Parsons\u2019 theorem","volume":"46","author":"Ferreira","year":"2005","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"2024091304303776600_ref10","article-title":"Metamathematics of first-order arithmetic","volume-title":"Perspectives in Logic","author":"H\u00e1jek","year":"1998"},{"key":"2024091304303776600_ref11","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-68011-6","volume-title":"David Hilbert\u2019s Lectures on the Foundations of Geometry 1891\u20131902","author":"Hallett","year":"2004"},{"key":"2024091304303776600_ref12","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":"2024091304303776600_ref13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1515\/crll.1932.166.1","article-title":"Sur la non-contradiction de l\u2019arithm\u00e9tique","volume":"1932","author":"Herbrand","year":"1932","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik"},{"volume-title":"Prinzipien der Mathematik. Lecture notes by Paul Bernays. Winter-Semester 1917\u201318","year":"1918","author":"Hilbert","key":"2024091304303776600_ref14"},{"key":"2024091304303776600_ref15","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BF01448445","article-title":"Die logischen Grundlagen der Mathematik","volume":"88","author":"Hilbert","year":"1923","journal-title":"Mathematische Annalen"},{"key":"2024091304303776600_ref16","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/BF01457953","article-title":"Die Grundlegung der elementaren Zahlenlehre","volume":"104","author":"Hilbert","year":"1931","journal-title":"Mathematische Annalen"},{"key":"2024091304303776600_ref17","first-page":"120","article-title":"Beweis des tertium non datur, Nachrichten von der Gesellschaft der Wissenschaften zu G\u00f6ttingen","author":"Hilbert","year":"1931","journal-title":"Mathematisch-physikalische Klasse"},{"key":"2024091304303776600_ref18","doi-asserted-by":"crossref","first-page":"359","DOI":"10.2307\/2273028","article-title":"Redundancies in the Hilbert\u2013Bernays derivability conditions for G\u00f6del\u2019s second incompleteness theorem","volume":"38","author":"Jeroslow","year":"1973","journal-title":"Journal of Symbolic Logic"},{"key":"2024091304303776600_ref19","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-3-030-65824-3_5","article-title":"Lorenzen between Gentzen and Sch\u00fctte","volume-title":"Paul Lorenzen Mathematician and Logician","author":"Kahle","year":"2021"},{"article-title":"Numeral Completeness of Weak Theories of Arithmetic","year":"2022","author":"Kahle","key":"2024091304303776600_ref20"},{"key":"2024091304303776600_ref21","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1111\/j.1746-8361.1958.tb01469.x","article-title":"Hilbert\u2019s programme","volume":"12","author":"Kreisel","year":"1958","journal-title":"Dialectica"},{"key":"2024091304303776600_ref22","article-title":"Formally self-referential propositions for cut free classical analysis and related systems","author":"Kreisel","year":"1974","journal-title":"Instytut Matematyczny Polskiej Akademi Nauk (Warszawa)"},{"key":"2024091304303776600_ref23","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":"2024091304303776600_ref24","doi-asserted-by":"crossref","first-page":"953","DOI":"10.1007\/s00153-018-0618-3","article-title":"On partial disjunction properties of theories containing Peano arithmetic","volume":"57","author":"Kurahashi","year":"2018","journal-title":"Archive for Mathematical Logic"},{"key":"2024091304303776600_ref25","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":"The Journal of Symbolic Logic"},{"key":"2024091304303776600_ref26","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/978-981-16-4173-2_4","article-title":"Rosser provability and the second incompleteness theorem","volume-title":"Advances in Mathematical Logic","author":"Kurahashi","year":"2021"},{"key":"2024091304303776600_ref27","article-title":"Aspects of incompleteness","volume-title":"Lecture Notes in Logic","author":"Lindstr\u00f6m","year":"2017"},{"key":"2024091304303776600_ref28","first-page":"123","article-title":"Lecture Notes in Logic.","volume-title":"Intensionality in Philosophy and Metamathematics","author":"Niebergall","year":"2005"},{"key":"2024091304303776600_ref29","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780198783596.001.0001","volume-title":"Towards Non-Being","author":"Priest","year":"2016"},{"key":"2024091304303776600_ref30","article-title":"G\u00f6del\u2019s incompleteness theorems","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Raatikainen","year":"2020"},{"author":"Santos","key":"2024091304303776600_ref31","article-title":"On notions of provability"},{"key":"2024091304303776600_ref32","first-page":"3","article-title":"Finitism = PRA? On a thesis of W. W. Tait","author":"Schirn","year":"01 2005","journal-title":"Reports on Mathematical Logic"},{"key":"2024091304303776600_ref33","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"},{"volume-title":"Hilbert\u2019s Programs and Beyond","year":"2013","author":"Sieg","key":"2024091304303776600_ref34"},{"key":"2024091304303776600_ref35","article-title":"An introduction to G\u00f6del\u2019s theorems","volume-title":"Cambridge Introductions to Philosophy","author":"Smith","year":"2013"},{"key":"2024091304303776600_ref36","doi-asserted-by":"crossref","first-page":"821","DOI":"10.1016\/S0049-237X(08)71123-6","article-title":"The incompleteness theorems","volume-title":"Handbook of Mathematical Logic","author":"Smorynski","year":"1977"},{"key":"2024091304303776600_ref37","article-title":"Source books in the history of the sciences","volume-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931","author":"van Heijenoort","year":"1967"},{"key":"2024091304303776600_ref38","article-title":"Provability logic","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Verbrugge","year":"2017"},{"key":"2024091304303776600_ref39","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":"The Review of Symbolic Logic"},{"key":"2024091304303776600_ref40","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/s00153-020-00752-5","article-title":"The absorption law","volume":"60","author":"Visser","year":"2021","journal-title":"Archive for Mathematical Logic"},{"key":"2024091304303776600_ref41","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/s001530050081","article-title":"Fragments of HA based on $\\{\\varSigma \\}\\_1$-induction","volume":"37","author":"Wehmeier","year":"1997","journal-title":"Archive for Mathematical Logic"},{"key":"2024091304303776600_ref42","article-title":"Hilbert\u2019s program","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Zach","year":"2019"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/34\/6\/1179\/59088585\/exad021.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/34\/6\/1179\/59088585\/exad021.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T17:21:31Z","timestamp":1726248091000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/34\/6\/1179\/7131413"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,24]]},"references-count":42,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2023,4,24]]},"published-print":{"date-parts":[[2024,9,6]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exad021","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2024,9]]},"published":{"date-parts":[[2023,4,24]]}}}