An Analysis of Tennenbaum’s Theorem in Constructive Type Theory

Authors Marc Hermes , Dominik Kirst



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.9.pdf
  • Filesize: 0.76 MB
  • 19 pages

Document Identifiers

Author Details

Marc Hermes
  • Department of Mathematics, Universität des Saarlandes, Saarbrücken, Germany
Dominik Kirst
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany

Cite AsGet BibTex

Marc Hermes and Dominik Kirst. An Analysis of Tennenbaum’s Theorem in Constructive Type Theory. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.9

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
Keywords
  • first-order logic
  • Peano arithmetic
  • Tennenbaum’s theorem
  • constructive type theory
  • Church’s thesis
  • synthetic computability
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. Google Scholar
  2. Andrej Bauer. Intuitionistic mathematics for physics, 2008. URL: http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/.
  3. George S. Boolos, John P. Burgess, and Richard C. Jeffrey. Computability and logic. Cambridge university press, 2002. Google Scholar
  4. 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. Google Scholar
  5. 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.
  6. Thierry Coquand and Gérard Huet. The calculus of constructions. Technical report, INRIA, 1986. Google Scholar
  7. 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.
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. 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. Google Scholar
  13. Johannes Hostert, Mark Koch, and Dominik Kirst. A toolbox for mechanised first-order logic. In The Coq Workshop 2021, 2021. Google Scholar
  14. 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. Google Scholar
  15. 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.
  16. 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. Google Scholar
  17. Stephen C. Kleene. Recursive predicates and quantifiers. Transactions of the American Mathematical Society, 53(1):41-73, 1943. Google Scholar
  18. 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. Google Scholar
  19. 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. Google Scholar
  20. Henning Makholm. Tennenbaum’s theorem without overspill. Mathematics Stack Exchange. (version: 2014-01-24). URL: https://math.stackexchange.com/q/649457.
  21. Bassel Mannaa and Thierry Coquand. The independence of Markov’s principle in type theory. Logical Methods in Computer Science, 13, 2017. Google Scholar
  22. Kenneth McAloon. On the complexity of models of arithmetic. The Journal of Symbolic Logic, 47(2):403-415, 1982. Google Scholar
  23. David C. McCarty. Variations on a thesis: intuitionism and computability. Notre Dame Journal of Formal Logic, 28(4):536-580, 1987. Google Scholar
  24. David C. McCarty. Constructive validity is nonarithmetic. The Journal of Symbolic Logic, 53(4):1036-1041, 1988. URL: http://www.jstor.org/stable/2274603.
  25. David C. McCarty. Incompleteness in intuitionistic Metamathematics. Notre Dame journal of formal logic, 32(3):323-358, 1991. Google Scholar
  26. 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. Google Scholar
  27. 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. Google Scholar
  28. Lawrence C. Paulson. A mechanised proof of Gödel’s incompleteness theorems using nominal Isabelle. Journal of Automated Reasoning, 55(1):1-37, 2015. Google Scholar
  29. 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. Google Scholar
  30. 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. Google Scholar
  31. Fred Richman. Church’s thesis without tears. The Journal of symbolic logic, 48(3):797-803, 1983. Google Scholar
  32. Natarajan Shankar. Proof-checking metamathematics (theorem-proving). PhD thesis, The University of Texas at Austin, 1986. Google Scholar
  33. Peter Smith. An introduction to Gödel’s theorems. Cambridge University Press, 2013. Google Scholar
  34. Peter Smith. Tennenbaum’s theorem. Technical report, Cambridge University, 2014. URL: https://www.logicmatters.net/resources/pdfs/tennenbaum_new.pdf.
  35. Andrew Swan and Taichi Uemura. On Church’s Thesis in Cubical Assemblies, 2019. URL: http://arxiv.org/abs/1905.03014.
  36. Michał T. Godziszewski and Joel D. Hamkins. Computable quotient presentations of models of arithmetic and set theory. arXiv e-prints, pages arXiv-1702, 2017. Google Scholar
  37. The Coq Development Team. The Coq Proof Assistant, January 2022. URL: https://doi.org/10.5281/zenodo.5846982.
  38. Stanley Tennenbaum. Non-archimedean models for arithmetic. Notices of the American Mathematical Society, 6(270):44, 1959. Google Scholar
  39. Anne S. Troelstra. Metamathematical investigation of intuitionistic arithmetic and analysis, volume 344. Springer Science & Business Media, 1973. Google Scholar
  40. 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. Google Scholar
  41. George Wilmers. Bounded existential induction. The Journal of Symbolic Logic, 50(1):72-90, 1985. Google Scholar
  42. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail