9
$\begingroup$

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.

$\endgroup$
11
  • 3
    $\begingroup$ The main obstruction would be that the statement is false. Maybe you meant to relativize "Peano" as well? If so, please explain how. (See the well-studied notion of PA-degrees.) $\endgroup$ Aug 8 '20 at 23:03
  • 1
    $\begingroup$ The RTT statement is false because if $M$ is nonstandard then the standard model is not isomorphic to $M$ but the standard model is recursive. $\endgroup$ Aug 9 '20 at 5:32
  • 4
    $\begingroup$ I’m pretty sure Tennenbaum’s theorem is provable in PA, which, translated to model-theoretic terms, means that no proper extension $M'$ satisfying PA of a model $M$ of PA is $\Sigma_1$-definable in $M$. (Note that such internally definable models are automatically end-extensions.) This should also hold for much weaker theories than PA. Perhaps there might be a version that applies to proper end-extensions that are merely externally relatively computable rather than $\Sigma_1$-definable, but I don’t think that any such thing stands a chance to hold when $M'$ is not an extension of $M$. $\endgroup$ Aug 9 '20 at 8:38
  • 1
    $\begingroup$ (In principle, I should have written “proper extension $M'$ of $M$ such that $M$ thinks $M'$ is a model of PA” rather than “proper extension $M'$ satisfying PA”, but since, as I mentioned, this should hold even for much weaker, finitely axiomatizable fragments of PA, the distinction does not matter.) $\endgroup$ Aug 9 '20 at 8:49
  • 2
    $\begingroup$ Ok, I will try to write it up as an answer, but it may take a while, as I’m out of office at the moment. $\endgroup$ Aug 10 '20 at 10:48
2
$\begingroup$

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.

$\endgroup$
1
  • 2
    $\begingroup$ let me process what you wrote (meanwhile you got already my vote, at the very least for trying to sum up the above). . The last comment of Emil was "Ok, I will try to write it up as an answer, but it may take a while,". $\endgroup$ Mar 16 at 20:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.