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)模型是自然数字的标准模型。 在本文中,我们使用建设性类型的理论作为重新审视、分析和概括这一结果的框架。 所选择的框架允许采用合成方法来推算可比较理论, 利用外部所有在建设性类型理论中可定义的功能都可以被显示为可计算。 然后我们以此观点为基础, 进一步内部化, 假设一个版本的教会理论, 表明自然数字的任何函数都可以由PA的公式代表。 这个假设提供了一种方便的抽象设置, 以进行严格的可比较性论点, 即使在理论的机械化中也是如此。 具体地说, 我们构建了若干经典证据, 并展示了Tennenenbaum 词的内在的建设性解释, 所有这些都遵循文献中的论点。 特别是, 有关经典证据的建设性设置使我们能够突出其假设和结论的差异, 而这些差异并不为典型的典型的公式。 所有版本都配有统一的Coq 证明助手的统一的机械化。</s>