[Tennenbaum's Theorem][5] in its usual form states that for any countable non-standard model $M$ of PA there is no way to code the elements of $M$ as natural numbers such that either the addition or multiplication operation of the model is a computable function on the codes.


Here are two papers by Charles McCarty containing proofs for Tennenbaum's theorem in a constructive setting:

(1) [**Variations on a thesis: intuitionism and computability**][1] *(starting on pdf page 26)*

(2) [**Constructive Validity is Nonarithmetic**][2] *(proof is a bit more detailed)*


He is working in Heyting arithmetic ($\mathsf{HA}$) instead of $\mathsf{PA}$ and further considers the models to be put into a constructive setting (e.g. $\mathsf{IZF}$?) as well. 

Below, I will list the main steps of the proof as I see them. For any $\mathsf{HA}$ Model $M$, I will call $a \in M$ standard an write $\operatorname{std}(a)$ iff there is an $n \in \mathbb{N}$ with $\overline{n} = a$, where $\overline{\,\ast \,} : \mathbb{N} \rightarrow M$ is the canonical embedding.

- Let $a \in M$ with $\neg \operatorname{std} a$. One can show that it is greater than any numeral $\overline{n}$.
- There are recursively inseparable sets $A, B$ represented by $\Sigma_1$ formulas $\alpha(x), \beta(x)$. 
- For **any** unary predicate $\varphi$ you can show $\mathsf{HA} \vdash \forall x ~\neg \neg \forall y < x. ~ \, \varphi(y) \, \lor \, \neg \varphi(y)$ 
- Using soundness and instantiating the above for $\alpha$ and $a$ we get $M \vDash \neg
\neg \forall y < a. ~\, \alpha(y) \, \lor \, \neg \alpha(y)$
- We are trying to prove $\bot$, so we can get rid of the $\neg \neg$ in the above and since any numeral $\overline{n}$ is smaller than $a$ we get $(M \vDash \alpha(\overline{n}) ) \lor (M \vDash \neg \alpha(\overline{n}))$.
- Models are considered to be constructive, so the above $\lor$ means we have a decider which we can use to define a function by $f(n) = 0 ~\Leftrightarrow~ M \vDash \alpha(\overline{n})$.
- By Church's Thesis, the function $f : \mathbb{N} \rightarrow \mathbb{N}$ is recursive and separates $A$ and $B$, leading to a contradiction. 

So far this shows $\neg \exists a \in M ~ \neg \operatorname{std}(a) ~\Leftrightarrow~ \forall a \in M ~ \neg \neg \operatorname{std}(a)$. 

Further assuming Markov's Principle, we immediately get $\forall a \in M ~\, \operatorname{std}(a)$, showing that Heyting arithmetic has (up to isomorphism which is given by $\overline{\,\ast \,}$) only one model, namely $\mathbb{N}$.



I have done a mechanized proof of Tennenbaum in Coq, based on the presentations in articles of [Peter Smith][3] and [Richard Kaye][4] and the articles by McCarty were only a recent find by my advisor. They were not referenced by Smith or Kaye and there don't seem to be a lot of publications out there citing them. 

I am wondering why this work does not seem to be more widely known since the end-result (HA categorial) seems at least worth mentioning. I would be happy about anyone who can comment on this result, maybe also putting it into a larger context.


  [1]: https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-28/issue-4/Variations-on-a-thesis-intuitionism-and-computability/10.1305/ndjfl/1093637648.full
  [2]: https://www.jstor.org/stable/2274603?seq=1
  [3]: https://www.logicmatters.net/resources/pdfs/TennenbaumTheorem.pdf
  [4]: https://www.cambridge.org/core/books/set-theory-arithmetic-and-foundations-of-mathematics/tennenbaums-theorem-for-models-of-arithmetic/EEF8A22A2DBF156464F174EC467A531B
  [5]: https://en.wikipedia.org/wiki/Tennenbaum%27s_theorem