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证明助手中的统一机械化实现。