Check my proof of "overspill" in non-standard models of Peano arithmetic. Proposition
Let $\mathcal{M}$ be a nonstandard model of Peano arithmetic, $\phi(v,\bar{w})$ a formula in the language of arithmetic, and $\bar{a} \in \mathbb{M}$. Show that if $\mathcal{M} \models \phi(n,\bar{a})$ for all $n < \omega$, then there is an infinite $c \in \mathbb{M}$ s.t. $\mathcal{M} \models \phi(c,\bar{a})$.
My Proof
Let $\mathcal{N}$ be the standard model of Peano arithmetic, and $\pmb{PA}$ the theory of Peano arithmetic so that $\mathcal{N} \models \pmb{PA}$; additionally, we know by definition $\mathcal{M} \models \pmb{PA}$. Suppose for the sake of contradiction that there exists a nonstandard model $\mathcal{M}$ so that $\mathcal{M} \models \phi(n,\bar{a})$ but $\mathcal{M} \not\models \phi(c,\bar{a})$. Since $\mathcal{M} \models \pmb{PA}$, $\mathcal{M} \models \phi(0,\bar{a})$ and by the assumption that $\mathcal{M} \models \phi(n,\bar{a})$ for all $n < \omega$, we know $\mathcal{M} \models \forall x (\phi(x,\bar{a}) \Rightarrow \phi(x + 1, \bar{a}))$. Hence by the induction axiom of $\pmb{PA}$:
$$Ind(\phi) := (\phi(0) \wedge \forall x(\phi(x) \Rightarrow (x+1))) \Rightarrow \forall x \phi(x),$$
we know $\mathcal{M} \models \forall x (\phi(x,\bar{v}))$, therefore $\mathcal{M} \models \phi(c,\bar{a})$. But this contradicts our hypothesis and we conclude:
$$\mathcal{M} \models \phi(c,\bar{a}).$$
My Problem
My primary concern is whether I can use the induction principle of Peano arithmetic to argue that I can "reach" this $c$ by induction. Since as I understand, this $c$ lies beyond $\omega$.
Additionally, is there another way to prove the proposition without invoking the details of Peano Arithmetic?
 A: To me, Rick's proof is correct, but does not give enough details. Here is a complete proof. Let's assume we have a formula $\psi$ such that : $$\forall n < \omega, \mathcal{M} \vDash \psi(n)$$
Let's show that there exists a non standard integer satisfying $\psi$. By contradiction, we assume that all non standard integers do not satisfy $\psi$.

*

*We have $\mathcal{M} \vDash \psi (0)$. For $n < \omega$, we have $\mathcal{M} \vDash \psi(n+1)$, so we also have $\mathcal{M} \vDash \psi(n) \rightarrow \psi(n+1)$

*By hypothesis, for a non standard integer $b$ we have $\mathcal{M}\nvDash \psi(b)$, so, exfalso, we have $\mathcal{M} \vDash \psi(b) \rightarrow \psi(b+1)$ (the left side of implication is false).

*By induction hypothesis, that is true in $\mathcal{M}$ as it is a model of Peano's arithmetic, we have $\forall x, \mathcal{M} \vDash \psi(x)$, which contradicts our hypothesis. So there exists at least one non standard integer satisfying $\psi$.

One can easily extend this proof to show that once we have $\mathcal{M} \vDash \psi(a)$ for some-non standard integer $a$, then we have $\forall b < a, \mathcal{M} \vDash \psi(b)$.
Have a good day !
A: The induction principle is OK in $\mathcal M$, but its hypothesis is not necessarily satisfied in your situation.  You inferred from (1) $\mathcal M\models\phi(n,\bar a)$ for all $n<\omega$ that (2) $\mathcal M\models\forall x\,(\phi(x,\bar a)\implies\phi(x+1,\bar a))$.  Unfortunately, (1) does not imply (2).  The error arises because the variable $x$ in (2) ranges over the whole universe of $\mathcal M$, not just over numbers $n<\omega$.
Note also that, if your argument were correct, it would give that $\mathcal M\models\phi(c,\bar a)$ for all elements $c$ of $\mathcal M$.  That conclusion is not in general right; the correct conclusion is that some infinite $c$ in $\mathcal M$ satisfies $\mathcal M\models\phi(c,\bar a)$. (One can do a bit better; there is some infinite $d$ in $\mathcal M$ such that $\mathcal M\models\phi(c,\bar a)$ for all $c\leq d$.)
A: Summing up the answer from Andreas and the comments above, here is a full answer to the question.

Assume for contradiction that $\mathscr M \not\models \psi(c,\overline a)$ for all non-standard $c \in |\mathscr M|$. By assumption, we have that $\mathscr M \models \psi(0, \overline a)$ and $\mathscr M \models (\psi(n, \overline a) \rightarrow \psi(n+1, \overline a))$, so by the induction axiom of PA it follows that $\mathscr M \models \forall x (\psi(x, \overline a))$. In particular, $\mathscr M \models \psi(c, \overline a)$ for all non-standard $c \in |\mathscr M|$, a contradiction.
A: Below is a more "positive" version of the Overspill Lemma, which does not require a proof by contradiction which slightly eases the proof.

A $\mathsf{PA}$ model $\mathcal{M}$ is isomorphic to $\mathbb{N}$ if and only if there is a formula $\varphi(x)$ such that $e < \omega \iff \mathcal{M} \vDash \varphi(e)$ for every $e \in \mathcal{M}$.

Proof:
$(\Longrightarrow)$ If $\mathcal{M} \cong \mathbb{N}$ then there is indeed such a formula $\varphi(x)$, namely $x = x$.
$(\Longleftarrow)$ Assume there is a formula $\varphi(x)$ with $e < \omega \iff \mathcal{M} \vDash \varphi(e)$, then note that we have:

*

*$0 < \omega$ and therefore $\mathcal{M} \vDash \varphi(0)$.

*Obviously we have $e < \omega \Rightarrow e + 1 < \omega$, which is equivalent to $\mathcal{M} \vDash \varphi(e) \Rightarrow \mathcal{M} \vDash \varphi(e+1)$ by our assumption. Overall this shows $\mathcal{M} \vDash \forall x \; (\, \varphi(x) \to \varphi(x+1) \,)$.

Together with the induction principle the above bullet points imply the truth of $\mathcal{M} \vDash \forall x \; \varphi(x)$, further giving us
$$
 \mathcal{M} \vDash \forall x \; \varphi(x)
 \iff
 \forall e \in \mathcal{M} : \mathcal{M} \vDash \varphi(e) 
 \iff
 \forall e \in \mathcal{M} : e < \omega
$$
showing that all of the elements in $\mathcal{M}$ are standard numbers, i.e. $\mathcal{M} \cong \mathbb{N}$. $\hspace{1em} \Box$


*

*Institutionistically, the above proof establishes a stronger version of Overspill.

*The usual Overspill Lemma is implied by the contrapostion of the above constructive result.

*$e < \omega$ should be understood as $\exists \, n \in \mathbb{N} \; (e = S^n 0)$.

A: This is my current proof. It incorporates suggestions from comments above and elsewhere.
First recall that $\phi(x) \rightarrow \phi(x+1)$ is short hand for $\neg \phi(x) \vee \phi(x+1)$. Now suppose for some infinite $c$, we have $\mathcal{M} \models \neg\psi(c,\bar{a})$, then the statement:
$$\mathcal{M} \models \neg\psi(c,\bar{a}) \vee \mathcal{M} \models (c + 1, \bar{a}),$$
is true since the first statement of the disjunction is true by definition. But by definition:
$$\mathcal{M} \models \neg\psi(c,\bar{a}) \vee \mathcal{M} \models (c + 1, \bar{a}) \Rightarrow \mathcal{M} \models \psi(c,\bar{a}) \rightarrow \psi(c + 1, \bar{a}),$$
hence the implication is true for all infinite $c$. On the other hand, we know $\mathcal{M} \models \psi(n,\bar{a})$ for all $n < \omega$ so $\mathcal{M} \models \psi(n+1,\bar{a})$. Hence we have:
$$\mathcal{M} \models \neg\psi(n,\bar{a}) \vee \mathcal{M} \models (n + 1, \bar{a}) \Rightarrow \mathcal{M} \models \psi(n,\bar{a}) \rightarrow \psi(n + 1, \bar{a}),$$
where the term on the left hand side of of $\Rightarrow$ is true because the term to the right of the disjunction is true by assumption. But we know all terms in $\mathbb{M}$ is either of form $n < \omega$ or some infinite $c$, so we can say:
$$\forall x (\psi(x,\bar{a}) \rightarrow \psi(x+1,\bar{a})) \rightarrow \forall x \psi(x,\bar{a}).$$
Hence $\mathcal{M} \models \psi(c,\bar{a})$ for some infinite $c \in \mathbb{M}$.
