{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:20Z","timestamp":1753894400409,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Tennenbaum's theorem states that the only countable model of Peano arithmetic\n(PA) with computable arithmetical operations is the standard model of natural\nnumbers. In this paper, we use constructive type theory as a framework to\nrevisit, analyze and generalize this result. The chosen framework allows for a\nsynthetic approach to computability theory, exploiting that, externally, all\nfunctions definable in constructive type theory can be shown computable. We\nthen build on this viewpoint, and furthermore internalize it by assuming a\nversion of Church's thesis, which expresses that any function on natural\nnumbers is representable by a formula in PA. This assumption provides for a\nconveniently abstract setup to carry out rigorous computability arguments, even\nin the theorem's mechanization. Concretely, we constructivize several classical\nproofs and present one inherently constructive rendering of Tennenbaum's\ntheorem, all following arguments from the literature. Concerning the classical\nproofs in particular, the constructive setting allows us to highlight\ndifferences in their assumptions and conclusions which are not visible\nclassically. All versions are accompanied by a unified mechanization in the Coq\nproof assistant.<\/jats:p>","DOI":"10.46298\/lmcs-20(1:19)2024","type":"journal-article","created":{"date-parts":[[2024,3,11]],"date-time":"2024-03-11T10:00:14Z","timestamp":1710151214000},"source":"Crossref","is-referenced-by-count":0,"title":["An Analysis of Tennenbaum's Theorem in Constructive Type Theory"],"prefix":"10.46298","volume":"Volume 20, Issue 1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0375-759X","authenticated-orcid":false,"given":"Marc","family":"Hermes","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4126-6975","authenticated-orcid":false,"given":"Dominik","family":"Kirst","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,3,7]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/13204\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/13204\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,11]],"date-time":"2024-03-11T10:00:15Z","timestamp":1710151215000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/11042"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(1:19)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2302.14699v4","asserted-by":"subject"},{"id-type":"arxiv","id":"2302.14699v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2302.14699v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2302.14699","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2302.14699","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,3,7]]},"article-number":"11042"}}