An Analysis of Tennenbaum's Theorem in Constructive Type Theory

TL;DR

This paper revisits Tennenbaum's theorem within constructive type theory, providing a synthetic computability framework, generalizations, and mechanized proofs in Coq, highlighting differences from classical assumptions.

Contribution

It introduces a constructive approach to Tennenbaum's theorem, generalizes classical proofs, and provides a mechanized formalization in Coq.

Findings

Constructive type theory enables a synthetic approach to computability.

The paper generalizes classical Tennenbaum's theorem within a constructive setting.

Mechanized proofs in Coq validate the constructive versions of the theorem.

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

Equations

$$:=\forall P:\mathbb{P}.\mathsf{definite}P$$

$$:=\forall P:\mathbb{P}.\mathsf{stable}P$$

$$:=\forall f:\mathbb{N}\to \mathbb{N}.\mathsf{stable}(\exists n.fn=0)$$

$$s,t:\mathsf{tm}$$

$$\alpha ,\beta :\mathsf{fm}$$

$$\perp [\sigma ]:=\perp (P\vec{v})[\sigma ]:=P(\vec{v}[\sigma ])(\alpha \dot{\square }\beta )[\sigma ]:=\alpha [\sigma ]\dot{\square }\beta [\sigma ](\dot{\nabla }\phi )[\sigma ]:=\dot{\nabla }(\phi [x_0;\lambda x.(\sigma x)[\uparrow ]])$$

$$\hat{\rho }{x}_k:=\rho k\hat{\rho }(f\vec{v}):=f^{\mathcal{M}}(\hat{\rho }\vec{v})(v:{\mathsf{tm}}^n)$$

$$\mathcal{M}{\models }_{\rho }P\vec{v}$$

$$\mathcal{M}{\models }_{\rho }\alpha \wedge \beta$$

$$\mathcal{M}{\models }_{\rho }\forall \alpha$$

$${\Sigma }_{\mathsf{PA}}:=({\mathcal{F}}_{\mathsf{PA}};{\mathcal{P}}_{\mathsf{PA}})=(0,S,+,\times ;=)$$

$$\forall x.Sx=0\to \perp$$

$$\forall x.0+x=x$$

$$\forall x.0\times x=0$$

$$\forall x.x=x$$

$$\forall xy.x=y\to y=x$$

$$\forall xyz.x=y\to y=z\to x=z$$

$$\forall xy.x=y\to Sx=Sy$$

$$\forall xyuv.x=u\to y=v\to x+y=u+v$$

$$\forall xyuv.x=u\to y=v\to x\times y=u\times v$$

$$\exists c\!:\!\mathbb{N}{}~{}\forall u\!:\!\mathbb{N}.\big{(}u<n\rightarrow(p\,u\leftrightarrow\pi_{u}\mid c)\big{)}\land\big{(}\pi_{u}\mid c\rightarrow u<n\big{)}$$

$$\neg\neg\,\exists c\!:\!\mathbb{N}{}~{}\forall u\!:\!\mathbb{N}.\big{(}u<n\rightarrow(p\,u\leftrightarrow\pi_{u}\mid c)\big{)}\land\big{(}\pi_{u}\mid c\rightarrow u<n\big{)}$$

$$\mathcal{M}\models \forall e\neg \neg \exists c\forall u<\overline{n}.\alpha (u,e)\leftrightarrow \Pi (u)\mid c.$$

$$\mathcal{M}\models \exists c\forall u<\overline{n}.\alpha (u,e)\leftrightarrow \Pi (u)\mid c.$$

$$\mathcal{M}\models \alpha (\overline{u},e)⟺pu⟺{\pi }_u\mid a⟺\mathcal{M}\models \Pi (\overline{u})\mid \overline{a}$$

$$\neg \neg \exists c:\mathcal{M}\forall u:\mathbb{N}.\mathcal{M}\models \alpha (\overline{u})\leftrightarrow \Pi (\overline{u})\mid c.$$

$$\mathcal{M}\models \neg \neg \exists c\forall u<\overline{n}.\alpha (u)\leftrightarrow \Pi (u)\mid c$$

$$\neg \neg \exists e>\mathbb{N}.\mathcal{M}\models \neg \neg \exists c\forall u<e.\alpha (u)\leftrightarrow \Pi (u)\mid c$$

$$⟹$$

$$\neg \neg \exists c:\mathcal{M}\forall u:\mathbb{N}.\mathcal{M}\models \alpha (\overline{u},e)\leftrightarrow \Pi (\overline{u})\mid c.$$

$$pn$$

$$\neg pn$$

$$\mathsf{Q}⊢{\phi }_p(\overline{x})$$

$$⟺\exists n:\mathbb{N}.\mathsf{Q}⊢\overline{fn}=S\overline{x}⟺\exists n:\mathbb{N}.fn=x+1⟺px$$

$$\mathcal{M}\models \forall ed\exists rq.e=q\cdot d+r\wedge (0<d\to r<d)$$

$$pn$$

$$\neg pn$$

$$\neg \mathcal{M}\models \overline{{\pi }_c}\mid gc\stackrel{\text{def.}}{⟺}pc\stackrel{\text{coding}}{⟺}\mathcal{M}\models \overline{{\pi }_c}\mid gc$$

Full text

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.

1. Introduction

There are well-known proofs in classical logic showing that the first-order theory of Peano arithmetic ($\mathsf{PA}$) has non-standard models, meaning models which are not isomorphic to the standard model $\mathbb{N}$. One way to do so (cf. [BBJ02]), starts by adding a new constant symbol $c$ to the language of $\mathsf{PA}$, together with the enumerable list of new axioms $c\neq 0$, $c\neq 1$, $c\neq 2$ etc. This theory has the property that every finite subset of its axioms is satisfied by the standard model $\mathbb{N}$, since we can always give a large enough interpretation of the constant $c$ in $\mathbb{N}$. Hence, by the compactness theorem, the full theory has a model $\mathcal{M}$, which must then be non-standard since the interpretation of $c$ in $\mathcal{M}$ corresponds to an element which is larger than any number $n$ in $\mathbb{N}{}$.

The presence of non-standard elements like this has interesting consequences. $\mathsf{PA}$ can prove that for every bound $n$, sums of the form $\sum_{k\leq n}a_{k}$ exist, so in particular for example the Gaussian sum $\sum_{k\leq n}k$. The presence of the non-standard element $c$ in $\mathcal{M}$ allows for the creation of infinite sums like $\sum_{k\leq c}k$. Remarkably, while this means that it includes a summation over all natural numbers, the model specifies a single element as the result of this infinite sum. A general $\mathsf{PA}$ model $\mathcal{M}$ therefore exhibits behaviors which disagree with the common intuition that computations in $\mathsf{PA}$ are finitary, which are—in the end—largely based on the familiarity with the standard model $\mathbb{N}$.

These intuitions are still not too far off the mark, as was demonstrated by Stanley Tennenbaum [Ten59] in a remarkable theorem. By being a little more restrictive on the models under consideration, $\mathbb{N}$ regains a unique position:

Tennenbaum’s Theorem: Apart from the standard model $\mathbb{N}$, there is no countable computable model of first-order $\mathsf{PA}$.

A model is considered computable if its elements can be coded by numbers in $\mathbb{N}$, and the arithmetic operations on its elements can be realized by computable functions on these codes. Usually, Tennenbaum’s theorem is formulated in a classical framework such as $\mathsf{ZF}$ set theory, and the precise meaning of computable is given by making reference to a concrete model of computation like Turing machines, $\mu$-recursive functions, or the $\lambda$-calculus [Kay11, Smi14]. In a case like this, where computability theory is applied rather than developed, the computability of a function is rarely proven by exhibiting an explicit construction in the specific model, but rather by invoking the informal Church-Turing thesis, stating that every function intuitively computable is computable in the chosen model. Proving the computability of a function is then reduced to giving an intuitive justification.

The focus of this paper lies on revisiting Tennenbaum’s theorem and several of its proofs in a constructive type theory ($\mathsf{CTT}$). In contrast to classical treatments, the usage of a constructive meta-theory enables us to formally assume Church’s thesis [Kre70, TvD88, For21a] in the form of an axiom, stating that every total function is computable. By its usage, the elegant and succinct paper-style computability proofs can be reproduced, but in a fully formal manner, also allowing for straightforward mechanized proofs.

In the constructive type theory that we will specify in Section 2, the addition of this axiom becomes possible since we can adapt the approach of synthetic computability [Ric83, Bau06, FKS19]: Any function term that is definable in $\mathsf{CTT}$ by the virtue of its syntactic rules, can externally be observed to be a computable function. Following through on this external observation, it can be taken as a justification to also internally treat functions as if they were computable. For example, we will make use of this perspective when defining a predicate on a type $X$ to be decidable if there exists a function $f\!:\!X\to\mathbb{B}$ computing booleans which reflect the truth values of $p$ (Definition 2.3).

This approach leads to a simplification when it comes to the statement of Tennenbaum’s theorem itself: By interpreting arithmetic operations as type-theoretic functions in $\mathsf{CTT}$, all models are automatically computable in the synthetic sense. Consequently, “computable model” no longer needs to be part of the theorem statement. Moreover, the given synthetic proofs unveil the computational essence of Tennenbaum’s theorem with neither the technical overhead of constructions in a formal model of computability nor the informal practice to simply disregard computability arguments. The paper therefore contributes to an active line of research on mechanized metamathematics [Kir22] with the two-fold goal to obtain a uniform and constructive development of the foundations of mathematics, complemented by a principled mechanization for guaranteed correctness and collaborative use.

In the above sketched framework, we follow the classical presentations of Tennenbaum’s theorem [Kay11, Smi14] and develop constructive versions that only assume a type-theoretic version of Markov’s principle [MC17]. This is then complemented by the adaption of an inherently more constructive variant given by McCarty [McC87, McC88].

Concretely, our contributions can be summarized as follows:

• •

We review several existing proofs of Tennenbaum’s theorem drawn from the literature, and carry them out in a constructive meta-theory. We work out subtle differences in the strengths of their conclusions, which are left invisible in any classical treatment, but come to light once they are viewed through a constructive lens.

• •

By considering models with a decidable divisibility relation (Theorem 7.50), we extend the theorem to models which do not have to be discrete or enumerable.

• •

We provide a Coq mechanization covering all results presented in this paper.111 The full mechanization is available on GitHub [Her23] and can conveniently be viewed on a webpage [HK23]. We make use of a fact for which we gave no mechanized proof, namely Hypothesis 7.3 in Section 7.3.

The present paper is an extended version of [HK22] and adds the following contributions:

• •

In [HK22], we only gave a reference to a possible proof strategy for showing the existence of $\mathsf{HA}$-inseparable formulas (Definition 7.52). A comment in [Pet22] pointed to a more straightforward approach, which we were able to mechanize, and have added to Section 7.3.

• •

We added a short discussion in Section 7.4, in which we aim to abstractly identify the main ingredients that are used in Section 7.3 to derive Tennenbaum’s theorem.

• •

Our Coq mechanization has been re-based and now relies on a collaborative Coq library for first-order logic [KHD*+*22], to which we have contributed by integrating the mechanization developed for this publication. This integration not only enabled the utilization of pre-existing definitions for $\Delta_{1}$ and $\Sigma_{1}$–formulas but also provides additional validation for our application of Church’s thesis for Robinson arithmetic ($\mathsf{CT_{Q}}$), given the library includes its derivation from a more conventional formulation of Church’s thesis [KP23].

• •

The presentation of several proofs, definitions and theorem statements in Section 5 and Section 7 has been revised. Additionally, a mistake in [HK22] has been corrected; the original version of $\mathsf{HA}$-coding (cf. [HK22] Hypothesis 2) was not constructively provable, the new one (subsection 7.3) is.

To conclude this introduction, we give a brief overview on the structure of the paper, in the order that we consider most suitable for a first reading:

The main results of the analysis are summarized in Section 8, where we give a tabulated overview on the different variants of Tennenbaum’s theorem that result from the various proofs. It clarifies which assumptions are made for each version, and we give a brief discussion of what to take from these differences. The complete proofs are covered in Section 7, ending with Section 7.4 in which we abstractly capture the essence of Tennenbaum’s theorem.

In Section 6 we motivate and introduce our chosen formulation of Church’s thesis which is utilized as an axiom. Basic results about $\mathsf{PA}$’s standard and non-standard models are shown in Section 4 and then used in Section 5 to establish results that allow the encoding of predicates on $\mathbb{N}$, which are essential in the proof of Tennenbaum’s theorem.

To make the paper self-contained, we also give an introduction to the essential features of constructive type theory, synthetic computability, and the type-theoretic specification of first-order logic in Section 2. This is continued in Section 3 by the presentation of the first-order axiomatization of $\mathsf{PA}$ as given in previous work [KH21, KH23].

2. Preliminaries

2.1. Constructive Type Theory

The chosen framework for this paper is a constructive type theory ($\mathsf{CTT}$). More specifically, it will be the calculus of inductive constructions ($\mathsf{CIC}$) [CH88, PM93] which is implemented in the Coq proof assistant [Coq23]. It provides a predicative hierarchy of type universes above a single impredicative universe $\mathbb{P}$ of propositions and the capability of inductive type definitions. On the type level, we have the unit type $\mymathbb{1}$ with a single element, the void type $\mymathbb{0}$, function spaces $X\to Y$, products $X\times Y$, sums $X+Y$, dependent products222 As is custom in Coq, we write $\forall$ in place of the symbol $\Pi$ for dependent products.

$\forall(x:X).\,A\,x$, and dependent sums $\Sigma(x:X).\,A\,x$. On the propositional level, analogous notions to the one listed for types in the above are present, but denoted by their usual logical notation ($\top$, $\bot$, $\to$, $\land$, $\lor$, $\forall$, $\exists$).333 Negation $\neg A$ is used as an abbreviation for both $A\to\bot$ and $A\to\mymathbb{0}$.

It is important to note that the so-called large eliminations from the impredicative $\mathbb{P}$ into higher types of the hierarchy are restricted. In particular, it is generally not possible to show $(\exists x.\,p\,x)\to\Sigma x.\,p\,x$.444 The direction $(\Sigma x.\,p\,x)\to\exists x.\,p\,x$ is however always provable. Intuitively, one can think of $\exists x.\,p\,x$ as stating the mere existence of a value satisfying $p$, while $\Sigma x.\,p\,x$ is a type that also carries a value satisfying $p$.

The restriction does however allow for large elimination of the equality predicate $=$ of type $\forall X.\,X\to X\to\mathbb{P}$, as well as function definitions by well-founded recursion.

We will also use the basic inductive types of Booleans ($\mathbb{B}:=\mathsf{tt}\mid\mathsf{ff}$), Peano natural numbers ($n:\mathbb{N}:=0\mid n+1$), the option type ($\mathcal{O}{(X)}:={}^{\circ}{x}\mid\emptyset$) and lists ($l:\mathsf{List}{(X)}:={[\,]}\mid x\mathbin{::}l$). Furthermore, by $X^{n}$ we denote the type of vectors $\vec{v}$ of length $n:\mathbb{N}{}$ over $X$.

Given predicates $P,Q\!:\!X\to\mathbb{P}$ on a type $X$, we will occasionally use the set notation $P\subseteq Q$ for expressing $\forall x\!:\!X.\,P\,x\to Q\,x$.

Definition 2.1** ( ).**

[definite] A proposition $P\!:\!\mathbb{P}$ is called definite if $P\lor\neg P$ holds and stable if $\neg\neg P\to P$. The same terminology is used for predicates $p\!:\!X\to\mathbb{P}$ given they are pointwise definite or stable. We furthermore want to recall the following logical principles:

[TABLE]

Note that $LEM$ and $DNE$ are equivalent and not provable in $\mathsf{CIC}$, while $\mathsf{MP}$ is much weaker and has a constructive interpretation [MC17]. For convenience, and as used by Bauer [Bau08], we adapt the reading of double negated statements like $\neg\neg P$ as “potentially $P$”.555 A referee pointed out to us that $\neg\neg P$ is closely related to $\Box\Diamond P$ in modal logic, where $\Box$ stands for necessity and $\Diamond$ for possibility. The statement can therefore also be read as “by necessity, $P$ must be possible”.

Remark \the\ifcsdef{countsame}{dummy}{coqrem} (Handling $\neg\neg$).

Given any propositions $A,B$ we constructively have the equivalence $(A\to\neg B)\leftrightarrow(\neg\neg A\to\neg B)$, meaning that when trying to prove a negated goal, we can remove double negations in front of any assumption. More generally, any statement of the form $\neg\neg A_{1}\to\ldots\to\neg\neg A_{n}\to\neg\neg C$ is equivalent to $A_{1}\to\ldots\to A_{n}\to\neg\neg C$ and since $C\to\neg\neg C$ holds, it furthermore suffices to show $A_{1}\to\ldots\to A_{n}\to C$ in this case. In the following, we will make use of these facts without further notice.

2.2. Synthetic Computability

As already expressed in Section 1, constructive type theory permits us to take a viewpoint that considers all functions to be computable functions, yielding simple definitions [FKS19] of many textbook notions of computability theory:

Definition 2.2** (Enumerability).**

[enumerable] Let $p:X\to\mathbb{P}$ be some predicate. We say that $p$ is enumerable if there is an enumerator $f:\mathbb{N}{}\to\mathcal{O}{(X)}$ such that $\forall x\!:\!X.\,p\,x\leftrightarrow\exists n.\,fn={}^{\circ}{x}$.

Definition 2.3** (Decidability).**

[Dec] Let $p:X\to\mathbb{P}$ be some predicate. We call $f:X\to\mathbb{B}$ a decider for $p$ and write $\mathsf{decider}\,{p}\,{f}$ iff $\forall x\!:\!X.\,p\,x\leftrightarrow fx=\mathsf{tt}$. We then define the following notions of decidability:

• •

$$\mathsf{Dec}${\,p}$ $\mathbin{:=}~\exists f\!:\!X\to$\mathbb{B}$.\,$\mathsf{decider}$\,{p}\,{f}$**

• •

$$\mathsf{dec}{(P\!:\!\mathbb{P})} $\mathbin{:=}~P+\neg P$**.

In both cases we will often refer to the predicate or proposition simply as being decidable.

We also expand the synthetic vocabulary with notions for types. In the textbook setting, many of them can only be defined for sets which are in bijection with $\mathbb{N}$, but synthetically they can be handled in a very uniform way.

Definition 2.4** ( ).**

[Enumerable] We call a type $X$

• •

enumerable* if $\lambda x\!:\!X.\top$ is enumerable,*

• •

discrete* if there exists a decider for equality $=$ on $X$,*

• •

separated* if there exists a decider for apartness $\neq$ on $X$,*

• •

witnessing* if $\forall f\!:\!X\to\mathbb{B}.\,(\exists x.\,fx=\mathsf{tt})\to\Sigma{x}.\,{fx=\mathsf{tt}}$.*

Fact \the\ifcsdef{countsame}{dummy}{coqfact} ( ).

In $\mathsf{CIC}$, the types $N$ and $$\mathbb{N}$^2$ are witnessing. ∎

2.3. First-Order Logic

In order to study Tennenbaum’s theorem, we need to give a description of the first-order theory of $\mathsf{PA}$ and the associated intuitionistic theory of Heyting arithmetic ($\mathsf{HA}$), which has the same axiomatization, but uses intuitionistic first-order logic. We follow prior work in [FKS19, FKW21, KH21] and describe first-order logic as embedded inside the constructive type theory, by inductively defining formulas, terms, and the deduction system. We then define a semantics for this logic, which uses Tarski models and interprets formulas over the respective domain of the model. The type of natural numbers $\mathbb{N}$ will then naturally be a model of $\mathsf{HA}$.

Before specializing to one particular theory, we keep the definition of first-order logic general and fix some arbitrary signature $\Sigma=(\mathcal{F};\mathcal{P})$ for function and predicate symbols.

Definition 2.5** (Terms and Formulas).**

[term] We define terms $t\!:\!\mathsf{tm}$ and formulas $\varphi\!:\!\mathsf{fm}$ inductively:

[TABLE]

where $|f|$ and $|P|$ are the arities of the function symbol $f$ and predicate symbol $P$, respectively.

We use de Bruijn indexing to formalize the binding of variables to quantifiers. This means that the variable $x_{n}$ at some position in a formula is bound to the $n$-th quantifier preceding this variable in the syntax tree of the formula. If there is no quantifier binding the variable, it is said to be free.

Definition 2.6** (Substitution).**

[subst_term] Given a variable assignment $\sigma:\mathbb{N}\to\mathsf{tm}$ we recursively define substitution on terms by $x_{k}[\sigma]\mathbin{:=}\sigma\,k$ and $f\,\vec{v}\mathbin{:=}f(\vec{v}[\sigma])$, and extended to formulas by

[TABLE]

where $\dot{\Box}$ is any logical connective and $\dot{\nabla}$ any quantifier. The variable assignment $x;\sigma$ is defined by $(x;\sigma)\,0\mathbin{:=}x$ as well as $(x;\sigma)(n+1)\mathbin{:=}\sigma\,n$ and simply appends $x$ as the first element to $\sigma\!:\!\mathbb{N}{}\to\mathsf{tm}$. By $\uparrow$ we designate the assignment $\lambda n.\,x_{n+1}$ shifting all variable indices by one.

Definition 2.7** (Natural Deduction).**

*[ ] Natural deduction $\vdash~:$\mathsf{List}{(\mathsf{fm})}\rightarrow\mathsf{fm}$\rightarrow$\mathbb{P}$$ is characterized inductively by the usual rules (see Appendix A). We write $\vdash$ for intuitionistic natural deduction and $\vdash_{c}$ for the classical variant, which extends $\vdash$ by adding every instance of Peirce’s law $((\varphi\to\psi)\to\varphi)\to\varphi$.666 Another way to treat the distinction between classical and intuitionistic theories would be to add all instances of Peirce’s law to the axioms of a theory, instead of building them into the deduction system. *

Definition 2.8** (Tarski Semantics).**

[ ] A model $\mathcal{M}$ consists of a type $D$ designating its domain together with functions ${f}^{\mathcal{M}}:D^{|{f}|}\to D$ and ${P}^{\mathcal{M}}:D^{|{P}|}\to\mathbb{P}$ for all symbols $f$ in $\mathcal{F}$ and $P$ in $\mathcal{P}$. We will also use $\mathcal{M}$ to refer to the domain. Functions $\rho:\mathbb{N}{}\to\mathcal{M}$ are called environments and are used as variable assignments to recursively give evaluations to terms:

[TABLE]

This interpretation is then extended to formulas via the satisfaction relation:

[TABLE]

We say that a formula $\varphi$ holds in the model $\mathcal{M}$ and write $\mathcal{M}\vDash\varphi$ if for every $\rho$ we have ${\mathcal{M}}\vDash_{\rho}{\varphi}$. We extend this notation to theories $\mathcal{T}\!:\!\mathsf{fm}\to\mathbb{P}$ by writing $\mathcal{M}\vDash\mathcal{T}$ iff $\forall\varphi.\,\mathcal{T}\,\varphi\rightarrow\mathcal{M}\vDash\varphi$, and we write $\mathcal{T}\vDash\varphi$ if $\mathcal{M}\vDash\varphi$ for all models $\mathcal{M}$ with $\mathcal{M}\vDash\mathcal{T}$. Given a $e\!:\!\mathcal{M}$, we also use the notation $\mathcal{M}\vDash\varphi(e)$ for all $\rho$ we have $\mathcal{M}\vDash_{e;\rho}\varphi$.

Fact \the\ifcsdef{countsame}{dummy}{coqfact} (Soundness).

For any formula $\varphi$ and theory $\mathcal{T}$, if $\mathcal{T}\vdash\varphi$ then $\mathcal{T}\vDash\varphi$. ∎

From the next section on, we will use conventional notation with named variables instead of explicitly writing formulas with de Bruijn indices.

3. Axiomatization of Peano Arithmetic and Heyting Arithmetic

We present $\mathsf{PA}$ following [KH21], as a first-order theory with a signature consisting of symbols for the constant zero, the successor function, addition, multiplication and equality:

[TABLE]

The finite core of $\mathsf{PA}$ axioms consists of statements characterizing the successor function, as well as addition and multiplication:

[TABLE]

We then get the full (and infinite) axiomatization of $\mathsf{PA}$ with the axiom scheme of induction for unary formulas. In our meta-theory the schema is a type-theoretic function on formulas:

[TABLE]

If instead of the induction scheme we add the axiom $\forall\,x.\,x=0\lor\exists\,y.\,x=Sy$, we get the theory $\mathsf{Q}$ known as Robinson arithmetic. Both $\mathsf{PA}$ and $\mathsf{Q}$ also contain axioms for equality:

[TABLE]

Using classical derivability $\vdash_{c}\,$ we get the classical first-order theory of Peano arithmetic $\mathsf{PA}\vdash_{c}$. Its intuitionistic counterpart $\mathsf{PA}\vdash$ uses intuitionistic derivability $\vdash$ and is called Heyting arithmetic. Given that the constructive type theory selected for this work only provides a model for the intuitionistic theory, we will restrict our focus on Heyting arithmetic. To emphasize this, we will from now on write $\mathsf{HA}$ instead of $\mathsf{PA}$.

For simplicity, we only consider models that interpret the equality symbol with the actual equality relation of its domain, so-called extensional models. In the Coq development we make the equality symbol a syntactic primitive, therefore enabling the convenient behavior that the interpreted equality reduces to actual equality.

Definition 3.9** ( ).**

[num] We recursively define a function $\overline{\,\cdot\,}:$\mathbb{N}${}\rightarrow$\mathsf{tm}$$ by $\overline{0}\mathbin{:=}0$ and $\overline{n+1}\mathbin{:=}S{\overline{n}}$, giving every natural number a representation as a term. Any term $t$ which is of the form $\overline{n}$ will be called numeral.

We furthermore use notations for expressing less than $x<y\mathbin{:=}\exists\,k.\,S(x+k)=y$, less than or equal $x\leq y\mathbin{:=}\exists\,k.\,x+k=y$ and for divisibility $x\mid y\mathbin{:=}\exists\,k.\,x\times k=y$.

The formulas of $\mathsf{HA}$ can be classified in a hierarchy based on their computational properties. We will only consider two levels of this hierarchy:

Definition 3.10** ($\Delta_{1}$ and $\Sigma_{1}$–formulas (cf. [KP23])).**

*[Qdec] A formula $\varphi$ is $\Delta_1$ if for every assignment $\sigma$ that only substitutes closed terms, we have $\mathsf{Q}\vdash\varphi[\sigma]$ or $\mathsf{Q}\vdash\neg\varphi[\sigma]$.

A formula is $\Sigma_1$ if it is of the form $\exists x_{1}\dots\exists x_{n}.\,\varphi_{0}$, where $\varphi_{0}$ is a $\Delta_{1}$–formula.*

Given a $\Sigma_{1}$–formula $\exists x_{1}\ldots\exists x_{n}.\varphi$ where $\varphi$ is $\Delta_{1}$, we can prove it equivalent to the formula $\exists x\,\exists x_{1}<x\ldots\exists x_{n}<x.\,\varphi$. Since $\Delta_{1}$–formulas stay $\Delta_{1}$ if they are closed by a bounded quantifier, this shows that the initial $\Sigma_{1}$–formula can be written as a $\Delta_{1}$–formula, which is preceded by exactly one existential quantifier. We will occasionally make use of this fact and refer to it as

$\Sigma_1$–compression. A more syntactic definition of $\Delta_{1}$ would characterize them as the formulas which are equivalent to both a $\Pi_{1}$ and $\Sigma_{1}$–formula. For our purposes the definition which only stipulates the necessary decidability properties is sufficient, as it implies the absoluteness and completeness properties we will need [KP23]:

Fact \the\ifcsdef{countsame}{dummy}{coqfact} ($\Sigma_{1}$–Completeness).

For any $\Sigma_{1}$–formula $\varphi$ we have $\mathbb{N}\vDash\varphi$ iff $\mathsf{HA}\vdash\varphi$. ∎

Fact \the\ifcsdef{countsame}{dummy}{coqfact} ($\Delta_{1}$–Absoluteness).

Let $\mathcal{M}\vDash\mathsf{HA}$ and $\varphi$ be any closed $\Delta_{1}$–formula, then we have $\mathbb{N}\vDash\varphi\to\mathcal{M}\vDash\varphi$. ∎

4. Standard and Non-standard Models of HA

From now on $\mathcal{M}$ will always designate a $\mathsf{HA}$ model. Any model like this has an interpretation $0^{\mathcal{M}}$ of the zero symbol, as well as an interpretation $S^{\mathcal{M}}{}\!:\!\mathcal{M}\to\mathcal{M}$ of the symbol for the successor. By repeated application of $S^{\mathcal{M}}{}$ we can therefore get the sequence of elements $0^{\mathcal{M}},S^{\mathcal{M}}{}0^{\mathcal{M}},S^{\mathcal{M}}{}S^{\mathcal{M}}{}0^{\mathcal{M}},\ldots$, essentially giving us a copy of the standard numbers inside $\mathcal{M}$. We will now put this intuition more formally.

Fact \the\ifcsdef{countsame}{dummy}{coqfact} ( ).

We recursively define a function $\nu\,{}:$\mathbb{N}${}\to$\mathcal{M}$$ by $\nu\,{0}\mathbin{:=}0^{\mathcal{M}}$ and $\nu\,{(n+1)}\mathbin{:=}S^{\mathcal{M}}{(\nu\,{\,n})}$. Furthermore, we define the predicate {\mathsf{std}{}}\mathbin{:=}\lambda e.\,\exists n.\,\nu\,{n}=e and refer to $e$ as a standard number if $\mathsf{std}{\,e}$ and non-standard if $\neg\,\mathsf{std}{\,e}$. We then have

1. ()

$\hat{\rho}\,{\overline{n}}=\nu\,{n}$* for any $n\!:\!\mathbb{N}{}$ and environment $\rho\!:\!\mathbb{N}\to\mathcal{M}$.* 2. ()

$\nu\,{}$* is an injective homomorphism and therefore an embedding of $\mathbb{N}$ into $\mathcal{M}$.*

Both facts are taken as justification to abuse notation and also write $\overline{n}$ for $\nu\,{n}$. ∎

Usually we would have to write $0^{\mathcal{M}},S^{\mathcal{M}}{},+^{\mathcal{M}},\times^{\mathcal{M}},=^{\mathcal{M}}$ for the interpretations of the respective symbols in a model $\mathcal{M}$. For better readability we will however take the freedom to overload the symbols $0,S,+,\cdot,=$ to also refer to these interpretations.

Definition 4.11** ( ).**

[stdModel’] $\mathcal{M}$ is called a standard model if there is a bijective homomorphism $\varphi:\mathbb{N}\to\mathcal{M}$. We will accordingly write $\mathcal{M}\cong\mathbb{N}$ if this is the case.

We can show that $\nu\,{}$ is essentially the only homomorphism from $\mathbb{N}$ to $\mathcal{M}$ we need to worry about, since it is unique up to extensional equality of functions:

Lemma 4.12** ( ).**

[hom_agree_inu] Let $\varphi:\mathbb{N}\to\mathcal{M}$ be a homomorphism, then $\forall x\!:\!\mathbb{N}.\,\varphi\,x=\nu\,{x}$.

Proof 4.13**.**

By induction on $x$ and using the fact that both are homomorphisms.

We now have two equivalent ways to express standardness of a model.

Lemma 4.14** ( ).**

[stdModel_eqiv] $\mathcal{M}\cong\mathbb{N}$ iff $\forall e\!:\!\mathcal{M}.\,\mathsf{std}{\,e}$.

Proof 4.15**.**

Given $\mathcal{M}\cong\mathbb{N}$, there is an isomorphism $\varphi:\mathbb{N}\to\mathcal{M}$. Since $\varphi$ is surjective, Lemma 4.12 implies that $\nu\,{}$ must also be surjective. For the converse: if $\nu\,{}$ is surjective, it is an isomorphism since it is injective by section 4.

Having seen that every model contains a unique embedding of $\mathbb{N}$, one may wonder whether there is a formula $\varphi$ which could define and pick out precisely the standard numbers in $\mathcal{M}$. Lemma 4.16 gives a negative answer to this question:

Lemma 4.16** ( ).**

[predicate_equiv] There is a unary formula $\varphi(x)$ with \forall e\!:\!\mathcal{M}.\,\big{(}\,\mathsf{std}{\,e}\,\leftrightarrow\,\mathcal{M}\vDash\varphi(e)\,\big{)} if and only if $\mathcal{M}\cong\mathbb{N}{}$.

Proof 4.17**.**

Given a formula $\varphi$ with the stated property, we certainly have $\mathcal{M}\vDash\varphi(\overline{0})$ since $\overline{0}$ is a standard number, and clearly $\mathcal{M}\vDash\varphi(x)\implies\mathsf{std}{\,x}\implies\mathsf{std}{\,(Sx)}\implies\mathcal{M}\vDash\varphi(Sx)$. Thus, by induction in the model, we have $\mathcal{M}\vDash\forall x.\,\varphi(x)$, which is equivalent to $\forall e\!:\!\mathcal{M}.\,\mathsf{std}{\,e}$. The converse implication holds by choosing the formula $x=x$.

We now turn our attention to models which are not isomorphic to $\mathbb{N}$.

Fact \the\ifcsdef{countsame}{dummy}{coqfact} ( ).

For any $e\!:\!\mathcal{M}$, we have $\neg\,\mathsf{std}{\,e}$ iff $\forall n\!:\!\mathbb{N}.~{}e>\overline{n}$. ∎

Definition 4.18** ( ).**

[nonStd] Founded on the result of section 4 we write $e>\mathbb{N}$ iff $\neg\,\mathsf{std}{\,e}$ and call $\mathcal{M}$

• •

non-standard* (written $\mathcal{M}>\mathbb{N}{}$) iff there is $e\!:\!\mathcal{M}$ such that $e>\mathbb{N}$,*

• •

not standard* (written $\mathcal{M}\not\cong\mathbb{N}{}$) iff $\neg\mathcal{M}\cong\mathbb{N}{}$.*

We will also write $e\!:\!\mathcal{M}>\mathbb{N}$ to express that $e$ is a non-standard element in $\mathcal{M}$.

Of course, we have \mathcal{M}$>$\mathbb{N}$\to$\mathcal{M}$\not\cong$\mathbb{N}, but the converse implication does not hold constructively in general, so the distinction of both notions becomes meaningful.

Lemma 4.19** (Overspill).**

[Model.Overspill] If $\mathcal{M}\not\cong\mathbb{N}$ and $\varphi(x)$ is unary with $\mathcal{M}\vDash\varphi(\overline{n})$ for every $n\!:\!\mathbb{N}$, then

1. ()

\neg\,\big{(}\forall e\!:\!\mathcal{M}.\,\mathcal{M}\vDash\varphi(e)\to\mathsf{std}{\,e}\big{)}** 2. ()

$\mathsf{stable}\,{\,\mathsf{std}{}}\to\neg\neg\,\exists\,e>\mathbb{N}.\,\mathcal{M}\vDash\varphi(e)$** 3. ()

$\mathsf{DNE}$* $\to\exists\,e>\mathbb{N}.\,\mathcal{M}\vDash\varphi(e).$*

Proof 4.20**.**

$(1)$* Assuming $\forall e\!:\!\mathcal{M}.~{}\mathcal{M}\vDash\varphi(e)\to\mathsf{std}{\,e}$ and combining it with our assumption that $\varphi$ holds on all numerals, Lemma 4.16 implies $\mathcal{M}\cong\mathbb{N}{}$, giving us a contradiction. For $(2)$ note that we constructively have that $\neg\exists e\!:\!\mathcal{M}.\,\neg\mathsf{std}{\,e}\,\land\,\mathcal{M}\vDash\varphi(e)$ implies $\forall e\!:\!\mathcal{M}.\,\mathcal{M}\vDash\varphi(e)\to\neg\neg\,\mathsf{std}{\,e}$, and by using the stability of $\mathsf{std}{}$ we therefore get a contradiction in the same way as in $(1)$. Statement $(3)$ immediately follows from $(2)$.*

From Lemma 4.19 we learn that under certain conditions, whenever a formula is satisfied on all standard numbers $\overline{n}$, this satisfaction “spills over” into the non-standard part of the model, meaning there is a non-standard element which also satisfies the formula. In the next section, we will encounter our first application of this principle.

5. Coding Finite and Infinite Predicates

There is a standard way in which finite sets of natural numbers can be encoded by a single natural number. Assuming we have some injective function $\pi:\mathbb{N}{}\to\mathbb{N}{}$ whose image consists only of prime numbers, and given a finite set of numbers like $S\mathbin{:=}\{4,13,21,33\}$, we can encode this set by the single number $c\mathbin{:=}\pi_{4}\cdot\pi_{13}\cdot\pi_{21}\cdot\pi_{33}$. It then satisfies $n\in S\leftrightarrow\pi_{n}\mid c$, allowing us to reconstruct $S$ by checking which primes divide $c$.

Instead of applying this to sets, we can also use it to encode bounded portions of predicates on $\mathbb{N}$.

Lemma 5.21** ( ).**

[Coding_nat’] Given $n\!:\!\mathbb{N}$ and any predicate $p:\mathbb{N}\rightarrow\mathbb{P}$ with $\forall x<n.\,p\,x\lor\neg\,p\,x$, we have

[TABLE]

The right part of the conjunction assures that no primes above $\pi_{n}$ end up in the code $c$.

Proof 5.22**.**

We do a proof by induction on $n$. For $n=0$ we can choose $c\mathbin{:=}1$. In the induction step, the induction hypothesis gives us a code $c\!:\!\mathbb{N}{}$ which codes $p$ up to $n$. Since by assumption, $p$ is definite below $Sn$, we know that $p\,n\lor\neg p\,n$, allowing us to consider two cases: If $p\,n$, we set the new code to be $c^{\prime}\mathbin{:=}c\cdot\pi_{n}$, if $\neg p\,n$ we simply set $c^{\prime}\mathbin{:=}c$. In both cases one can now verify that $c^{\prime}$ will correctly code $p$ up to $Sn$.

Corollary 5.23** (Finite Coding in $\mathbb{N}$).**

[Coding_nat] Given any $p:\mathbb{N}\rightarrow\mathbb{P}$ and bound $n\!:\!\mathbb{N}$, we have

[TABLE]

Note that if $p$ is definite, we can drop the $\neg\neg$.

Proof 5.24**.**

If $p$ is definite, we trivially have $\forall x<n.\,p\,x\lor\neg\,p\,x$, so Lemma 5.21 gives us the $\neg\neg$–free existence as claimed. Without assuming definiteness, we can still constructively show $\neg\neg(\forall x<n.\,p\,x\lor\neg\,p\,x)$ by induction on $n$, which combined with Lemma 5.21 gives us the existence, but behind a double negation.

With a proof of the encoding in $\mathbb{N}$ we can give a straightforward proof that this is possible in any model of $\mathsf{HA}$.

Remark \the\ifcsdef{countsame}{dummy}{coqrem} ( ).

To formulate the above result in a generic model $\mathcal{M}\vDash\mathsf{HA}{}$, we require an object-level representation of the prime function $\pi$. For now, we will simply assume that we have such a binary formula $\Pi(x,y)$ and defer the justification to Section 6.

The statement “$\pi_{u}$ divides $c$” can now be expressed by $\exists\,p.~{}\Pi(u,p)\land p\mid c$, for which we will abuse notation and simply write $\Pi(u)\mid c$.

Lemma 5.25** (Finite Coding in $\mathcal{M}$).**

[Coding_model_binary] For any binary formula $\alpha(x,y)$ and $n\!:\!\mathbb{N}{}$ we have

[TABLE]

Proof 5.26**.**

Let $e\!:\!\mathcal{M}$, and define the predicate $p\mathbin{:=}\lambda u\!:\!\mathbb{N}.\,\mathcal{M}\vDash\alpha(\overline{u},e)$. Then Corollary 5.23 potentially gives us a code $a\!:\!\mathbb{N}{}$ for $p$ up to the bound $n$. It now suffices to show that the actual existence of $a\!:\!\mathbb{N}{}$ already implies

[TABLE]

And indeed, we can verify that $c=\overline{a}$ shows the existential claim: given $u\!:\!\mathcal{M}$ with $\mathcal{M}\vDash u<\overline{n}$ we can conclude that $u$ must be a standard number $\overline{u}$. We then have the equivalences

[TABLE]

since $a$ codes $p$ and $\Pi$ represents $\pi$.

Overspill now has interesting consequences when it comes to encoding, as for models that are not standard, it allows for the potential encoding of a complete predicate $p:\mathbb{N}{}\to\mathbb{P}$, and therefore also of infinite subsets.

Lemma 5.27** (Infinite Coding in $\mathcal{M}$).**

[Coding_nonStd_unary] If $\mathsf{std}{}$ is stable, $\mathcal{M}\not\cong\mathbb{N}{}$ and $\alpha(x)$ unary, we have

[TABLE]

Proof 5.28**.**

Using Lemma 5.25 for the present case where $\alpha$ is unary, we get

[TABLE]

for every $n\!:\!\mathbb{N}{}$, so by Lemma 4.19 (Overspill) we get

[TABLE]

where we used that since the equivalence holds for all $u<e$ with $e$ non-standard, it will in particular hold for all $u\!:\!\mathbb{N}$.

Lemma 5.29** ( ).**

[Coding_nonstd_binary] If $\mathsf{std}{}$ is stable and $\mathcal{M}\not\cong\mathbb{N}{}$, then for binary $\alpha(x,y)$ and $e\!:\!\mathcal{M}$ we have

[TABLE]

Proof 5.30**.**

Analogous to the proof of Lemma 5.27.

These coding results allow us to connect a unary formula $\alpha$ to an element $c\!:\!\mathcal{M}$ of the model, in such a way that the decidability of the divisibility for $c$ will entail the decidability of $\mathcal{M}\vDash\alpha(\overline{\,\cdot\,})$.

6. Church’s Thesis for First-Order Arithmetic

Church’s thesis ($\mathsf{CT}$) is an axiom of constructive mathematics which states that every total function is computable. We will assume a version of it in this paper, since by its addition to the ambient type theory, we merely need to show that a function can be defined at all, to prove its computability. This makes it possible to stay completely formal, yet achieve a textbook-style conciseness for proofs involving computability, even in their mechanization.

This addition is not possible in every meta-theory. If we were to add it to $\mathsf{ZF}$, it would immediately imply the computability of the function that solves the halting problem, leading to an inconsistent theory. In general however, theories that tend to the constructive side do allow for the consistent addition of this axiom. In the type theory we use in this paper, this is achieved by strictly distinguishing between functional relations and total functions. The aforementioned function that solves the halting problem in $\mathsf{ZF}$ can only be shown to be a functional relation, which means we can still safely assume total functions to be computable. Currently, there is no consistency proof for $\mathsf{CT}$ (cf. Section 7.1 in [For21b]) and the exact type theory we are using, but there are proofs showing that it can be consistently added to very similar systems [Yam20, SU19].

Since $\mathsf{CT}$ makes reference to computability, its exact form as an axiom does not only depend on the theory in which it is assumed, but also on the model of computation it makes reference to. Robinson’s $\mathsf{Q}$, a finitely axiomatized arithmetical system, is expressive enough to serve as a computational model, and is a particularly well-suited choice in our case, leading us to the following formulation of $\mathsf{CT}$ which we assume for the remainder of the paper:

Axiom \the\ifcsdef{countsame}{dummy}{coqaxiom} ($\mathsf{CT_{Q}}$).

For every function $f:\mathbb{N}\to\mathbb{N}$ there exists a binary $\Sigma_{1}$–formula $\varphi_{f}(x,y)$ such that for every $n\!:\!\mathbb{N}$ we have $\mathsf{Q}\vdash\forall y.\,\varphi_{f}(\overline{n},y)\leftrightarrow\overline{fn}=y$.

Note that $\mathsf{CT_{Q}}$ can be derived from the more conventional version of Church’s thesis for $\mu$-recursive functions [KP23].777 In [KP23], the abbreviation $\mathsf{CT_{Q}}$ was used to refer to a version of Church’s thesis which applies to partial functions. From the partial version, the version for total functions can be derived, and in this paper we use $\mathsf{CT_{Q}}$ to refer to the latter, total version.

Using $\mathsf{CT_{Q}}$ we can get an internal representation $\varphi_{f}$ of any computable function $f$, allowing us to reason about the function inside of first-order arithmetic. We also have an immediate use-case for $\mathsf{CT_{Q}}$, since applying it to the injective prime function $\pi$ lets us settle the earlier section 5:

Fact \the\ifcsdef{countsame}{dummy}{coqfact} ( ).

There is a binary $\Sigma_{1}$–formula representing the injective prime function $\pi$ in $\mathsf{Q}$. ∎

In Section 2.1 we defined decidable and enumerable predicates in a synthetic way, but using $\mathsf{CT_{Q}}$ we can now give characterizations and representations of such predicates by formulas in $\mathsf{Q}$ (cf. [Raa21]).

Definition 6.31** ( ).**

[weak_repr] We call $p:\mathbb{N}\to\mathbb{P}$ weakly representable if there is a $\Sigma_{1}$–formula $\varphi_{p}(x)$ such that $\forall n\!:\!\mathbb{N}.\,p\,n\leftrightarrow\mathsf{Q}\vdash\varphi_{p}(\overline{n})$, and strongly representable if instead, $p\,n\to\mathsf{Q}\vdash\varphi_{p}(\overline{n})$ and $\neg p\,n\to\mathsf{Q}\vdash\neg\varphi_{p}(\overline{n})$ hold for every $n\!:\!\mathbb{N}$.

Lemma 6.32** (Representability Theorem).**

[CT_RTs] Assume $\mathsf{CT_{Q}}$, and let $p:\mathbb{N}\to\mathbb{P}$ be given.

1. ()

If $p$ is decidable, it is strongly representable. 2. ()

If $p$ is enumerable, it is weakly representable.

Proof 6.33**.**

If $p$ is decidable, then there is a decider $\mathbb{N}\to\mathbb{B}$ which can be used to define a function $f\!:\!$\mathbb{N}$\to$\mathbb{N}$$ such that $\forall x\!:\!$\mathbb{N}$.\,p\,x\leftrightarrow fx=0$, and by $\mathsf{CT_{Q}}$ there is a binary $\Sigma_{1}$–formula $\varphi_{f}(x,y)$ representing $f$. We then define $\varphi_{p}(x)\mathbin{:=}\varphi_{f}(x,\overline{0})$ and deduce

[TABLE]

which shows that $p$ is strongly representable.

If $p$ is enumerable, then there is an enumerator $\mathbb{N}\to\mathcal{O}{(\mathbb{N})}$ which can be used to define a function $f:$\mathbb{N}$\to$\mathbb{N}$$ such that $\forall x\!:\!$\mathbb{N}$.\,p\,x\leftrightarrow\exists n.\,fn=x+1$. By $\mathsf{CT_{Q}}$ there is a binary $\Sigma_{1}$–formula $\varphi_{f}(x,y)$ representing $f$. We then define $\varphi_{p}(x)\mathbin{:=}\exists\,n.\,\varphi_{f}(n,Sx)$ giving us

[TABLE]

which shows that $p$ is weakly representable by a $\Sigma_{1}$–formula.

7. Tennenbaum’s Theorem

With our choice of $\mathsf{CTT}+\mathsf{CT_{Q}}$ for the meta-theory in place, we now begin with our analysis of Tennenbaum’s theorem. We will present several proofs of the theorem from the literature. In a classical meta-theory all of these proofs would yield the same result, but in our constructive setting, they turn out to differ in the strength of their assumptions and conclusions. Almost all the proofs will make use of some coding results for non-standard models from Section 5, enabling us to use a single model element to fully encode the standard part of any predicate $p:\mathcal{M}\to\mathbb{P}$.

For the proof in Section 7.1 we will assume enumerability of the model, enabling a very direct diagonal argument [BBJ02]. In Section 7.2 we look at the proof approach that is most prominently found in the literature [Smi14, Kay11] and uses the existence of recursively inseparable sets.

Another refinement of this proof was proposed in a post by Makholm [Mak14] and comes with the advantage that it circumvents the usage of Overspill. Strikingly, it turns out that in the constructive setting, this eliminates the necessity for $\mathsf{MP}$, which is required for the standard proof using inseparable sets. Additionally, we look at the consequences of Tennenbaum’s theorem once the underlying semantics is made explicitly constructive. The latter two variations are discussed in Section 7.3.

7.1. Via a Diagonal Argument

We start by noting that every $\mathsf{HA}$ model can prove the most basic fact about division and remainders.

Lemma 7.34** (Euclid’s Lemma).**

[iEuclid] We have

[TABLE]

and the uniqueness property telling us that if $r_{1},r_{2}<d$ then $q_{1}\cdot d+r_{1}=q_{2}\cdot d+r_{2}$ implies $q_{1}=q_{2}$ and $r_{1}=r_{2}$.

Proof 7.35**.**

For Euclid’s lemma, there is a standard proof by induction on $e$. The uniqueness claim requires some basic results about the strict order.

Lemma 7.36** ( ).**

[dec_div] If $\mathcal{M}$ is enumerable and discrete, then $\lambda(n\!:\!\mathbb{N})(d\!:\!\mathcal{M}).\,\mathcal{M}\vDash\overline{n}\!\mid\!d$ has a decider.

Proof 7.37**.**

*Let $n\!:\!\mathbb{N}$ and $d\!:\!\mathcal{M}$ be given. By Lemma 7.34 we have $\exists q^{\prime},r^{\prime}\!:\!\mathcal{M}.\,d=q^{\prime}\cdot\overline{n}+r^{\prime}$. This existence is propositional, so presently we cannot use it to give a decision for $\overline{n}\mid d$.

Since $M$ is enumerable, there is a surjective function $g:$\mathbb{N}$\to$\mathcal{M}$$ and the above existence therefore shows $\exists q,r\!:\!\mathbb{N}.\,d=(g\,q)\cdot\overline{n}+(g\,r)$. Since equality is decidable in $\mathcal{M}$ and

$$\mathbb{N}$^2$ is witnessing, we get $\Sigma q,r\!:\!\mathbb{N}.\,d=(g\,q)\cdot\overline{n}+(g\,r)$, giving us computational access to $r$, now allowing us to construct the decision. By the uniqueness part of Lemma 7.34 we have $g\,r=0\leftrightarrow\overline{n}\mid d$, so the decidability of $\overline{n}\mid d$ is entailed by the decidability of $g\,r=0$.*

Lemma 7.38** ( ).**

[Stable_std_stable_stdModel]

1. ()

If $\mathsf{std}{}$ is stable, then $\mathcal{M}\cong\mathbb{N}$ is stable. 2. ()

If $\mathsf{std}{}$ is stable, then $\neg\mathcal{M}>\mathbb{N}$ is equivalent to $\mathcal{M}\cong\mathbb{N}$. 3. ()

Assuming $\mathsf{MP}$, if $\mathcal{M}$ is discrete, then $\mathsf{std}{}$ is stable.

Proof 7.39**.**

$(1)$* is trivial by Lemma 4.14. $(2)$ The implication $\forall e.\,\mathsf{std}{\,e}\to\neg\exists e.\,\neg\mathsf{std}{\,e}$ holds constructively, but the converse needs the stability of $\mathsf{std}{}$. For $(3)$, recall that $\mathsf{std}{\,e}$ stands for $\exists n\!:\!\mathbb{N}.\,\overline{n}=e$. Since $\overline{n}=e$ in $\mathcal{M}$ is decidable, stability follows from subsection 2.2.*

Lemma 7.40** ( ).**

[Coding_Dec] If $\mathsf{std}{}$ is stable, $\mathcal{M}\not\cong\mathbb{N}$, and $p\!:\!\mathbb{N}\to\mathbb{P}$ decidable, then potentially there is a code $c\!:\!\mathcal{M}$ such that $\forall n\!:\!\mathbb{N}.~{}p\,n\leftrightarrow\mathcal{M}\vDash\overline{\pi_{n}}\mid c$.

Proof 7.41**.**

By Lemma 6.32, there is a formula $\varphi_{p}$ strongly representing $p$. Under the given assumptions, we can use the coding Lemma 5.27, yielding a code $c\!:\!\mathcal{M}$ for the formula $\varphi_{p}$, such that $\forall u\!:\!\mathbb{N}.\,\mathcal{M}\vDash\varphi_{p}(\overline{u})\leftrightarrow\Pi(\overline{u})\mid c$. Overall this shows:

[TABLE]

Since $p$ is decidable, the latter implication entails $\mathcal{M}\vDash\Pi(\overline{n})\mid c\implies p\,n$, which overall shows the desired equivalence.

This gives us the following version of Tennenbaum’s theorem:

Theorem 7.42** ( ).**

[Tennenbaum_diagonal_ct] Assuming $\mathsf{MP}$ and discrete $\mathcal{M}$, enumerability of $\mathcal{M}$ implies $\mathcal{M}\cong\mathbb{N}$.

Proof 7.43**.**

*By Lemma 7.38 it suffices to show $\neg\neg\mathcal{M}\cong\mathbb{N}$. So assume $\mathcal{M}\not\cong\mathbb{N}$ and try to derive $\bot$.

Given the enumerability, there is a surjective function $g\!:\!$\mathbb{N}$\to$\mathcal{M}$$, allowing us to define the predicate $p\mathbin{:=}\lambda n\!:\!\mathbb{N}.\,\neg\,\mathcal{M}\vDash\overline{\pi_{n}}\mid g\,n$, which is decidable by Lemma 7.36. By the coding result in Lemma 7.40 there is an $e\!:\!\mathcal{M}$ which codes $p$, and by the surjectivity of $g$, there is some $c\!:\!\mathbb{N}$ with $g\,c=e$. Combined, these facts give us*

[TABLE]

leading to the desired contradiction.

7.2. Via Inseparable Predicates

The most frequently reproduced proof of Tennenbaum’s theorem [Kay11, Smi14] uses the existence of recursively inseparable sets and non-standard coding to establish the existence of a non-recursive set.

Definition 7.44** ( ).**

[Insep_pred] A pair $A,B:\mathbb{N}\to\mathbb{P}$ of predicates is called inseparable if they are disjoint and $A\subseteq D$, $B\subseteq\neg D$ implies the undecidability of $D$.

Lemma 7.45** ( ).**

[CT_Insep_pred] There are inseparable enumerable predicates $A,B:\mathbb{N}\to\mathbb{P}$.

Proof 7.46**.**

We use an enumeration $\Phi_{n}:$\mathsf{fm}$$ of formulas to define predicates $A\mathbin{:=}\lambda n\!:\!\mathbb{N}.\,\mathsf{Q}\vdash\neg\,\Phi_{n}(\overline{n})$ and $B\mathbin{:=}\lambda n\!:\!\mathbb{N}.\,\mathsf{Q}\vdash\Phi_{n}(\overline{n})$, which are disjoint since $\mathsf{Q}\not\vdash\bot$, and enumerable since proofs over $Q$ can be enumerated. Given a predicate $D$ with $A\subseteq D$, $B\subseteq\neg D$ and assuming it were decidable, Lemma 6.32 gives us a formula strongly representing $D$, and by the enumeration there is $d\!:\!\mathbb{N}$ such that $\Phi_{d}$ is said formula. Everything together gives us the following chain of implications:

[TABLE]

Since this shows $D\,d\mathbin{\Longleftrightarrow}\neg D\,d$, we must conclude that $D$ is undecidable.

Corollary 7.47** ( ).**

[CT_Insep_form] There is a pair $\alpha,\beta$ of unary $\Sigma_{1}$–formulas such that $A\mathbin{:=}\lambda n\!:\!\mathbb{N}.\,\mathsf{Q}\vdash\alpha(\overline{n})$ and $B\mathbin{:=}\lambda n\!:\!\mathbb{N}.\,\mathsf{Q}\vdash\beta(\overline{n})$ are inseparable and enumerable.

Proof 7.48**.**

Use weak representability (Lemma 6.32) on the predicates given by Lemma 7.45.

Contrary to the proof delineated in Section 7.1, the alternative proof via inseparable sets eliminates the need for enumerability of the model. Furthermore, we will now factor Tennenbaum’s theorem into two parts, mirroring what Kaye does in [Kay11]. He first shows that for any non-standard model $\mathcal{M}$, a non-recursive coded set exists within $\mathcal{M}$, and separately to this, he establishes that computability of the model would entail the recursiveness of all coded sets. Combining both of these results then yields Tennenbaum’s theorem. In the following we will focus on the first part, and establish the existence of an undecidable predicate, which is coded by an element of $\mathcal{M}$. Our coding here concretely uses prime numbers, but in Section 7.4, we will revisit a more abstract perspective on the coding.

Definition 7.49** ( ).**

[Div_nat] For $d\!:\!\mathcal{M}$ define the predicate $\,\overline{\,\cdot\,}\mid{d}\mathbin{:=}\lambda n\!:\!\mathbb{N}.\,\mathcal{M}\vDash\overline{n}\mid d$.

Theorem 7.50** ( ).**

[Tennenbaum_inseparable] Assuming stability of $\mathsf{std}{}$, then $\mathcal{M}>\mathbb{N}$ implies $\neg\neg\exists d\!:\!\mathcal{M}.\,\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{d})}$.

Proof 7.51**.**

*We will assume $\neg\exists d.\,\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{d})}$ and try to reach a contradiction. By Corollary 7.47 there is a pair $\alpha^{\prime},\beta^{\prime}$ of inseparable unary $\Sigma_{1}$–formulas. By

$\Sigma_1$–compression, they can be written in the form $\exists w.\,\alpha(w,x)$ and $\exists w.\,\beta(w,x)$, where $\alpha,\beta$ are $\Delta_{1}$. Since they are disjoint, we have:*

[TABLE]

for every bound $n\!:\!\mathbb{N}$. Due to its bounded quantification, the above formula is also $\Delta_{1}$, allowing us to use $\Delta_{1}$–absoluteness (section 3) to get

[TABLE]

Since we are assuming $\mathcal{M}>\mathbb{N}$, we have $\mathcal{M}\not\cong\mathbb{N}$, which together with the stability of $\mathsf{std}{}$ allows us to use both Overspill (Lemma 4.19) and coding for predicates (Lemma 5.29). Overspill gives us the potential existence of an element $e\!:\!\mathcal{M}>\mathbb{N}$ with

[TABLE]

which shows the disjointness of $\alpha,\beta$ when everything is bounded by $e$. By the coding result, we can get a code $c\!:\!\mathcal{M}$ which satisfies

[TABLE]

Given the above equivalence between $D\mathbin{:=}\lambda n\!:\!\mathbb{N}.\,\mathcal{M}\vDash\exists\,w<e.\,\alpha(w,\overline{n})$ and $\Pi(\overline{\,\cdot\,})\mid c$, our initial assumption $\neg\exists d.\,\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{d})}$ entails that $D$ cannot be undecidable. However, we will now see that $D$ separates the given inseparable formulas:

[TABLE]

which will establish its undecidability.

1. (1)

If $\mathsf{Q}\vdash\exists\,w.\,\alpha(w,\overline{n})$ there is $w\!:\!\mathbb{N}$ with $\mathbb{N}\vDash\alpha(\overline{w},\overline{n})$ and $\mathcal{M}\vDash\alpha(\overline{w},\overline{n})$ by section 3. Since $\overline{w}<e$ we can therefore show $D\,n$. 2. (2)

If $\mathsf{Q}\vdash\exists\,w.\,\beta(w,\overline{n})$ there is $w\!:\!\mathbb{N}$ with $\mathbb{N}\vDash\beta(\overline{w},\overline{n})$ and $\mathcal{M}\vDash\beta(\overline{w},\overline{n})$ by section 3. Assume we had $D\,n$, then there is $v<e$ with $\mathcal{M}\vDash\alpha(v,\overline{n})$, which leads to a contradiction since $\alpha,\beta$ were shown disjoint below $e$.

It leaves us with the contradiction that $D$ is both potentially decidable and undecidable.

7.3. Variants of the Theorem

We now investigate two further variants of the theorem, going back to McCarty [McC87, McC88] and Makholm [Mak14] respectively. They make use of a stronger notion of inseparable formulas, which requires the formulas to be provably disjoint on the object level.

Definition 7.52** ($\mathsf{HA}$-inseparable).**

[def_HA_Insep] A pair of unary formulas $\alpha(x),\beta(x)$ is called $\mathsf{HA}$-inseparable if they are disjoint in the sense of $\mathsf{HA}\vdash\neg\exists\,x.\,\alpha(x)\land\beta(x)$ and if any $D$ with $\mathsf{Q}\vdash\alpha(\overline{\,\cdot\,})\subseteq D$, $\mathsf{Q}\vdash\beta(\overline{\,\cdot\,})\subseteq\neg D$ is undecidable.

According to McCarty [McC88], the existence of $\mathsf{HA}$-inseparable formulas can be established by taking the construction of inseparable formulas as seen in Lemma 7.45, and internalizing the given proof within $\mathsf{HA}$. However, as pointed out in [Pet22] (Fact 6.1), Rosser’s trick [Ros36] can be used to construct the desired $\mathsf{HA}$-inseparable formulas from the inseparable formulas given by Corollary 7.47.

Definition 7.53** (Rosser Formula).**

[rosser] Given any binary formulas $\alpha(t,x)$ and $\beta(t,x)$ we define

[TABLE]

Intuitively, if we interpret $\exists t.\,\alpha(t,x)$ as “There is some time $t$ at which $\alpha(t,x)$ can be verified”, then $(\alpha<\beta)(x)$ expresses that $\alpha(\,\cdot\,,x)$ will be verified before $\beta(\,\cdot\,,x)$.

Lemma 7.54** (Disjointness of Rosser Formulas).**

[rosser_disj] $\mathsf{HA}\vdash\forall x.\,(\alpha<\beta)(x)\to(\beta<\alpha)(x)\to\bot$

Proof 7.55**.**

Our goal is to prove $(\alpha<\beta)(x),\,(\beta<\alpha)(x),\,\mathsf{HA}\vdash\bot$. From the formulas in the context of the derivation, we can conclude that there are terms $t,t^{\prime}$ such that

[TABLE]

From this we get $t^{\prime}<t\land t<t^{\prime}$ and then clearly $\mathsf{HA}\vdash t<t^{\prime}\to t^{\prime}<t\to\bot$.

Lemma 7.56** ($\mathsf{HA}$-inseparable formulas).**

[HA_Insep] There are unary $\mathsf{HA}$-inseparable formulas.

Proof 7.57**.**

*By Corollary 7.47, there are inseparable $\Sigma_{1}$–formulas, and due to

$\Sigma_1$–compression, we can assume they have the form $\alpha^{\prime}(x)=\exists\,w.\,\alpha(w,x)$, $\beta^{\prime}(x)=\exists\,w.\beta(w,x)$, where $\alpha,\beta$ are both $\Delta_{1}$. Since we have the equivalence*

[TABLE]

where the latter formula is $\Delta_{1}$, we can conclude that the Rosser formula $(\alpha<\beta)(x)$ is $\Sigma_{1}$.

*We will now show that

\mathsf{Q}$\vdash\alpha^{\prime}(\overline{n})$ implies \mathsf{Q}$\vdash(\alpha<\beta)(\overline{n})$. From the assumption and soundness we get $w\!:\!\mathbb{N}$ such that $\mathbb{N}\vDash\alpha(\overline{w},\overline{n})$. Since $\alpha^{\prime},\beta^{\prime}$ are inseparable and therefore disjoint, we must have $\mathbb{N}\vDash\neg\beta(\overline{v},\overline{n})$ for every $v\!:\!\mathbb{N}$ and therefore in particular $\mathbb{N}\vDash\forall v.\,\beta(v,\overline{n})\to\overline{w}<v$. Overall this shows $\mathbb{N}\vDash(\alpha<\beta)(\overline{n})$, which by $\Sigma_{1}$–completeness gives $\mathsf{Q}\vdash(\alpha<\beta)(\overline{n})$. With the exact same reasoning we can get the analogous result for $\beta<\alpha$.*

We can now move on to prove that $\alpha<\beta$ and $\beta<\alpha$ constitute a pair of $\mathsf{HA}$-inseparable formulas. The disjointness property follows from the previous Lemma 7.54. Abbreviating any predicate $\lambda n\!:\!\mathbb{N}.\,\mathsf{Q}\vdash\varphi(\overline{n})$ by $\mathsf{Q}\vdash\varphi$, it remains to show that any $D$ satisfying

[TABLE]

is undecidable. By the implications we have just shown above, we get the inclusions

[TABLE]

The undecidability of $D$ therefore follows from the inseparability of the pair $\alpha^{\prime},\beta^{\prime}$.

This stronger disjointness property allows us to easily establish that satisfiability of $\mathsf{HA}$-inseparable formulas is undecidable in any model.

Lemma 7.58** ( ).**

[HA_Insep_undec] If $\alpha,\beta$ are $\mathsf{HA}$-inseparable, then ${\mathcal{M}}\vDash{\alpha}(\overline{\,\cdot\,})$ and ${\mathcal{M}}\vDash{\beta}(\overline{\,\cdot\,})$ are undecidable.

Proof 7.59**.**

Using soundness and the $\mathsf{HA}$-disjointness of $\alpha$ and $\beta$, we get

[TABLE]

Undecidability of ${\mathcal{M}}\vDash{\alpha}(\overline{\,\cdot\,})$ then follows from inseparability of the given formulas (Corollary 7.47), and the same argument also shows the undecidability of ${\mathcal{M}}\vDash{\beta}(\overline{\,\cdot\,})$.

McCarty [McC87, McC88] considers Tennenbaum’s theorem with constructive semantics. Instead of models placed in classical set theory, he works in an intuitionistic theory (e.g. $\mathsf{IZF}$), making the interpretation of the object-level disjunction much stronger. By furthermore assuming $\mathsf{MP}$, he is then able to show that all models of $\mathsf{HA}$ in this constructive setting are standard. To achieve the constructive rendering of disjunctions, we will locally make use of the following choice principle:

Definition 7.60** ( ).**

[UC] By $\mathsf{AUC}$ we denote the principle of unique choice:

[TABLE]

Note that generally, Church’s thesis and unique choice principles combined prove the negation of $\mathsf{LEM}$ (cf. [For21a]), which will make the results that use $\mathsf{AUC}$ (deliberately) anti-classical.

Lemma 7.61** ( ).**

[UC_unary_DN_Dec] If $\mathsf{AUC}$ and $\mathcal{M}>\mathbb{N}$, then there is no unary formula $\alpha$ such that ${\mathcal{M}}\vDash{\alpha}(\overline{\,\cdot\,})$ is undecidable.

Proof 7.62**.**

*Since single instances of the law of excluded middle are provable under double negation, induction on $n$ can be used to prove $\mathcal{M}\vDash\forall\,n.\,\neg\neg\forall\,x<n.\,\alpha(x)\lor\neg\alpha(x)$. Choosing $e\!:\!\mathcal{M}>\mathbb{N}$ for the bound $n$ above, we get $\mathcal{M}\vDash\neg\neg\forall\,x<e.\,\alpha(x)\lor\neg\alpha(x)$ and therefore in particular $\neg\neg\,\forall n\!:\!\mathbb{N}.\,\mathcal{M}\vDash\alpha(\overline{n})\lor\neg\alpha(\overline{n})$, meaning ${\mathcal{M}}\vDash{\alpha}(\overline{\,\cdot\,})$ is potentially definite.

Since $AUC$ entails that definite predicates on $N$ are decidable,

we get $\neg\neg\mathsf{Dec}{({\mathcal{M}}\vDash{\alpha}(\overline{\,\cdot\,}))}$ for all formulas $\alpha$, which implies the non-existence claim.*

Corollary 7.63** ( ).**

[UC_no_nonStd] If $\mathsf{AUC}$, then $\neg\mathcal{M}>\mathbb{N}$.

Proof 7.64**.**

By Lemma 7.56 there exist $\mathsf{HA}$-inseparable formulas, and by Lemma 7.58 their satisfiability is undecidable. This directly contradicts Lemma 7.61.

Theorem 7.65** (McCarty).**

[McCarty] Given $\mathsf{AUC}$ and $\mathsf{MP}$, every model of $\mathsf{HA}$ is standard.888Or another way to put it: $\mathsf{HA}$ is categorical.

Proof 7.66**.**

By Corollary 7.63 we have $\neg\mathcal{M}>\mathbb{N}$. Since $\mathsf{HA}\vdash\forall xy.\,x=y\lor\neg\,x=y$, it follows from $\mathsf{AUC}$ that every model $\mathcal{M}\vDash\mathsf{HA}$ is discrete. Since we also assume $\mathsf{MP}$, Lemma 7.38 $(2)$ now entails $\mathcal{M}\cong\mathbb{N}$.

Now turning to Makholm [Mak14], we will no longer require $\mathsf{AUC}$, but will instead make use of the fact that the coding lemma can be established in $\mathsf{HA}$. While we have proven this result on the level of Coq in Corollary 5.23, we did not mechanize its derivation in the first-order theory $\mathsf{HA}$. To make this transparent, we make its assumption explicit here.

Hypothesis \the\ifcsdef{countsame}{dummy}{coqhyp} ($\mathsf{HA}$-Coding).

*For any unary formula $\alpha(x)$, $\mathsf{HA}$ can internally prove the coding lemma: $\mathsf{HA}\vdash\forall\,n\,\neg\neg\exists\,c\,\forall\,u<n.~{}\alpha(u)\leftrightarrow\Pi(u)\mid c$.999 In the conference paper [HK22], Hypothesis 2 stated that $\mathsf{HA}\vdash\forall\,n\,\exists\,c\,\forall\,u<n.~{}\alpha(u)\leftrightarrow\Pi(u)\mid c$. Contrary to what was claimed, this is not provable for arbitrary formulas $\alpha$. The new formulation of $\mathsf{HA}$-coding solves this mistake through the addition of the double negation. *

Theorem 7.67** (Makholm).**

[Makholm] If $\mathcal{M}>\mathbb{N}$ then $\neg\neg\exists d\!:\!\mathcal{M}.\,\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{d})}$.

Proof 7.68**.**

By Lemma 7.56 there are $\mathsf{HA}$-inseparable unary formulas $\alpha$ and $\beta$. Using soundness and $\mathsf{HA}$-coding we get that $\alpha$ can be coded up to any bound $n\!:\!\mathcal{M}$

[TABLE]

By assumption, there is a non-standard element $e\!:\!\mathcal{M}>\mathbb{N}$, and picking this for the bound $n$, we potentially get a code $c\!:\!\mathcal{M}$ satisfying

[TABLE]

Since the above equivalence holds for all standard numbers $u\!:\!\mathcal{M}$, the undecidability of $\mathcal{M}\vDash\alpha(\overline{\,\cdot\,})$ (Lemma 7.58) entails $\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{c})}$, which shows the existence claim.

Note the quite remarkable fact that in contrast to Theorem 7.50, we do not need to assume $\mathsf{MP}$ or discreteness of the model in order to establish Theorem 7.67.

7.4. Unearthing the Roots of Tennenbaum’s Theorem

In this section, we want to record briefly and mostly informally some general ingredients that seem to go into a proof of Tennenbaum’s theorem.

Taking a look at the proofs of both McCarty and Makholm, we can see a very clear structure. In both of them:

• •

$\mathsf{HA}$-inseparable formulas are used to derive the existence of an undecidable ${\mathcal{M}}\vDash{\alpha}(\overline{\,\cdot\,})$.

• •

Assuming the model has a non-standard element, it is shown that there potentially exists an element with undecidable divisibility on numerals.

In Makholm’s proof the latter point was achieved by usage of the coding result subsection 7.3, which establishes a connection between satisfaction of a formula and divisibility with respect to its code number. Close inspection of the proof of Corollary 5.23 reveals that only two properties of divisibility by primes are needed for it:

[TABLE]

We can abstract away from divisibility and formulate the result as:

Lemma 7.69** ( ).**

[DN_coding] Let $\in~{}\!:\!\mathbb{N}\to\mathbb{N}\to\mathbb{P}$ be a binary predicate satisfying the conditions

1. (1)

$\exists e\,\forall x.\,\neg\,x\in e$*                                (Empty set)* 2. (2)

$\forall n\,c\,\exists c^{\prime}\,\forall x.\,x\in c^{\prime}\leftrightarrow x=n\lor x\in c$*       (Extension),*

which we can interpret as axiomatizing a weak notion of sets. For any predicate $p\!:\!\mathbb{N}\to\mathbb{P}$ we then have $\forall n\,\neg\neg\,\exists c\,\forall u<n.\,p\,u\leftrightarrow u\in c$.

Proof 7.70**.**

Following what we did for Corollary 5.23, it is easier to prove the strengthened statement

[TABLE]

by induction on $n$. The proof then follows the proof of Corollary 5.23. In the base case we make use of the empty set, and in the induction step we do a case distinction on $\neg\neg(p\,n\lor\neg p\,n)$ and utilize the extension property. The details for these steps were checked with Coq.

If we have a binary formula $\varphi_{\in}(x,y)$ satisfying the same conditions inside of $\mathsf{HA}$, we can give a derivation of $\mathsf{HA}\vdash\forall n\,\neg\neg\,\exists c\,\forall u<n.\,\alpha(u)\leftrightarrow\varphi_{\in}(u,c)$ and verbatim run Makholm’s proof. Using $\overline{\,\cdot\,}\in d$ as a shorthand for $\lambda n.\,\mathcal{M}\vDash\varphi_{\in}(\overline{n},d)$ we would then get:

Theorem. If $\mathcal{M}>\mathbb{N}$ then $\neg\neg\exists d\!:\!\mathcal{M}.\,\neg\mathsf{Dec}{(\overline{\,\cdot\,}\in d)}$.

This highlights that the statement of Theorem 7.67 is not inherently tied to divisibility, which is also remarked by Kaye in [Kay11]. It rather seems generally tied to relations that allow the implementation of finite sets or sequences inside of $\mathsf{HA}$. Visser [Vis08] analyzes several axiomatizations of pairs, sets and sequences in first-order theories, and the conditions we have listed above appear as the axioms of the weak set theory $\mathsf{WS}$, which can interpret $\mathsf{Q}$ and is therefore essentially undecidable. This latter point raises an interesting question: One can now wonder if it is decidability of $\overline{\,\cdot\,}\in d$ or $\,\overline{\,\cdot\,}\mid{d}$ respectively, together with the essential undecidability of $\mathsf{WS}$ and $\mathsf{Q}$, which combine to rule out that the model is non-standard.

8. Discussion

8.1. General Remarks

In Section 7, we presented several proofs of Tennenbaum’s theorem which we summarize in the table below, listing their assumptions101010 We do not list the global assumption $\mathsf{CT_{Q}}$. $\mathsf{HA}$-coding (subsection 7.3) was not mechanized in Coq but is provable, which is why we leave it out of the table.

on the left and the conclusion on the right.

First note that in the first row we can clearly show the reverse implication ($\mathcal{M}\cong\mathbb{N}$ implies enumerability). If we additionally assume $\mathsf{MP}$ and discreteness of $\mathcal{M}$, the first two results combined give the equivalences

[TABLE]

Furthermore, we can see that Makholm’s result is a strengthening of the second one, in the sense that it no longer requires $\mathsf{MP}$ nor the discreteness assumption. This becomes possible by the usage of $\mathsf{HA}$-inseparable formulas, overcoming the need for Overspill, which—in the proof of Theorem 7.50—can be identified to be the root for these additional assumptions. In general, we can observe that the results become progressively stronger and less reliant on further assumptions as more and more intermediary results are proven on the object level of $\mathsf{HA}$. For example, instead of using Overspill to establish infinite coding, we later use that the coding lemma holds internally (subsection 7.3). Likewise, using $\mathsf{HA}$-inseparable formulas, instead of inseparable formulas, contributed to another strengthening. This might not be the end of the strengthenings that can be done, as it is remains open whether the constructively stronger $\mathcal{M}>\mathbb{N}\to\exists d.\,\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{d})}$ can also be shown.

As was pointed out by McCarty in [McC88], a weaker version $\mathsf{WCT}$ of $\mathsf{CT}$ suffices for his proof, where the code representing a given function is hidden behind a double negation. He mentions in [McC91] that $\mathsf{WCT}$ is still consistent with the Fan theorem, while $\mathsf{CT}$ is not. Analogously, the following weakening of $\mathsf{CT_{Q}}$ suffices for all of the proofs that we have presented:

Definition 8.71** ($\mathsf{WCT_{Q}}$).**

[WCT_Q] For every function $f:\mathbb{N}\to\mathbb{N}$ there potentially is a binary $\Sigma_{1}$–formula $\varphi_{f}(x,y)$ such that for every $n\!:\!\mathbb{N}$ we have $\mathsf{Q}\vdash\forall y.\,\varphi_{f}(\overline{n},y)\leftrightarrow\overline{fn}=y$.

This only needs few changes of the presented proofs.111111 We could have presented all results with respect to $\mathsf{WCT_{Q}}$. We opted against this in favor of $\mathsf{CT_{Q}}$, to avoid additional handling of double negations and to keep the proofs more readable.

An advantage of $\mathsf{WCT_{Q}}$ over $\mathsf{CT_{Q}}$ is that the former follows from the double negation of the latter and is therefore negative, ensuring that its assumption does not block the reduction of proof-terms found in the mechanization [CDE*+*13].

Depending on the fragment of first-order logic, one can give constructive proofs of the model existence theorem [FKW21], producing a countable syntactic model with computable functions for every consistent theory. By the argument given in the introduction, model existence would yield a countable and computable non-standard model of $\mathsf{PA}$, which at first glance seems to contradict the statement of Tennenbaum’s theorem. For any countable non-standard model of $\mathsf{PA}$ however, Theorem 7.67 and Lemma 7.36 entail that neither equality nor apartness can be decidable. This is similar in spirit to the results in [GH17], showing that even if the functions of the model are computable, non-computable behavior still emerges, but in relation to equality.

8.2. Coq Mechanization

The Coq development is axiom-free and the usage of crucial but constructively justified assumptions $\mathsf{CT_{Q}}$, $\mathsf{MP}$ and $\mathsf{AUC}$ is localized in the relevant sections. Apart from these, there is subsection 7.3 which is taken as an additional assumption in the relevant sections. We have given details as to how this hypothesis can be proven, but since we did not yet mechanize the proof, we wanted to make its assumption on the level of the mechanization very explicit, by labeling it as a hypothesis in the accompanying text.

The development depends on and contributes to a growing collaborative Coq library for first-order logic [KHD*+*22]. Restricting to the files for this project, the line count is roughly 3600 lines of code. From those, 1500 lines on basic results about $\mathbb{N}$ and $\mathsf{PA}$ models were reused from earlier work [KH21]. Notably, the formalization of the various coding lemmas from Section 5 took 470 lines and all variants of Tennenbaum’s theorem together amount to a total of only 800 lines.

8.3. Related Work

Classical proofs of Tennenbaum’s theorem can be found in [BBJ02, Smi14, Kay11]. There are also refinements of the theorem which show that computability of either operation suffices [McA82] or which reduce the argument to a weaker induction scheme [Wil85, CMW82]. Constructive accounts were given by McCarty [McC87, McC88] and Plisko [Pli90], and a relatively recent investigation into Tennenbaum phenomena was conducted by Godziszewski and Hamkins [GH17].

For an account of $\mathsf{CT}$ as an axiom in constructive mathematics we refer to Kreisel [Kre70] and Troelstra [Tro73]. Investigations into $\mathsf{CT}$ and its connections to other axioms of synthetic computability based on constructive type theory were done by Forster [For21a, For22]. While there is no proof for the consistency of $\mathsf{CT}$ in $\mathsf{CIC}$, there are consistency proofs for very similar systems [Yam20, SU19, For22].

Compared to the previous conference paper [HK22], this extended journal version relies on the slightly different definition of $\Sigma_{1}$ and $\Delta_{1}$–formulas used by Kirst and Peters [KP23]. Moreover, they give a derivation of our formulation of $\mathsf{CT_{Q}}$ from a more conventional formulation of Church’s thesis, illustrating that $\mathsf{CT_{Q}}$ is a convenient axiom for sidestepping much of the first-order encoding overhead, while the work needed to formally capture computation within $\mathsf{Q}$ is feasible in its mechanization.

Presentations of first-order logic in the context of proof-checking have already been discussed and used, among others, by Shankar [Sha86], Paulson [paulson2015mechanized], O’Connor [O’C05], as well as Han and van Doorn [HvD20]. We make use of the Coq library for first-order logic [KHD*+*22, HKK21], which has evolved from several previous projects [FKS19, FKW21, KLW20, KH21] and depends on the Coq library of undecidability proofs [FLWD*+*20].

Synthetic computability theory was introduced by Richman and Bauer [Ric83, Bau06] and initially applied to constructive type theory by Forster, Kirst, and Smolka [FKS19]. Their synthetic approach to undecidability results has been used in several other projects, all merged into the Coq library of undecidability proofs [FLWD*+*20].

8.4. Future Work

By relying on the synthetic approach, our treatment of Tennenbaum’s theorem does not explicitly mention the computability of addition or multiplication of the model. To make these assumptions explicit again, and to also free our development from the necessity of adapting this viewpoint, we could assume an abstract version of $\mathsf{CT}$ which makes reference to a $T$ predicate [Kle43, For21a] and is then used to axiomatize $T$-computable functions. Combining this with a version of $\mathsf{CT}$ that stipulates the computability of every $T$-computable function, would then allow us to specifically assume $T$-computability for either addition or multiplication, and to formalize the result that $T$-computability of either operation leads to the model being standard [McA82].

In this work, we have mechanized one of the two hypotheses that remained unmechanized in [HK22], leaving solely the object level coding lemma (subsection 7.3) yet to be mechanized. Achieving this will necessitate the transformation of the proof provided for Corollary 5.23 into a derivation using the axioms of $\mathsf{HA}$. This task will require the establishment of standard results about prime numbers, akin to what we established on the level of Coq’s logic in one of the files. Similar to the mechanization of Lemma 7.56, these proofs will significantly benefit from the proof mode developed in [HKK21]. However, even with the proof mode, the translation of these Coq proofs into derivations entails a substantial amount of engineering work. Our preliminary estimates suggest that this will be a relatively independent project on its own, hence we leave it for future exploration.

A more satisfying rendering of McCarty’s result would be achieved by changing the semantics (Definition 2.8), and putting the interpretations of formulas on the (proof-relevant) type level instead of the propositional level, therefore removing the need to assume $\mathsf{AUC}$ to break the barrier from the propositional to the type level.

Following usual practice in textbooks, we consider the first-order equality symbol as a syntactic primitive and only regard models interpreting it as actual equality in Coq. When treated as axiomatized relation instead, we could consider the (slightly harder to work with) setoid models and obtain the more general result that no computable non-standard setoid model exists.

There are interesting parallels when comparing the proofs of Tennenbaum’s theorem and proofs of the first incompleteness theorem. In particular, we saw that the usage of $\mathsf{HA}$-inseparable sets, and therefore the usage of Rosser’s trick, leads to an improvement of the constructive Tennenbaum result. Connections between the two theorems are well-known [Kay91, Kay11], but it should be interesting to combine the presented work with work like [KP23], to study their connection in a constructive framework. We hope that this work has illustrated the value of such projects, as they can shed new light on old proofs, bringing forward their constructive content.

Acknowledgments

The authors want to thank Yannick Forster, Johannes Hostert, Benjamin Peters, and the anonymous reviewers for their helpful comments and suggestions.

Appendix A Deduction Systems

Intuitionistic natural deduction $\vdash~{}:\mathsf{List}{(\mathsf{fm})}\rightarrow\mathsf{fm}\rightarrow\mathbb{P}$ is defined inductively by the rules

$\begin{gathered}\Gamma\vdash\varphi\varphi\in\Gamma\hskip 30.00005pt\Gamma\vdash\varphi\Gamma\vdash\bot\hskip 30.00005pt\Gamma\vdash\varphi\to\psi\Gamma,\varphi\vdash\psi\hskip 30.00005pt\Gamma\vdash\psi\lx@proof@logical@and\Gamma\vdash\varphi\to\psi\Gamma\vdash\varphi\\[8.5359pt] \Gamma\vdash\varphi\land\psi\lx@proof@logical@and\Gamma\vdash\varphi\Gamma\vdash\psi\hskip 30.00005pt\Gamma\vdash\varphi\Gamma\vdash\varphi\land\psi\hskip 30.00005pt\Gamma\vdash\psi\Gamma\vdash\varphi\land\psi\\[8.5359pt] \Gamma\vdash\varphi\lor\psi\Gamma\vdash\varphi\hskip 30.00005pt\Gamma\vdash\varphi\lor\psi\Gamma\vdash\psi\hskip 30.00005pt\Gamma\vdash\theta\lx@proof@logical@and\Gamma\vdash\varphi\lor\psi\Gamma,\varphi\vdash\theta\Gamma,\psi\vdash\theta\\[8.5359pt] \Gamma\vdash\forall\,\varphi\Gamma[\uparrow]\vdash\varphi\hskip 30.00005pt\vphantom{\forall}\Gamma\vdash\varphi[t]\Gamma\vdash\forall\,\varphi\hskip 30.00005pt\Gamma\vdash\exists\,\varphi\Gamma\vdash\varphi[t]\hskip 30.00005pt\vphantom{\forall\,}\Gamma\vdash\psi\lx@proof@logical@and\Gamma\vdash\exists\,\varphi\Gamma[\uparrow],\varphi\vdash\psi[\uparrow]\end{gathered}$

where $\varphi[t]$ for a term $t$ is a short for $\varphi[\,t;\lambda n.\,x_{n}]$. We get the classical variant $\vdash_{c}$ by adding Peirce’s rule as an axiom:

$\Gamma\vdash_{c}((\varphi\to\psi)\to\varphi)\to\varphi$

The deduction systems lift to possibly infinite contexts $\mathcal{T}:\mathsf{fm}\to\mathbb{P}$ by writing $\mathcal{T}\vdash\varphi$ if there is a finite $\Gamma\subseteq\mathcal{T}$ with $\Gamma\vdash\varphi$.