eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-06-28
9:1
9:19
10.4230/LIPIcs.FSCD.2022.9
article
An Analysis of Tennenbaum’s Theorem in Constructive Type Theory
Hermes, Marc
1
https://orcid.org/0000-0002-0375-759X
Kirst, Dominik
2
https://orcid.org/0000-0003-4126-6975
Department of Mathematics, Universität des Saarlandes, Saarbrücken, Germany
Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany
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 and generalize this result.
The chosen framework allows for a synthetic approach to computability theory, by exploiting the fact that, externally, all functions definable in constructive type theory can be shown computable. We internalize this fact by assuming a version of Church’s thesis expressing that any function on natural numbers is representable by a formula in PA. This assumption allows for a conveniently abstract setup to carry out rigorous computability arguments and feasible 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol228-fscd2022/LIPIcs.FSCD.2022.9/LIPIcs.FSCD.2022.9.pdf
first-order logic
Peano arithmetic
Tennenbaum’s theorem
constructive type theory
Church’s thesis
synthetic computability
Coq