*This is an extended version of a paper published at FSCD 2022 [HK22].

[a,b] [b]

# An Analysis of Tennenbaum’s Theorem
in Constructive Type Theory*

Marc Hermes0000-0002-0375-759X  and  Dominik Kirst0000-0003-4126-6975
Department of Software Science, Radboud University Nijmegen, Netherlands
<EMAIL_ADDRESS>Universität des Saarlandes, Saarbrücken, Germany
<EMAIL_ADDRESS>
###### 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.

###### Key words and phrases:

first-order logic, Peano arithmetic, Tennenbaum’s theorem, constructive type
theory, Church’s thesis, synthetic computability, Coq

##  1\. Introduction

Classical logic allows for a straightforward proof 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}$ [BBJ02]. To do so,
we start 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,\ldots$ 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 Gauß-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$,
which includes the summation over all natural numbers. The 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 to be considered, $\mathbb{N}$ regains a unique
position:

> Tennenbaum’s Theorem: Apart from form the standard model $\mathbb{N}$, there
> is no countable non-_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 model elements can be realized
by computable functions on these codes. Usually, this 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_ , which states that
every function intuitively computable will be computable in the chosen model.
Proving the computability of a function is then reduced to giving an intuitive
argument for its computability.

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, usage of a constructive meta-theory enables us to
formally add _Church’s thesis_ [Kre70, TvD88, For21] 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, and allowing for straightforward mechanized proofs.

In the 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 constructable
in $\mathsf{CTT}$ by the virtue of its 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 when defining a predicate on $X$ to be _decidable_ ,
if we can show the existence of a function $f\\!:\\!X\to\mathbb{B}$ computing
booleans that reflect the truth values of $p$.

This approach leads to a simplification when it comes to the statement of
Tennenbaum’s theorem itself: In the most natural semantics we can give in
$\mathsf{CTT}$ (where arithmetic operations are interpreted as type-theoretic
functions) all models are now automatically viewed as computable, so we no
longer need “computable model” as part of the theorem statement.

In the sketched framework, we follow the classical presentations of
Tennenbaum’s theorem [Kay11, Smi14] to 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 constructive variant given by
McCarty [McC87, McC88].

Concretely, our contributions can be summarized as follows:

  * •

We review several existing proofs of Tennenbaum’s theorem from the literature.
We present them here, carried out in a constructive meta-theory, and work out
subtle differences in the strengths of their conclusions, which are left
invisible in any classical treatment, but become visible once viewed under a
constructive lense.

  * •

By considering models with a decidable divisibility relation (29), we extend
the theorem to models which must be neither discrete nor enumerable.

  * •

We provide a Coq mechanization covering all the proofs and results that are
presented in this paper, as well as the remaining details.111 The full
mechanization is available on github [Her23] and can conveniently be viewed on
a webpage [HK23]. We make use of two facts for which we gave no mechanized
proofs in Coq. They are therefore clearly marked as “Hypothesis” in the paper
(subsection 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 31. We
have now added a proof of it in Appendix B, solidifying its status as a
hypothesis that can be eliminated from the mechanization.

  * •

We added a discussion (subsection 7.4) in which we try to pin down the main
ingredients used in the derivation of Tennenbaum’s theorem.

  * •

The Coq mechanization has been re-based to depend on a Coq library for first-
order logic [KHD+22]. This enabled us to use existing definitions for
$\Delta_{1}$ and $\Sigma_{1}$-formulas, and more crucially, giving our usage
of $\mathsf{CT_{Q}}$ further justification, as the library contains a
derivation of $\mathsf{CT_{Q}}$ from a more conventional version of Church’s
thesis in [KP23].

  * •

The presentation of several proofs and definitions in section 5 and section 7
have been revised. Additionally, a mistake from [HK22] has been corrected; the
original version of $\mathsf{HA}$-coding was not constructively provable, the
new one 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 we
can get from the varying 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
subsection 7.4 in which we attempt to abstractly capture the essence of what
enables 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].

##  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}$) [CH86, PM93] which is implemented in the Coq
proof assistant [Tea22]. 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 as 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 $=~{}:~{}\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$. 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:

$\displaystyle{\mathsf{LEM}}$ $\displaystyle\mathbin{:=}\forall
P\\!:\\!\mathbb{P}.\,\mathsf{definite}\,{P}\hskip 15.00002pt$ (Law of Excluded
Middle) $\displaystyle{\mathsf{DNE}}$ $\displaystyle\mathbin{:=}\forall
P\\!:\\!\mathbb{P}.\,\mathsf{stable}\,{P}\hskip 15.00002pt$ (Double Negation
Elimination) $\displaystyle{\mathsf{MP}}$ $\displaystyle\mathbin{:=}\forall
f\\!:\\!\mathbb{N}{}\to\mathbb{N}.\,\mathsf{stable}\,{(\exists
n.\,fn=0)}\hskip 15.00002pt$ (Markov’s Principle)

all of which are not provable in $\mathsf{CIC}$. Note that $\mathsf{LEM}$ and
$\mathsf{DNE}$ are equivalent 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 $\neg\neg P$ expresses the impossibility of $P$
being wrong, and therefore representing a guarantee that $P$ can potentially
be shown correct.

######  Remark 1 (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:

[Enumerability] 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}$.

[Decidability] 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. 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 2.

In the particular type theory we use, $\mathbb{N}$ is 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. [Terms
and Formulas] We define terms $t\\!:\\!\mathsf{tm}$ and formulas
$\varphi\\!:\\!\mathsf{fm}$ inductively.

$\displaystyle s,t\\!:\\!\mathsf{tm}$ $\displaystyle\mathbin{::=}x_{n}\mid
f\,\vec{v}\hskip
17.07182pt(n\\!:\\!\mathbb{N},~{}f\\!:\\!\mathcal{F},~{}\vec{v}\\!:\\!{\mathsf{tm}}^{|{f}|})$
$\displaystyle\alpha,\beta\\!:\\!\mathsf{fm}$
$\displaystyle\mathbin{::=}\bot\mid
P\,\vec{v}\mid\alpha\to\beta\mid\alpha\land\beta\mid\alpha\lor\beta\mid\forall\,\alpha\mid\exists\,\beta\hskip
17.07182pt(P\\!:\\!\mathcal{P},~{}\vec{v}\\!:\\!{\mathsf{tm}}^{|{P}|}).$

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_. [Substitution] 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

$\bot[\sigma]\mathbin{:=}\bot\hskip
13.99995pt(P\,\vec{v})[\sigma]\mathbin{:=}P\,(\vec{v}[\sigma])\hskip
13.99995pt(\alpha~{}\dot{\Box}~{}\beta)[\sigma]\mathbin{:=}\alpha[\sigma]~{}\dot{\Box}~{}\beta[\sigma]\hskip
13.99995pt(\dot{\nabla}\,\varphi)[\sigma]\mathbin{:=}\dot{\nabla}(\varphi[x_{0};\lambda
x.(\sigma x)[\uparrow]])$

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

[Natural Deduction] Natural deduction
$\vdash~{}:(\mathsf{fm}\to\mathbb{P})\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$.

[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:

$\displaystyle\hat{\rho}\,{x_{k}}\mathbin{:=}\rho\,k\hskip
30.00005pt\hat{\rho}\,{(f\,\vec{v})}\mathbin{:=}{f}^{\mathcal{M}}(\hat{\rho}\,{\vec{v}})\hskip
25.00003pt(v\\!:\\!{\mathsf{tm}}^{n})$

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

$\displaystyle{\mathcal{M}}\vDash_{\rho}{P\,\vec{v}}~{}$
$\displaystyle\mathbin{:=}~{}{P}^{\mathcal{M}}(\hat{\rho}\,{\vec{v}})$
$\displaystyle{\mathcal{M}}\vDash_{\rho}{\alpha\to\beta}~{}$
$\displaystyle\mathbin{:=}~{}{\mathcal{M}}\vDash_{\rho}{\alpha}\to{\mathcal{M}}\vDash_{\rho}{\beta}$
$\displaystyle{\mathcal{M}}\vDash_{\rho}{\alpha\land\beta}~{}$
$\displaystyle\mathbin{:=}~{}{\mathcal{M}}\vDash_{\rho}{\alpha}\land{\mathcal{M}}\vDash_{\rho}{\beta}$
$\displaystyle\hskip 30.00005pt{\mathcal{M}}\vDash_{\rho}{\alpha\lor\beta}~{}$
$\displaystyle\mathbin{:=}~{}{\mathcal{M}}\vDash_{\rho}{\alpha}\lor{\mathcal{M}}\vDash_{\rho}{\beta}$
$\displaystyle{\mathcal{M}}\vDash_{\rho}{\forall\,\alpha}~{}$
$\displaystyle\mathbin{:=}~{}\forall
x\\!:\\!D.~{}{\mathcal{M}}\vDash_{x;\rho}{\alpha}$
$\displaystyle{\mathcal{M}}\vDash_{\rho}{\exists\,\alpha}~{}$
$\displaystyle\mathbin{:=}~{}\exists
x\\!:\\!D.~{}{\mathcal{M}}\vDash_{x;\rho}{\alpha}$

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}$.

######  Fact 3 (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

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:

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

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

Disjointness: $\displaystyle{\forall\,}x.\,Sx=0\to\bot$ Injectivity:
$\displaystyle{\forall\,}xy.\,Sx=Sy\to x=y$ $\displaystyle{+\text{-base: }}$
$\displaystyle{\forall\,}x.\,0+x=x$ $\displaystyle{+\text{-recursion: }}$
$\displaystyle{\forall\,}xy.\,(Sx)+y=S(x+y)$ $\displaystyle{\times\text{-base:
}}$ $\displaystyle{\forall\,}x.\,0\times x=0$
$\displaystyle{\times\text{-recursion: }}$
$\displaystyle{\forall\,}xy.\,(Sx)\times y=y+x\times y$

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:

${\lambda\varphi.\,\varphi[0]\to(\forall\,x.\,\varphi[x]\to\varphi[Sx])\to\forall\,x.\,\varphi[x]}$

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:

Reflexivity: $\displaystyle{\forall\,}x.\,x=x$ Symmetry:
$\displaystyle{\forall\,}xy.\,x=y\to y=x$ Transitivity:
$\displaystyle{\forall\,}xyz.\,x=y\to y=z\to x=z$
$\displaystyle{S\text{-equality: }}$ $\displaystyle{\forall\,}xy.\,x=y\to
Sx=Sy$ $\displaystyle{+\text{-equality: }}$
$\displaystyle{\forall\,}xyuv.\,x=u\to y=v\to x+y=u+v$
$\displaystyle{\times\text{-equality: }}$
$\displaystyle{\forall\,}xyuv.\,x=u\to y=v\to x\times y=u\times v$

The classical first-order theory of Peano arithmetic is described by
$\mathsf{PA}{}\vdash_{c}\,$, while its intuitionistic counterpart – Heyting
arithmetic – is given by $\mathsf{PA}\vdash\,$.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.  Since the constructive type theory we have chosen
to work in only gives us a model for Heyting arithmetic, we will only work
with the intuitionistic theory $\mathsf{PA}\vdash\,$. 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. Note that in the Coq development we even make the equality symbol a
syntactic primitive, therefore enabling the convenient behavior that the
interpreted equality reduces to actual equality.

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 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:
[$\Delta_{1}$ and $\Sigma_{1}$-formulas (cf. [KP23])] A formula $\varphi$ is
$\Delta_{1}$ if for every substitution $\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$, which shows that it can be
written as a $\Delta_{1}$-formula, which is proceeded 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 4 ($\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$. ∎

######  Fact 5 ($\Sigma_{1}$-Completeness).

For any $\Sigma_{1}$-formula $\varphi$ we have $\mathbb{N}\vDash\varphi$ iff
$\mathsf{HA}\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 6.

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.\overline{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. (1)

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

  2. (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. $\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 functional extensionality:

######  Lemma 7.

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

######  Proof 4.1.

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

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

######  Proof 4.2.

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

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}$. 9 gives a negative answer
to this question:

######  Lemma 9.

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

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

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

Founded on the result of 10 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 the existence
of a non-standard element $e$ 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 11 (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. (1)

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

  2. (2)

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

  3. (3)

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

######  Proof 4.4.

$(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, 9
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 11 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 are present in $c$.

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

######  Lemma 12.

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

$\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{)}$

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

######  Proof 5.1.

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 13 (Finite Coding in $\mathbb{N}$).

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

$\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{)}$

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

######  Proof 5.2.

If $p$ is definite, we trivially have $\forall x<n.\,p\,x\lor\neg\,p\,x$, so
12 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 12 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 14.

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 15 (Finite Coding in $\mathcal{M}$).

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

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

######  Proof 5.3.

Let $e\\!:\\!\mathcal{M}$, and define the predicate $p\mathbin{:=}\lambda
u\\!:\\!\mathbb{N}.\,\mathcal{M}\vDash\alpha(\overline{u},e)$. Then 13
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

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

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

$\displaystyle\mathcal{M}\vDash\alpha(\overline{u},e)~{}\mathbin{\Longleftrightarrow}~{}p\,u~{}\mathbin{\Longleftrightarrow}~{}\pi_{u}\mid
a~{}\mathbin{\Longleftrightarrow}~{}\mathcal{M}\vDash\Pi(\overline{u})\mid\overline{a}$

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 the potential encoding of a complete
predicate $p:\mathbb{N}{}\to\mathbb{P}$, and therefore also of infinite
subsets.

######  Lemma 16 (Infinite Coding in $\mathcal{M}$).

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

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

######  Proof 5.4.

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

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

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

$\displaystyle\neg\neg\,\exists\,e>\mathbb{N}.~{}\mathcal{M}\vDash\neg\neg\,\exists\,c\,\forall\,u<e.~{}\alpha(u)\leftrightarrow\Pi(u)\mid
c$ $\displaystyle\implies~{}$ $\displaystyle\neg\neg\,\exists
c\\!:\\!\mathcal{M}\,\forall
u\\!:\\!\mathbb{N}.~{}\mathcal{M}\vDash\alpha(\overline{u})\leftrightarrow\Pi(\overline{u})\mid
c.$

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

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

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

######  Proof 5.5.

Analogous to the proof of 16.

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 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 of proofs involving computability, even in their mechanization.

It is not safe to add a strong statement like this to just any 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. There currently is no consistency proof for $\mathsf{CT}$ 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, For22].

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. $\mathsf{Q}$ as a 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 18 ($\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$.

Using $\mathsf{CT_{Q}}$ we can get an internal representation $\varphi_{f}$ of
any computable function $f$, allowing us to argue and reason about the
function inside of first-order arithmetic. As a further justification for the
validity of this version, we want to note that it can be derived from a more
common version of Church’s thesis for $\mu$-recursive functions [KP23].777 In
[KP23], the abbreviation $\mathsf{CT_{Q}}$ was used to refer for a version of
Church’s thesis which applies to partial functions. From it, version for total
functions was derived, which is what we refer to as $\mathsf{CT_{Q}}$.  We
also have an immediate use-case for $\mathsf{CT_{Q}}$, since applying it on
the injective prime function $\pi$ lets us settle the earlier 14:

######  Fact 19.

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

Since we defined decidable and enumerable predicates in subsection 2.1 by
reference to computable functions, we can use $\mathsf{CT_{Q}}$ to give
characterizations and representations of such predicates by formulas in
$\mathsf{Q}$ [Raa21]. 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
$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 20 (Representability Theorem ($\mathsf{RT}$)).

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

  1. (1)

If $p$ is decidable, it is strongly representable.

  2. (2)

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

######  Proof 6.1.

If $p$ is decidable, then there is 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

$\displaystyle p\,n$ $\displaystyle\implies$ $\displaystyle fn=0$
$\displaystyle\implies$
$\displaystyle\mathsf{Q}\vdash\overline{fn}=\overline{0}$
$\displaystyle\implies$
$\displaystyle\mathsf{Q}\vdash\varphi_{f}(\overline{n},\overline{0})$
$\displaystyle\implies$
$\displaystyle\mathsf{Q}\vdash\varphi_{p}(\overline{n})$ $\displaystyle\neg
p\,n$ $\displaystyle\implies$ $\displaystyle fn\neq 0$ $\displaystyle\implies$
$\displaystyle\mathsf{Q}\vdash\neg(\overline{fn}=\overline{0})$
$\displaystyle\implies$
$\displaystyle\mathsf{Q}\vdash\neg\varphi_{f}(\overline{n},\overline{0})$
$\displaystyle\implies$
$\displaystyle\mathsf{Q}\vdash\neg\varphi_{p}(\overline{n})$

which shows that $p$ is strongly representable.

If $p$ is enumerable, then there is $f:\mathbb{N}\to\mathbb{N}$ such that
$\forall x\\!:\\!\mathbb{N}.\,p\,x\leftrightarrow\exists n.\,fn=x+1$ 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{:=}\exists\,n.\,\varphi_{f}(n,Sx)$ giving us

$\displaystyle\mathsf{Q}\vdash\varphi_{p}(\overline{x})~{}$
$\displaystyle\Longleftrightarrow~{}\mathsf{Q}\vdash\exists\,n.\,\varphi_{f}(n,S\overline{x})\Longleftrightarrow~{}\exists
n\\!:\\!\mathbb{N}.\,\mathsf{Q}\vdash\varphi_{f}(\overline{n},S\overline{x})$
$\displaystyle\Longleftrightarrow~{}\exists
n\\!:\\!\mathbb{N}.\,\mathsf{Q}\vdash\overline{fn}=S\overline{x}\Longleftrightarrow~{}\exists
n\\!:\\!\mathbb{N}.\,fn=x+1~{}\Longleftrightarrow~{}p\,x$

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 encode all the values of a predicate $p:\mathcal{M}\to\mathbb{P}$ on the
standard part $\mathbb{N}$ of the model.

The proof in subsection 7.1 we will assume enumerability of the model,
enabling a very direct diagonal argument [BBJ02]. In subsection 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 variant of this proof was proposed in a post by Makholm [Mak14] and
comes with the advantage that it circumvents the usage of Overspill. 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. Lastly we look at the consequences of Tennenbaum’s theorem, once the
underlying semantics is made explicitly constructive. The latter two
variations are discussed in subsection 7.3.

###  7.1. Via a Diagonal Argument

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

######  Lemma 21 (Euclidean Lemma).

Given $e,d\\!:\\!\mathcal{M}$ we have

$\mathcal{M}\vDash\exists\,r\,q.~{}e=q\cdot d+r~{}\land~{}(0<d\to r<d)$

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

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

######  Lemma 22.

If $\mathcal{M}$ is enumerable and discrete, then $\lambda
nd.\,\mathcal{M}\vDash\overline{n}\mid d$ has a decider.

######  Proof 7.2.

Let $n\\!:\\!\mathbb{N}$ and $d\\!:\\!\mathcal{M}$ be given. By the Euclidean
21 we have $\exists q,r\\!:\\!\mathcal{M}.\,d=q\cdot\overline{n}+r$. This
existence is propositional, so presently we cannot use it to give a decision
for $\overline{n}\mid d$. Since $\mathcal{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 21 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 23.

  1. (1)

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

  2. (2)

Assuming $\mathsf{MP}$ and discreteness of $\mathcal{M}$, then
$\mathsf{std}{}$ is stable.

######  Proof 7.3.

The first statement is trivial by 8. For the second, 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
2.

######  Lemma 24.

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

By $\mathsf{RT}$, there is a formula $\varphi_{p}$ strongly representing $p$.
Under the given assumptions, we can use the coding 16, 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:

$\displaystyle p\,n$
$\displaystyle\implies\mathsf{Q}\vdash\varphi_{p}(\overline{n})$
$\displaystyle\implies$
$\displaystyle\mathcal{M}\vDash\varphi_{p}(\overline{n})$
$\displaystyle\implies$ $\displaystyle\mathcal{M}\vDash\Pi(\overline{n})\mid
c$ $\displaystyle\neg p\,n$
$\displaystyle\implies\mathsf{Q}\vdash\neg\,\varphi_{p}(\overline{n})$
$\displaystyle\implies$ $\displaystyle\neg\,$
$\displaystyle\mathcal{M}\vDash\varphi_{p}(\overline{n})$
$\displaystyle\implies$ $\displaystyle\neg\,$
$\displaystyle\mathcal{M}\vDash\Pi(\overline{n})\mid c.$

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

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

######  Proof 7.5.

By 23 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 22. By the coding result in 24 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

$\displaystyle\neg\,\mathcal{M}\vDash\overline{\pi_{c}}\mid
g\,c~{}\stackrel{{\scriptstyle\text{def.}}}{{\mathbin{\Longleftrightarrow}}}~{}p\,c~{}\stackrel{{\scriptstyle\text{\text{coding}}}}{{\mathbin{\Longleftrightarrow}}}~{}\mathcal{M}\vDash\overline{\pi_{c}}\mid
g\,c$

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. A pair
$A,B:\mathbb{N}\to\mathbb{P}$ of predicates is called _inseparable_ if they
are disjoint and $A\subseteq D\subseteq\neg B$ implies the undecidability of
$D$.

######  Lemma 26.

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

######  Proof 7.6.

We use an enumeration $\Phi_{n}:\mathsf{fm}$ of formulas to define disjoint
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})$. Since proofs
over $\mathsf{Q}$ can be enumerated, $A$ and $B$ are enumerable. Assuming a
predicate $D$ satisfying $A\subseteq D\subseteq\neg B$ were decidable,
$\mathsf{RT}$ would give us a formula strongly representing $D$, and by the
enumeration there is $d\\!:\\!\mathbb{N}$ such that $\Phi_{d}$ is said
formula. Since $D\subseteq\neg B$ is equivalent to $B\subseteq\neg D$ this
gives us the following chain of implications:

$\displaystyle
D\,d\stackrel{{\scriptstyle\text{s.repr.}}}{{\implies}}\mathsf{Q}\vdash\Phi_{d}(\overline{d})\stackrel{{\scriptstyle\text{def.}}}{{\implies}}B\,d\stackrel{{\scriptstyle\subseteq}}{{\implies}}\neg
D\,d\stackrel{{\scriptstyle\text{s.repr.}}}{{\implies}}\mathsf{Q}\vdash\neg\Phi_{d}(\overline{d})\stackrel{{\scriptstyle\text{def.}}}{{\implies}}A\,d\stackrel{{\scriptstyle\subseteq}}{{\implies}}D\,d$

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

######  Corollary 27.

There is a pair $\alpha(x),\beta(x)$ 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.7.

Use weak representability (20) on the predicates given by 26.

Unlike the proof in subsection 7.1, which needed enumerability of the model,
the proof via inseparable sets allows for a characterization of
$\mathcal{M}\cong\mathbb{N}$ which only makes reference to the decidability of
divisibility by numerals: For $d\\!:\\!\mathcal{M}$ define the predicate
$\,\overline{\,\cdot\,}\mid{d}\mathbin{:=}\lambda
n\\!:\\!\mathbb{N}.\,\mathcal{M}\vDash\overline{n}\mid d$.

######  Theorem 28.

Assuming stability of $\mathsf{std}{}$, then $\forall
d\\!:\\!\mathcal{M}.\,\neg\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{d})}$
implies $\neg\neg\mathcal{M}\cong\mathbb{N}$.

######  Proof 7.8.

With the goal of reaching a contradiction, we assume
$\mathcal{M}\not\cong\mathbb{N}$ and the potential decidability of
$\,\overline{\,\cdot\,}\mid{d}$ for any $d\\!:\\!\mathcal{M}$. By 27 there is
a pair $\alpha^{\prime},\beta^{\prime}$ of inseparable unary $\Sigma_{1}$
formulas. By a compression result for $\Sigma_{1}$ formulas, 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:

$\mathbb{N}\vDash\forall\,x\,w\,v<\overline{n}.~{}\alpha(w,x)\to\beta(v,x)\to\bot$

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 (4) to get

$\mathcal{M}\vDash\forall\,x\,w\,v<\overline{n}.~{}\alpha(w,x)\to\beta(v,x)\to\bot$

Since we have stability of $\mathsf{std}{}$ and
$\mathcal{M}\not\cong\mathbb{N}$ by assumption, we can make use of both
Overspill (11) and coding for predicates (17). Overspill gives us the
potential existence of an element $e\\!:\\!\mathcal{M}$ with

$\mathcal{M}\vDash\forall\,x\,w\,v<e.~{}\alpha(w,x)\to\beta(v,x)\to\bot$

which shows the disjointness of $\alpha,\beta$ when everything is bounded by
$e$. By the coding result, we can take the predicate
$D\,n\mathbin{:=}\mathcal{M}\vDash\exists\,w<e.\,\alpha(w,\overline{n})$ and
get a code $c\\!:\\!\mathcal{M}$ which satisfies

$\displaystyle\forall
u\\!:\\!\mathbb{N}.~{}\mathcal{M}\vDash(\exists\,w<e.\,\alpha(w,\overline{u}))\leftrightarrow\Pi(\overline{u})\mid
c$

Since divisibility for $c$ is potentially decidable, the same therefore holds
for $D$. However, we will now see that $D$ also sits in between the
inseparable formulas:

$\displaystyle\mathsf{Q}\vdash\exists\,w.\,\alpha(w,\overline{\,\cdot\,})~{}\stackrel{{\scriptstyle\text{(1)}}}{{\subseteq}}~{}D~{}\stackrel{{\scriptstyle\text{(2)}}}{{\subseteq}}~{}\neg\,\mathsf{Q}\vdash\exists\,w.\,\beta(w,\overline{\,\cdot\,})$

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 4. Since
$\overline{w}<e$ we can therefore show $D\,n$.

  2. (2)

Assuming $D\,n$, there is $w<e$ with
$\mathcal{M}\vDash\alpha(w,\overline{n})$. Since $\alpha,\beta$ were shown
disjoint below $e$, we must have
$\neg\,\mathcal{M}\vDash\beta(w,\overline{n})$ and therefore
$\neg\,\mathsf{Q}\vdash\exists\,w.\,\beta(w,\overline{n})$ by soundness.

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

By usage of 23, we then get:

######  Corollary 29.

Assuming $\mathsf{MP}$ and discreteness of $\mathcal{M}$, we have that
$\forall
d\\!:\\!\mathcal{M}.\,\neg\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{d})}$
implies $\mathcal{M}\cong\mathbb{N}$. ∎

###  7.3. Variants of the Theorem

We now investigate two further variants of the theorem, going back to McCarty
[McC88, McC87] and Makholm [Mak14] respectively. They both make use of the
fact that the inseparable formulas we have used so far can produce inseparable
formulas which are disjoint on the object level. This stronger property allows
us to easily establish that their satisfiability in any model is undecidable.
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\subseteq\neg\mathsf{Q}\vdash\beta(\overline{\,\cdot\,})$ is undecidable.

######  Lemma 30.

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

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

$\mathsf{Q}\vdash\alpha(\overline{n})~{}\stackrel{{\scriptstyle\text{sound}}}{{\Longrightarrow}}~{}\mathcal{M}\vDash\alpha(\overline{n})~{}\stackrel{{\scriptstyle\mathsf{HA}\text{-disj.}}}{{\Longrightarrow}}~{}\neg\mathcal{M}\vDash\beta(\overline{n})~{}\stackrel{{\scriptstyle\text{sound}}}{{\Longrightarrow}}~{}\neg\mathsf{Q}\vdash\beta(\overline{n}).$

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

According to McCarty [McC88], the existence of $\mathsf{HA}$-inseparable
formulas can be established by taking the construction of inseparable formulas
as seen in 26, and internalizing the given proof within $\mathsf{HA}$.
However, as pointed out in [Pet22] (Fact 6.1), Rosser’s trick can be used to
construct the desired $\mathsf{HA}$-inseparable formulas from the inseparable
formulas given in subsection 7.2. We did not mechanize the latter proof, but
have added it to Appendix B for completeness. Since we want the paper to
accurately reflect the state of the Coq mechanization, we will list it as an
explicit assumption here.

######  Hypothesis 31 ($\mathsf{HA}$-inseparable formulas).

There is a pair of unary $\mathsf{HA}$-inseparable formulas.

McCarty [McC88, McC87] considered 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: By $\mathsf{AUC}$
we denote the principle of unique choice:

$\forall X\,Y\,R.\,(\forall x\,\exists!y.\,Rxy)\to\exists f\\!:\\!X\to
Y.\,\forall x.\,Rx(fx)$

Note that $\mathsf{CT}$ and $\mathsf{AUC}$ combined prove the negation of
$\mathsf{LEM}$888See the discussion in [For21]., which will make the results
that use $\mathsf{AUC}$ (deliberately) anti-classical.

######  Lemma 32.

Assuming $\mathsf{AUC}$ and given $e\\!:\\!\mathcal{M}>\mathbb{N}$, we have
$\neg\neg\mathsf{Dec}{({\mathcal{M}}\vDash{\alpha}(\overline{\,\cdot\,}))}$
for any unary formula $\alpha$.

######  Proof 7.10.

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 the non-standard number $e$ 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 $\mathsf{AUC}$ implies that definite predicates on
$\mathbb{N}$ are decidable, the claim follows.

######  Corollary 33 (McCarty).

Given $\mathsf{AUC}$ and $\mathsf{MP}$, $\mathsf{HA}$ is categorical.

######  Proof 7.11.

Given that $\mathsf{HA}\vdash\forall xy.\,x=y\lor\neg\,x=y$, $\mathsf{AUC}$
entails the discreteness of every model $\mathcal{M}\vDash\mathsf{HA}$. Using
$\mathsf{MP}$ and 23, this entails stability of $\mathsf{std}{}$ and
$\mathcal{M}\cong\mathbb{N}$, giving us

$\mathcal{M}\cong\mathbb{N}~{}\Longleftarrow~{}\neg\neg\mathcal{M}\cong\mathbb{N}~{}\stackrel{{\scriptstyle\mathsf{MP}}}{{\Longleftarrow}}~{}\neg\mathcal{M}>\mathbb{N}$

where we can now prove the rightmost statement to finish: Assume we had
$\mathcal{M}>\mathbb{N}$, then by 30 and 32 we immediately get a
contradiction.

Now turning to Makholm, we will no longer require $\mathsf{AUC}$, but will
instead make use of the fact that the coding result establish in 13 can be
derived in $\mathsf{HA}$. We did not mechanize the proof of this statement, so
we again make its assumption explicit here.

######  Hypothesis 34 ($\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], the hypothesis 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 version solves this mistake through the presence of the
double negation.

######  Theorem 35 (Makholm).

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

######  Proof 7.12.

Assuming $\mathcal{M}>\mathbb{N}$ we aim to derive a contradiction. By 31
there are $\mathsf{HA}$-inseparable unary formulas $\alpha$ and $\beta$. Using
soundness on $\mathsf{HA}$-coding we get that $\alpha$ can be coded up to any
bound $n\\!:\\!\mathcal{M}$

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

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

$\mathcal{M}\vDash\forall\,u<e.\,\alpha(u)\leftrightarrow\Pi(u)\mid c.$

Since the above equivalence holds for all standard numbers
$u\\!:\\!\mathcal{M}$, the potential decidability of
$\,\overline{\,\cdot\,}\mid{c}$ entails the potential decidability of
$\mathcal{M}\vDash\alpha(\overline{\,\cdot\,})$, contradicting however its
undecidability, which follows from 30.

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

###  7.4. Unearthing the Roots of Tennenbaum’s Theorem

The proofs by McCarty and Makholm have 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\,})$.

  * •

Some assumption which stipulates some computability in the model is used to
show that in a non-standard model all predicates of the form
${\mathcal{M}}\vDash{\alpha}(\overline{\,\cdot\,})$ are after all
(potentially) decidable.

In Makholm’s proof the latter point was achieved by usage of the coding result
13, which is used to make the connection between satisfaction of a formula and
divisibility with respect to its code number. Inspecting the proof of the
coding lemma, we can see that any kind of binary relation will do, as long as
it satisfies two conditions.

######  Lemma 36.

Given a binary predicate $\in~{}\\!:\\!\mathbb{N}\to\mathbb{N}\to\mathbb{P}$
satisfying the conditions

$\displaystyle\exists e\,\forall x.\,\neg\,x\in e,\hskip 34.14322pt\forall
n\,c\,\exists c^{\prime}\,\forall x.\,x\in c^{\prime}\leftrightarrow x=n\lor
x\in c,$

and should be though of as formalizing set inclusion. 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.13.

By induction on $n$. In the case $n=0$, we use that first condition, giving us
an empty set $e$, which we use as the code $c$. In the inductive case, we
inspect the cases coming from $\neg\neg(p\,n\lor\neg p\,n)$. If $\neg p\,n$
then we simply use the code $c$ that is given by the inductive hypothesis. If
$p\,n$, we use the second condition to enlarge $c$ by the element $n$, and let
the bigger set be the new code.

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 short for $\lambda
n.\,\mathcal{M}\vDash\varphi_{\in}(\overline{n},d)$ we then get:

######  Theorem 37.

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

This highlights that the statement of 35 is not inherently tied to
divisibility. It rather seems generally tied to relations that allow the
implementation of finite sets or sequences inside of $\mathsf{HA}$. In [Vis08]
Visser analyses several axiomatizations of pairs, sets and sequences in first-
order theories. 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.

##  8\. Discussion

###  8.1. General Remarks

In section 7, we presented several proofs of Tennenbaum’s theorem which we
summarize in the below table, listing their assumptions101010 We do not list
the global assumption $\mathsf{CT_{Q}}$. Both 31 and $\mathsf{HA}$-coding (34)
were not mechanized in Coq but are provable, which is why we also leave them
out of the table.  on the left and the conclusion on the right.

$\mathsf{MP}$ | $\mathsf{AUC}$ | discrete |  | Conclusion | from
---|---|---|---|---|---
$\bullet$ |  | $\bullet$ |  $\mathcal{M}$ enumerable | $\to~{}~{}~{}\mathcal{M}\cong\mathbb{N}$ | Diagonalization
$\bullet$ |  | $\bullet$ | $\forall d\\!:\\!\mathcal{M}.\neg\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{d})}$ | $\to~{}~{}~{}~{}\mathcal{M}\cong\mathbb{N}$ | Inseparability
|  |  | $\forall d\\!:\\!\mathcal{M}.\neg\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{d})}$ | $\to\neg\mathcal{M}>\mathbb{N}$ | Makholm
$\bullet$ | $\bullet$ |  |  | $\mathcal{M}\cong\mathbb{N}$ | McCarty

First note that in the first two results we can clearly show the reverse
implications. Therefore, given $\mathsf{MP}$ and discreteness of $\mathcal{M}$
we have the equivalences

$\displaystyle\mathcal{M}\text{
enumerable}~{}\mathbin{\Longleftrightarrow}~{}\mathcal{M}\cong\mathbb{N}~{}\mathbin{\Longleftrightarrow}~{}\forall
d.\neg\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{d})}.$

Comparing the first three entries, we see that Makholm’s result is a
strengthening of the second one, in the sense that it no longer requires
$\mathsf{MP}$ and the discreteness assumption, but once we do assume them, it
gives us the same result as the inseparability proof. His result becomes
possible once we make use of $\mathsf{HA}$-inseparable formulas, overcoming
the need for Overspill, which is the root for needing the additional
assumptions. In general, we can observe that the results become progressively
stronger and less reliant on further assumptions as more intermediary results
are progressively proven on the object level of $\mathsf{HA}$. For example,
instead of using Overspill to establish a coding, we later use that there is
an internal proof of the coding lemma. 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. Makholm’s result can equivalently be written as
$\mathcal{M}>\mathbb{N}\to\neg\neg\exists
d.\,\neg\mathsf{Dec}{(\,\overline{\,\cdot\,}\mid{d})}$, leaving 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: [$\mathsf{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
of the 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
computation [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, 35 and 22 entail that neither
equality nor apartness can be decidable. This is similar in spirit to the
results in [TGH17], 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 axioms $\mathsf{CT_{Q}}$, $\mathsf{MP}$ and $\mathsf{AUC}$ are
localized in the relevant sections. Apart from these, there are the two facts
in subsection 7.3 we have labeled as hypotheses, and which were taken as
additional assumptions in the relevant sections. We have given details as to
how they can be proven, but since these proofs are not yet mechanized, we made
these assumptions very explicit in the accompanying text.

The development depends on a Coq library for first-order logic. Restricting to
the files for this project, the line count is roughly 4000 lines of code. From
those, 2000 loc on basic results about $\mathsf{PA}$ models were reused from
earlier work [KH21]. Notably, the formalization of the various coding lemmas
from section 5 took 580 loc and all variants of Tennenbaum’s theorem come 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 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 [TGH17].

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 [For21, 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, this extended journal version
relies on the slightly different definition of $\Sigma_{1}$ and $\Delta_{1}$
formulas used by Kirst and Peters [KP23]. 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 first-order encoding overhead, and 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
[Pau15], O’Connor [O’C05], as well as Han and van Doorn [HvD20]. We make use
of a Coq library for first-order logic [KHD+22], which has developed 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 to adapt this viewpoint, we could assume an
abstract version of $\mathsf{CT}$ which makes reference to a $T$ predicate
[Kle43, For21] which is then used to axiomatize $T$-computable functions. We
can then assume a version of $\mathsf{CT}$ that stipulates the computability
of every $T$-computable function. This would 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].

We plan to mechanize the facts left in subsection 7.3, namely 31 (proof given
in Appendix B) and 34 (proof of 13 needs to be turned into a derivation). As
these require sizeable syntactic derivations inside of $\mathsf{HA}$ but are
not so central for the main result, we decided to avoid the necessary
cumbersome manipulations in Coq. Their mechanization could possibly benefit
from the proof mode developed in [HKK21].

There are interesting parallels when comparing the proofs of Tennenbaum’s
theorem and the incompleteness results. 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], and study the
connection of these two theorems in a constructive framework.

A more satisfying rendering of McCarty’s result will be achieved by changing
subsection 2.3, 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.

## References

  * [Bau06] Andrej Bauer.  First steps in synthetic computability theory.  Electronic Notes in Theoretical Computer Science, 155:5–31, 2006\.
  * [Bau08] Andrej Bauer.  Intuitionistic mathematics for physics, 2008.  URL: http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/.
  * [BBJ02] George S. Boolos, John P. Burgess, and Richard C. Jeffrey.  Computability and logic.  Cambridge university press, 2002.
  * [CDE+13] 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.
  * [CH86] Thierry Coquand and Gérard Huet.  The calculus of constructions.  1986\.
  * [CMW82] 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.
  * [FKS19] 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.
  * [FKW21] 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.
  * [FLWD+20] 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.
  * [For21] 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://drops.dagstuhl.de/opus/volltexte/2021/13455, doi:10.4230/LIPIcs.CSL.2021.21.
  * [For22] 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.
  * [Her23] Marc Hermes.  Github repository, 2023.  URL: https://github.com/HermesMarc/coq-library-fol/tree/formulas.
  * [HK22] Marc Hermes and Dominik Kirst.  An Analysis of Tennenbaum’s Theorem in Constructive Type Theory.  In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1–9:19, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.  URL: https://drops.dagstuhl.de/opus/volltexte/2022/16290, doi:10.4230/LIPIcs.FSCD.2022.9.
  * [HK23] Marc Hermes and Dominik Kirst.  Website, 2023.  URL: https://www.ps.uni-saarland.de/extras/tennenbaum-ext/.
  * [HKK21] Johannes Hostert, Mark Koch, and Dominik Kirst.  A toolbox for mechanised first-order logic.  In The Coq Workshop 2021, 2021.
  * [HvD20] 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.
  * [Kay91] Richard Kaye.  Models of Peano Arithmetic.  Clarendon Press, 1991.
  * [Kay11] 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\.
  * [KH21] 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://drops.dagstuhl.de/opus/volltexte/2021/13918, doi:10.4230/LIPIcs.ITP.2021.23.
  * [KHD+22] Dominik Kirst, Johannes Hostert, Andrej Dudenhefner, Yannick Forster, Marc Hermes, Mark Koch, Dominique Larchey-Wendling, Niklas Mück, Benjamin Peters, Gert Smolka, and Dominik Wehr.  A Coq library for mechanised first-order logic.  In Coq Workshop, 2022.
  * [Kle43] Stephen C. Kleene.  Recursive predicates and quantifiers.  Transactions of the American Mathematical Society, 53(1):41–73, 1943.
  * [KLW20] 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.
  * [KP23] Dominik Kirst and Benjamin Peters.  Gödel’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability.  In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2023.
  * [Kre70] 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.
  * [Mak14] Henning Makholm.  Tennenbaum’s theorem without overspill.  Mathematics Stack Exchange, 2014.  (version: 2014-01-24).  URL: https://math.stackexchange.com/q/649457.
  * [MC17] Bassel Mannaa and Thierry Coquand.  The independence of Markov’s principle in type theory.  Logical Methods in Computer Science, 13, 2017.
  * [McA82] Kenneth McAloon.  On the complexity of models of arithmetic.  The Journal of Symbolic Logic, 47(2):403–415, 1982.
  * [McC87] David C. McCarty.  Variations on a thesis: intuitionism and computability.  Notre Dame Journal of Formal Logic, 28(4):536–580, 1987.
  * [McC88] David C. McCarty.  Constructive validity is nonarithmetic.  The Journal of Symbolic Logic, 53(4):1036–1041, 1988.  URL: http://www.jstor.org/stable/2274603.
  * [McC91] David C. McCarty.  Incompleteness in intuitionistic Metamathematics.  Notre Dame journal of formal logic, 32(3):323–358, 1991.
  * [O’C05] 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.
  * [Pau15] Lawrence C. Paulson.  A mechanised proof of Gödel’s incompleteness theorems using nominal Isabelle.  Journal of Automated Reasoning, 55(1):1–37, 2015.
  * [Pet22] Benjamin Peters.  Thesis: Gödel’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability, 2022.
  * [Pli90] 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.
  * [PM93] 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.
  * [Raa21] 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.
  * [Ric83] Fred Richman.  Church’s thesis without tears.  The Journal of symbolic logic, 48(3):797–803, 1983.
  * [Sha86] Natarajan Shankar.  Proof-checking metamathematics (theorem-proving).  PhD thesis, The University of Texas at Austin, 1986.
  * [Smi14] Peter Smith.  Tennenbaum’s theorem.  Technical report, 2014.  URL: https://www.logicmatters.net/resources/pdfs/tennenbaum_new.pdf.
  * [SU19] Andrew Swan and Taichi Uemura.  On Church’s Thesis in Cubical Assemblies, 2019.  arXiv:1905.03014.
  * [Tea22] The Coq Development Team.  The Coq Proof Assistant, January 2022.  doi:10.5281/zenodo.5846982.
  * [Ten59] Stanley Tennenbaum.  Non-archimedean models for arithmetic.  Notices of the American Mathematical Society, 6(270):44, 1959.
  * [TGH17] Michał T. Godziszewski and Joel D. Hamkins.  Computable quotient presentations of models of arithmetic and set theory.  arXiv e-prints, pages arXiv–1702, 2017.
  * [Tro73] Anne S. Troelstra.  Metamathematical investigation of intuitionistic arithmetic and analysis, volume 344.  Springer Science & Business Media, 1973.
  * [TvD88] 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.
  * [Vis08] Albert Visser.  Pairs, sets and sequences in first-order theories.  Archive for Mathematical Logic, 47:299–326, 2008.
  * [Wil85] George Wilmers.  Bounded existential induction.  The Journal of Symbolic Logic, 50(1):72–90, 1985.
  * [Yam20] Norihiro Yamada.  Game semantics of Martin-Löf type theory, part III: its consistency with Church’s thesis, 2020.  arXiv:2007.08094.

##  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<EMAIL_ADDRESS>\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 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$.

##  Appendix B $\mathsf{HA}$-inseparable Formulas

To prove the existence of $\mathsf{HA}$-inseparable formulas we will make use
of a general form of Rosser’s trick. [Rosser Formula] Given any binary
formulas $\alpha(t,x)$ and $\beta(t,x)$ we define

$\displaystyle(\alpha<\beta)(x)\mathbin{:=}\exists\,t.\,\alpha(t,x)\land\forall\,v.\,\beta(v,x)\to
t<v$

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

######  Lemma 38 (Disjointness of Rosser Formulas).

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

######  Proof B.1.

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

$\displaystyle\alpha(t,x)~{}\land~{}$ $\displaystyle\forall\,v.\,\beta(v,x)\to
t<v$ $\displaystyle\beta(t^{\prime},x)~{}\land~{}$
$\displaystyle\forall\,v.\,\alpha(v,x)\to t^{\prime}<v$

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

######  Theorem 39.

There is a pair of unary $\mathsf{HA}$-inseparable formulas.

######  Proof B.2.

By 27, 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

$\displaystyle\forall v.\,\beta(v,\overline{n})\to
w<v~{}\leftrightarrow~{}\forall v\leq w.\neg\beta(v,x)$

where the latter formula is $\Delta_{1}$, we know that $(\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 deep disjointness property
follows from the previous 38. 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

$\mathsf{Q}\vdash(\alpha<\beta)~{}\subseteq~{}D~{}\subseteq~{}\neg\,\mathsf{Q}\vdash(\beta<\alpha)$

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

$\mathsf{Q}\vdash\alpha^{\prime}~{}\subseteq~{}\mathsf{Q}\vdash(\alpha<\beta)~{}\subseteq~{}D~{}\subseteq~{}\neg\,\mathsf{Q}\vdash(\beta<\alpha)~{}\subseteq~{}\neg\,\mathsf{Q}\vdash\beta^{\prime}$

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