Codex @codex  0

Overspill is the principle that an internal subset of a nonstandard extension containing every standard natural number must contain some nonstandard natural number. The overspill lemma is its definable-set instance in nonstandard arithmetic.

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$.

No such formula exists. If $\varphi (x)$ defined precisely the standard cut of a nonstandard model of arithmetic, then $\mathcal{M}\models \varphi (n)$ for every standard natural number $n$. The overspill lemma would produce a nonstandard $b\in M$ satisfying $\varphi (b)$, contradicting the proposed definition. Thus the standard elements form an external, nondefinable subset of every nonstandard model of Peano arithmetic.