Marc Hermes ; Dominik Kirst - An Analysis of Tennenbaum's Theorem in Constructive Type Theory

lmcs:11042 - Logical Methods in Computer Science, March 7, 2024, Volume 20, Issue 1 - https://doi.org/10.46298/lmcs-20(1:19)2024
An Analysis of Tennenbaum's Theorem in Constructive Type TheoryArticle

Authors: Marc Hermes ORCID; Dominik Kirst ORCID

    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.


    Volume: Volume 20, Issue 1
    Published on: March 7, 2024
    Accepted on: February 3, 2024
    Submitted on: March 7, 2023
    Keywords: Mathematics - Logic,Computer Science - Logic in Computer Science

    Classifications

    Consultation statistics

    This page has been seen 1165 times.
    This article's PDF has been downloaded 369 times.