An Analysis of Tennenbaum's Theorem in Constructive Type Theory

Marc Hermes, Dominik Kirst

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,…