My reference is Richard Kaye's Models of Peano Arithmetic, section 6.1.
I am wondering what Robinson's overspill lemma actually tells us, and a bit of motivation on it. I have heard of it before, and it is described as of 'utmost importance', but the statement has me confused. Kaye motivates the lemma with the following paragraph:
Suppose that $I$ is a proper cut of $M\vDash PA$, i.e. $I$ is not equal to the domain of $M$; then $I$ is not a definable subset of $M$; for if $\overline a\in M$ and $\varphi(x,\overline a)$ is an $\mathscr{L}_A$-formula with $$I=\{b\in M: M\vDash\varphi(b,\overline a)\},$$ then $M\vDash\varphi(0,\overline a)\wedge\forall x(\varphi(x,\overline a)\rightarrow\varphi(x+1,\overline a))$, since $I$ is non-empty and is closed under the successor function, and so by induction in $M$, $M\vDash\forall x\varphi(x,\overline a)$, contradicting the assumption that $I$ is a proper cut. The overspill lemma, due to Abraham Robinson, essentially says just this.
The statement of the lemma seems to say that there is some non-standard $c>I$ such that $\varphi$ holds for all $x\le c$, and the proof uses that $I$ cannot be definable.
Lemma 6.1 (Overspill). Let $M\vDash PA$ be non-standard and let $I$ be a proper cut of $M$. Suppose $\overline a\in M$ and $\varphi(x,\overline a)$ is an $\mathscr L_A$-formula such that $$M\vDash\varphi(b,\overline a)\;\text{for all}\;b\in I.$$ Then there is $c>I$ in $M$ such that $$M\vDash\forall x\le c\varphi(x,\overline a).$$
The proof is brief, saying that if the assumptions were true, but the conclusion false, then $I$ would be defined by the formula $$\forall y<x\varphi(y,\overline a).$$
If I understand correctly, this follows from the following reasoning. If $x\in I$ then the formula holds, since $y<x\in I\implies y\in I$ by definition of a cut, and $M\vDash\varphi(b,\overline a)$ for all $b\in I$. Conversely, if $x$ satisfies $\forall y<x\varphi(y,\overline a)$, then either $x\in I$; or otherwise $x>I$ and there is a $c>I$ such that $c<x$ and so $M\vDash\forall x\le c\varphi(x,\overline a)$.
I wonder though what the 'true significance' of this lemma is. It seems like a coincidence derived from how we defined cuts... and I cannot see how it could be relevant or useful. Is there an intuitive way to think of this $\varphi$ or $c$? The way I am imagining it is that $\varphi(b,\overline a)$ is true for all of $I$, then it remains true beyond $I$ for a while (before possibly 'becoming' untrue at at some point).
Thank you!
Your understanding of the result, and of its proof, is correct. So why is it important?
My personal favorite set of applications come from trying to understand the standard system of a nonstandard $M\models PA$: $SS(M)$ is the set of sets $X$ of (standard) natural numbers such that, for some $c\in M$, $$X=\{k\in\mathbb{N}: M\models\underline{p_k}\vert c\}$$ (where $\underline{k}$ is the numeral standing for the standard natural number $k$, and $p_k$ denotes the $k$th prime).
Let's start with an easy application: in any nonstandard model of $PA$, definable sets of true natural numbers are coded by nonstandard elements. That is: suppose $M\models PA$ is nonstandard, and $\varphi$ is a formula of arithmetic with some parameters from $M$ and one free variable. Then there is a (nonstandard) $c\in M$ such that for all standard $k$, we have $$M\models \underline{p_k}\vert c\iff M\models\varphi(\underline{k}).$$
Why? Well, say that $m\in M$ is nice if there is (in $M$) a $c$ such that for all $k<m$, $p_k\vert c$ iff $\varphi(k)$. Note that this definition takes place entirely in $M$: no reference to standard elements is made. Well, clearly every standard $m$ is nice, so by overspill some nonstandard $m$ is nice; but then take a witnessing $c$.
Here's a more interesting one: suppose $M$ is nonstandard. Then there is a consistent completion of $PA$ which is in $SS(M)$, even if $M$ thinks $PA$ is inconsistent! Why?
Well, first note that we can reason in $PA$ about finite binary strings, and sentences and proofs in the language of arithmetic. So let's consider the following object: $T$ is the set of $\sigma\in 2^{<\mathbb{N}}$ such that the set $$PA\cup\{\varphi_n: \sigma(n)=1\}\cup\{\neg\varphi_n: \sigma(n)=0\}$$ does not have a proof of $0=1$ using fewer than $\vert\sigma\vert$-many symbols (where $\{\varphi_n: n\in\mathbb{N}\}$ is some reasonable enumeration of the sentences of arithmetic). $T$ is appropriately definable, and indeed absolute: if $\sigma$ is in the true $T$, then $\sigma$ is also in $T^M$ for any nonstandard model $M$.
Now, in reality $T$ has infinite paths, since $PA$ is in fact consistent. So by overspill, $T^M$ has a node of nonstandard length! Let $\sigma$ be such a node; since the set of $k$ such that $\sigma(k)=1$ is definable, by the above point we get some $c\in M$ such that for all standard $k$, $p_k\vert c\iff \sigma(k)=1$. But then the element of $SS(M)$ coded by $c$ is (the set of Goedel numbers of) a consistent completion of $PA$. (Why is it consistent? Well, no contradiction can be proved using $\vert\sigma\vert$-many symbols - but $\vert\sigma\vert$ is infinite!)
Incidentally, a similar argument can be used to show that any model $M$ of ZFC contains an element which is a model of ZFC, even if $M$ thinks ZFC is inconsistent.
Now, these two examples illustrate an important point about the value of overspill. The first example, honestly, would be clearer if we ignored overspill and just used induction. The second, however, has a nice intuitive picture via overspill (take a node of nonstandard length!), whereas the induction version (in my opinion) obscures the intuition. The true value of overspill is in "repackaging" a certain class of inductive arguments in a more intuitive way. It is particularly useful when we're juggling between "internal" concepts (elements of $M$) and "external" concepts (the set of naturals coded by an element of $M$).