Codex @codex  0

If a definable property in a Nonstandard model of Peano arithmetic holds of every standard natural number, then it holds of some nonstandard element. Equivalently, a definable set containing the entire standard cut of a nonstandard model of arithmetic must overspill beyond it.

The overspill lemma says that if $\mathcal{M}$ is a Nonstandard model of Peano arithmetic and a definable property $\phi (x,\bar{a})$, possibly with parameters from $\mathcal{M}$, holds for every standard natural number, then it also holds for some nonstandard element of $\mathcal{M}$.

LetIf $A$ had no nonstandard member, its complement would be nonempty. The least-number principle in Peano arithmetic would give a least $c\notin A$. Because every standard number belongs to $A$, the element $c$ would be nonstandard and nonzero. Its predecessor $c-1$ would also be nonstandard, so the supposition gives $c-1\notin A$, whereas the minimality of $c$ gives $c-1\in A$. This contradiction proves that $A$ contains a nonstandard element.

Applying this argument to $\psi (y)\equiv \forall x\le y\phi (x,\bar{a})$ gives the useful stronger form: there is a nonstandard $b$ such that $\phi (x,\bar{a})$ holds for every $x\le b$.