An internalized version of Tennenbaum's Theorem

Question

Tennenbaum's celebrated 1959 theorem (see here for a reference) is certainly one of the key theorems in mathematical logic. Not so much for its proof, but because it helps "isolating" $N$ as something very special: it is the only countable model of Peano arithmetic which is recursive.

But, does it?

Suppose I live inside any countable model $M$ of Peano: I think I am actually living in the standard natural numbers, and addition/multiplication are the standard ones (and so are all the recursive function, etc). So, it would seem that from the point of view of $M$, other PA-models are not recursive. To be a bit more precise, let me state this:

Internalized Tennenbaum Theorem (ITT): Let $M$ be a countable model of Peano. Then, for any other countable model $N$ not isomorphic to $M$, $N$ is not recursive in $M$, ie it is not $\Delta_1$-definable in M.

Question: Can ITT be proved in, say, ZFC? If not, what is the obstruction?

Post Scriptum.

Thanks to Emil Jerabek for his suggestion: rather than the original misleading name, Derived Tennenbaum, use Internal (or Internalized). The original name generated some confusion, see the comments of Francois Dorais, thus I decided to rename the question. The recursivity required is IN the model, not FROM the model.

Answer 1

To move this off the unanswered queue, let me summarize the situation as correctly explained by the comments above:

The standard proof of Tennenbaum's theorem goes through inside $\mathsf{PA}$: $\mathsf{PA}$ proves that there is no $\Delta_1$ description of a model of $I\Sigma_1$. (As usual, $\mathsf{PA}$ can be replaced with something vastly weaker here; at a glance, already $I\Sigma_1$ should be enough.)

One key point here is that $\mathsf{PA}$ can quantify over $\Delta_1$ descriptions since this only involves reference to a bounded truth predicate. (Something like "There is no definable structure such that [stuff]" would have to be expressed as a scheme, but that's not an issue here.)

On the other hand, $\mathsf{PA}$ cannot express "the structure defined by the formula tuple $\Phi$ satisfies $\mathsf{PA}$" (at least not as cleanly as one might hope - we'd need to talk about explicitly-Skolemized structures, and that's a whole annoying rabbit hole to go down). This is why I've used $I\Sigma_1$ as the "Tennenbaum target:" as a finitely axiomatizable theory, $\mathsf{PA}$ has no trouble talking about its satisfaction (or not) in a defined structure, again by virtue of the satisfactoriness of a bounded truth predicate.