Tennenbaum's Theorem 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 (starting on pdf page 26)
(2) Constructive Validity is Nonarithmetic (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)$ which is equivalent to $\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 and Richard Kaye, 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 (CT+MP show 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.
