Tennenbaum's theorem states that the only countable model of Peano arithmetic (PA) with computable arithmetical operations is the standard model of natural numbers. In this paper, we use constructive type theory as a framework to revisit, analyze and generalize this result. The chosen framework allows for a synthetic approach to computability theory, exploiting that, externally, all functions definable in constructive type theory can be shown computable. We then build on this viewpoint and furthermore internalize it by assuming a version of Church's thesis, which expresses that any function on natural numbers is representable by a formula in PA. This assumption provides for a conveniently abstract setup to carry out rigorous computability arguments, even in the theorem's mechanization. Concretely, we constructivize several classical proofs and present one inherently constructive rendering of Tennenbaum's theorem, all following arguments from the literature. Concerning the classical proofs in particular, the constructive setting allows us to highlight differences in their assumptions and conclusions which are not visible classically. All versions are accompanied by a unified mechanization in the Coq proof assistant.

翻译：Tennenbaum定理指出，皮亚诺算术（PA）的唯一具有可计算算术运算的可数模型是自然数的标准模型。本文以构造类型理论为框架重新审视、分析并推广了这一结果。所选框架采用综合方法处理可计算性理论，充分利用了构造类型理论中所有可定义函数在外部均可被证明可计算这一特性。我们进一步在此观点基础上进行内化，通过假设丘奇论题的某个版本（即自然数上的任何函数均可由PA中的公式表示）来实现。这一假设为执行严格的可计算性论证（包括定理的机械化证明）提供了便捷的抽象框架。具体而言，我们对几个经典证明进行了构造化改造，并给出了Tennenbaum定理的一种固有构造性表述，所有论证均源自文献中的经典推理。特别地，在经典证明方面，构造性设定使我们得以凸显其假设与结论中经典视角下不可见的差异。所有版本均附带在Coq证明助手中统一的机械化实现。