Uniqueness of Standard Model of Arithmetic Is the standard model of arithmetic unique? If so, is there a proof of such or is it just a consequence of the definitions?

I was reading the following blog which references a standard model of Peano arithmetic: "These are often called ‘nonstandard’ models. If you take a model of Peano arithmetic—say, your favorite ‘standard’ model —" link. My question is how do we know that such is the only one?
 A: The standard model of arithmetic is indeed unique (up to isomorphism). Of course, to assert this we need to give the phrase above a precise definition ...
Say that a model $M$ of arithmetic is standard if for every other model $N$ of arithmetic there is a unique initial segment embedding (= injective homomorphism with image an initial segment) of $M$ into $N$. There are in fact other definitions we could use here.  We can prove that $(i)$ a standard model of arithmetic exists and $(ii)$ any two standard models of arithmetic are isomorphic (indeed, uniquely isomorphic - if $M,N$ are standard models of arithmetic, then there is a unique isomorphism from $M$ to $N$). The latter justifies the use of "the" in "the standard model."
Of course, in stating the above we need to precisely define "arithmetic." But pretty much anything reasonable will work; in particular, the claim above is true for Robinson's Q and (restricting attention to addition alone) Presburger arithmetic. 
The best intuition for this in my opinion is by comparison. Suppose $M,N$ are models of arithmetic; we can try to define an embedding of $M$ into $N$ in "stages" (send the least element of $M$ to the least element of $N$, the next-least element of $M$ to the next-least element of $N$, ...). This will work for a while, but possibly not "all the way up" (maybe $M$ does not in fact embed into $N$). However, we can look at the subset of $M$ consisting of all $x$ such that for every model $N$, the attempted-embedding-process works up to $x$. The set of all such $x$ can then be shown to be a standard model of arithmetic.


*

*A bit more precisely: for a model $M$ of arithmetic, let $M_0$ be the set of $x\in M$ such that for every model $N$ of arithmetic there is some $y\in N$ such that $[0,x]^M$ is uniquely isomorphic to $[0,y]^N$, where "$[0,a]^B$" for $B$ a model of arithmetic and $a\in B$ is the "substructure"of $B$ consisting of all elements $\le a$ (it's not a literal substructure unless $a=0$, since if $a\not=0$ it's not closed under $+$ and $\times$, but we can resolve this either by talking about partial structures or by replacing $+$ and $\times$ with their corresponding "graph relations). It's not hard then to show that $M_0$ is a standard model of arithmetic.



Of course this depends on a background theory within which this proof takes place (this is distinct from the theory we choose to call "arithmetic" - we're proving something about arithmetic, in the context of a different, "larger" theory). Usually when we don't state that theory it's taken to be ZFC, and that certainly suffices here. However, in general ZFC is massive overkill, and this is such a case: the existence of the standard model of arithmetic can be appropriately stated and proved in the much weaker theory ACA$_0$, and in fact this is optimal in a precise sense (I don't know a citation for this fact but this is not hard to prove). 


*

*Incidentally, the general study of what axioms are needed to prove particular theorems is indeed a topic of much interest, most of it falling under the umbrella of reverse mathematics

*Also, it's worth pointing out that both ACA$_0$ and ZFC have a "distinguished" model of arithmetic, and so in each context we generally prove the stronger fact that that distinguished model is standard; indeed, in the ACA$_0$ context I think that's how we have to proceed.
On the other hand, we could always consider frameworks which actively refute (rather than simply are too weak to prove) the theorem above. See e.g. this article of Yessenin-Volpin (an ultrafinitist who interestingly believed that ZFC, and indeed much more, is consistent!) or more recently some approaches to a multiverse framework of set theory (see the discussion before the "well-foundedness mirage" bit on page $25$ - this would be an extreme version of that principle). Whether one finds these alternate theories compelling is of course subjective; personally, I happen to be at least somewhat sympathetic to them.
