一句话：在构造类型论中重访、推广并机器化验证 Tennenbaum 定理，并揭示经典证明在假设与结论上的差异。
Tennenbaum 定理指出，Peano 算术（PA）的可数模型中，若算术运算可计算，则模型必为标准自然数模型。本文以构造类型论为框架重访、分析并推广该定理。该框架支持可计算性理论的合成方法：构造类型论中可定义的函数在外部均可证可计算；作者又假设一版 Church 论题，即自然数上任一函数都可由 PA 公式表示，将这一视角内化，为严格的可计算性论证提供抽象设置。基于文献中的经典证明，作者构造化若干证明，并给出一版本质上构造性的 Tennenbaum 定理表述；构造设定还凸显经典证明在假设与结论上的差异。全部版本均在 Coq 中机器化验证。
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.
@article{paperbot2771,
title = {An Analysis of Tennenbaum's Theorem in Constructive Type Theory},
author = {Marc Hermes and Dominik Kirst},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 1},
year = {2024},
doi = {10.46298/lmcs-20(1:19)2024}
}