An Analysis of Tennenbaum’s Theorem in Constructive Type Theory
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.
first-order logic
Peano arithmetic
Tennenbaum’s theorem
constructive type theory
Church’s thesis
synthetic computability
Coq
Theory of computation~Constructive mathematics
9:1-9:19
Regular Paper
https://www.ps.uni-saarland.de/extras/tennenbaum
Marc
Hermes
Marc Hermes
Department of Mathematics, Universität des Saarlandes, Saarbrücken, Germany
https://orcid.org/0000-0002-0375-759X
Dominik
Kirst
Dominik Kirst
Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany
https://orcid.org/0000-0003-4126-6975
10.4230/LIPIcs.FSCD.2022.9
Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006.
Andrej Bauer. Intuitionistic mathematics for physics, 2008. URL: http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/.
http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/
George S. Boolos, John P. Burgess, and Richard C. Jeffrey. Computability and logic. Cambridge university press, 2002.
Patrick Cegielski, Kenneth McAloon, and George Wilmers. Modèles récursivement saturés de l'addition et de la multiplication des entiers naturels. In Studies in Logic and the Foundations of Mathematics, volume 108, pages 57-68. Elsevier, 1982.
Thierry Coquand, Nils A. Danielsson, Martın H. Escardó, Ulf Norell, and Chuangjie Xu. Negative consistent axioms can be postulated without loss of canonicity. Unpublished note, 2013. URL: https://www.cs.bham.ac.uk/~mhe/papers/negative-axioms.pdf.
https://www.cs.bham.ac.uk/~mhe/papers/negative-axioms.pdf
Thierry Coquand and Gérard Huet. The calculus of constructions. Technical report, INRIA, 1986.
Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.21.
https://doi.org/10.4230/LIPIcs.CSL.2021.21
Yannick Forster. Parametric Church’s Thesis: Synthetic Computability Without Choice. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, pages 70-89, Cham, 2022. Springer International Publishing.
Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 38-51, 2019.
Yannick Forster, Dominik Kirst, and Dominik Wehr. Completeness theorems for first-order logic analysed in constructive type theory: Extended version. Journal of Logic and Computation, 31(1):112-151, 2021.
Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maximilian Wuttke. A Coq library of undecidable problems. In CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages, 2020.
Jesse M. Han and Floris van Doorn. A formal proof of the independence of the continuum hypothesis. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 353-366, 2020.
Johannes Hostert, Mark Koch, and Dominik Kirst. A toolbox for mechanised first-order logic. In The Coq Workshop 2021, 2021.
Richard Kaye. Tennenbaum’s theorem for models of arithmetic. Set Theory, Arithmetic, and Foundations of Mathematics. Ed. by J. Kennedy and R. Kossak. Lecture Notes in Logic. Cambridge, pages 66-79, 2011.
Dominik Kirst and Marc Hermes. Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1-23:20, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.23.
https://doi.org/10.4230/LIPIcs.ITP.2021.23
Dominik Kirst and Dominique Larchey-Wendling. Trakhtenbrot’s theorem in Coq: A Constructive Approach to Finite Model Theory. In International Joint Conference on Automated Reasoning, pages 79-96. Springer, 2020.
Stephen C. Kleene. Recursive predicates and quantifiers. Transactions of the American Mathematical Society, 53(1):41-73, 1943.
Georg Kreisel. Church’s thesis: a kind of reducibility axiom for constructive mathematics. In Studies in Logic and the Foundations of Mathematics, volume 60, pages 121-150. Elsevier, 1970.
Dominique Larchey-Wendling and Yannick Forster. Hilbert’s tenth problem in Coq. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, volume 131, pages 27-1. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019.
Henning Makholm. Tennenbaum’s theorem without overspill. Mathematics Stack Exchange. (version: 2014-01-24). URL: https://math.stackexchange.com/q/649457.
https://math.stackexchange.com/q/649457
Bassel Mannaa and Thierry Coquand. The independence of Markov’s principle in type theory. Logical Methods in Computer Science, 13, 2017.
Kenneth McAloon. On the complexity of models of arithmetic. The Journal of Symbolic Logic, 47(2):403-415, 1982.
David C. McCarty. Variations on a thesis: intuitionism and computability. Notre Dame Journal of Formal Logic, 28(4):536-580, 1987.
David C. McCarty. Constructive validity is nonarithmetic. The Journal of Symbolic Logic, 53(4):1036-1041, 1988. URL: http://www.jstor.org/stable/2274603.
http://www.jstor.org/stable/2274603
David C. McCarty. Incompleteness in intuitionistic Metamathematics. Notre Dame journal of formal logic, 32(3):323-358, 1991.
Russell O’Connor. Essential incompleteness of arithmetic verified by Coq. In International Conference on Theorem Proving in Higher Order Logics, pages 245-260. Springer, 2005.
Christine Paulin-Mohring. Inductive definitions in the system Coq rules and properties. In International Conference on Typed Lambda Calculi and Applications, pages 328-345. Springer, 1993.
Lawrence C. Paulson. A mechanised proof of Gödel’s incompleteness theorems using nominal Isabelle. Journal of Automated Reasoning, 55(1):1-37, 2015.
Valerii E. Plisko. Constructive formalization of the Tennenbaum theorem and its applications. Mathematical notes of the Academy of Sciences of the USSR, 48(3):950-957, 1990.
Panu Raatikainen. Gödel’s Incompleteness Theorems. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, spring 2021 edition, 2021.
Fred Richman. Church’s thesis without tears. The Journal of symbolic logic, 48(3):797-803, 1983.
Natarajan Shankar. Proof-checking metamathematics (theorem-proving). PhD thesis, The University of Texas at Austin, 1986.
Peter Smith. An introduction to Gödel’s theorems. Cambridge University Press, 2013.
Peter Smith. Tennenbaum’s theorem. Technical report, Cambridge University, 2014. URL: https://www.logicmatters.net/resources/pdfs/tennenbaum_new.pdf.
https://www.logicmatters.net/resources/pdfs/tennenbaum_new.pdf
Andrew Swan and Taichi Uemura. On Church’s Thesis in Cubical Assemblies, 2019. URL: http://arxiv.org/abs/1905.03014.
http://arxiv.org/abs/1905.03014
Michał T. Godziszewski and Joel D. Hamkins. Computable quotient presentations of models of arithmetic and set theory. arXiv e-prints, pages arXiv-1702, 2017.
The Coq Development Team. The Coq Proof Assistant, January 2022. URL: https://doi.org/10.5281/zenodo.5846982.
https://doi.org/10.5281/zenodo.5846982
Stanley Tennenbaum. Non-archimedean models for arithmetic. Notices of the American Mathematical Society, 6(270):44, 1959.
Anne S. Troelstra. Metamathematical investigation of intuitionistic arithmetic and analysis, volume 344. Springer Science & Business Media, 1973.
Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics, Vol. 1. Studies in Logic and the Foundations of Mathematics, Vol. 121. North-Holland Press, Amsterdam, 1988.
George Wilmers. Bounded existential induction. The Journal of Symbolic Logic, 50(1):72-90, 1985.
Norihiro Yamada. Game semantics of Martin-Löf type theory, part III: its consistency with Church’s thesis, 2020. URL: http://arxiv.org/abs/2007.08094.
http://arxiv.org/abs/2007.08094
Marc Hermes and Dominik Kirst
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode