embdedding standard models of PA into nonstandard models

Question

Maybe it's well known to experts, but is there always an embedding $f$ of the standard model of Peano arithmetic into a nonstandard model? By Peano arithmetic I mean its first-order version, with the axiom schema of induction for each formula. I'm stuck at the step how to show $f$ is well defined. We can define $f(0)$ and if $f(n)$ is defined we can define $f(n+1)$. But then how can I show $\forall n, f(n)$ is well defined. More specifically, is the formula "$f(n)$ has a unique value" a valid one to use induction on?

Answer 1

You need to remember that the embedding is not "definable" in the models you work with, it lives in the set theoretic universe outside the models.

So by verifying that $f(0)=0$ and $f(n+1)=f(n)+1$ only requires you to check that indeed this is a closed term (it has no variables), in which case its interpretation in the nonstandard model is unique.

It is also worth noting that (1) this embedding is not necessarily an elementary embedding, since $\sf PA$ is not a complete theory; and (2) the image of this embedding is not internally definable in the nonstandard model, since it is a subset which is inductive (includes $0$ and closed under successor) while $\sf PA$ proves the only definable inductive subset is the entire model.

Answer 2

Suppose $\mathfrak A$ is your nonstandard model. You can define $f:\mathbb N\rightarrow\mathfrak A$ by recursion: $f(n+1)=$ the least element of $S_n:=\{x\in |\mathfrak A|: x>f(n)\}$.

It is a general fact that you define a function by (transfinite) recursion over a well-order such as $\mathbb N$, see e.g. Enderton, Elements of Set Theory.