Does $\textsf{PA}$+Con($\textsf{PA}$) entail the existence of non-standard models of $\textsf{PA}$?


Is there a reasonable way in which to code, inside $\textsf{PA}$, the statement that $\textsf{PA}$ has non-standard models?


If so, suppose we start from $\textsf{PA}$ and iteratively add consistency statements, obtaining a transfinite hierarchy of theories $\{\Gamma\_{\alpha}\}\_{\alpha\in\textsf{On}}$, each asserting the consistency of its predecessor. Is there some ordinal $\alpha$ at which $\Gamma\_{\alpha}$ proves that $\textsf{PA}$ has non-standard models? 



Does PA+Con(PA) entail the existence of non-standard models of PA?
$PA$ is a weird theory to work with, here: if you want to talk about models, then a two-sorted theory like $RCA\_0$ or $ACA\_0$ is probably better. $PA$ cannot directly talk about models, since it can't directly talk about sets.


However, $PA$ (in fact, much less than $PA$) proves that if $PA$ is consistent, then so is the theory $PA^\*$ in the language of arithmetic + one new constant, $c$, and containing the axioms $c\not=n$ for each (standard) natural number $n$; so in that sense, $PA+Con(PA)$ would prove that $PA$ has nonstandard models. 


If one wants to talk about models directly, using a two-sorted theory, then things get more interesting: there is a reasonable theory, $RCA\_0$ - its first-order part is $I\Sigma\_1$, $PA$ but with induction substantially restricted - which can prove that $Con(PA)$ implies $Con(PA+\neg Con(PA))$, and which proves that complete consistent theories have models, but can't quite prove that *arbitrary* consistent theories have models. So, for example, $RCA\_0+Con(RCA\_0)$ cannot prove that $RCA\_0$ has nonstandard models (the easiest way to see this is via Tennenbaum's theorem).


Note that this added complexity means that the distinction between *models* and *consistencies* [sic] is actually very significant, and not something to be lightly swept under the rug.


