Q:

What is the point of (Compactness theorem in the) Overspill principle?

The principle (called a Löwenheim–Skolem theorem by Huth and Ryan) states

Let $\phi$ be a sentence of predicate logic such that for any natural
  number $n \geq 1$, there is a model of $\phi$ with at least $n$
  elements. Then $\phi$ has a model with infinitely many elements.

IMO, it basically states that if you can always name a number larger than mine arbitrary natural number then your model is infinite. What needs to be proven here? There are no other options obviously for any school kid.
PS The answers state that there is a difference between having infinite amount of models and single infinite model. But this is similarly stupid. At first, I do not see whether I claim that I have a single infinite model or approach it by having all denumerable models. Secondly, it does not matter since in any case you should have an infinite model in order to respond to any natural number.
Nevertheless, I started to understand why people (mistakenly) ask me to differentiate between infinite amount of models and models of infinite size. They fail to recognize that principle "The fact that I can always name a number larger than yours implies that we have an infinite model/set", which is intuitive and used to prove the overspill theorem, also implies that the model of infinite size exists. The set of models $A = \{M_k, M_l, M_m \ldots\}$ has sizes $S = \{k, l, m, \ldots\}$ correspondingly. When you speak about size of models, you basically speak of the numbers in $S$. When you say "a model of size n" you just say "n". Thus, we can forget about set of models and speak only about S. Now, you say that "whatever integer you have, set S contains a larger one." This basically means that S contains an infinite number (i.e. $A$ contains infinite models). What to be proven here? 
In other words, what is the point of expanding $\phi$ with infinite set $\{I_1, I_2, \ldots\}$ in the proof and applying the Compactness theorem? This says that there is an infinite model. But this is obvious without even without it, right from the the premise of the overspill principle.

A:

The theorem says that when a sentence has arbitrarily large (finite) models, then it also has infinite models.
The antecedent of the theorem:

$\phi$ is a sentence of predicate logic such that for any natural
  number $n \geq 1$, there is a model of $\phi$ with at least $n$
  elements.

is equivalent to saying that there are infinitely many different models,
but it does not state that any of these models are infinite in size.
In fact, it would be clearer to use:

$\phi$ is a sentence of predicate logic such that for any natural
  number $n \geq 1$, there is a finite model of $\phi$ with at least $n$
  elements.

This is not exactly the same statement, but as an antecedent within this theorem, it is equivalent.
The consequent:

$\phi$ has a model with infinitely many elements.

does not say anything about how many different models there are - it just says something about the size of at least one of them.
To see that the truth of this theorem doesn't simply follow from its structure, consider the following statement, which has the same structure:

Let $\phi$ be a sentence of predicate logic such that for any natural
  number $n \geq 1$, there is an equivalent sentence of predicate logic with at least $n$ elements. Then there is an equivalent sentence with infinitely many elements.

Is this a theorem, too?  No, this statement is false, for the simple reason that all sentences of predicate logic have finitely many elements by definition.

A:

Your interpretation isn't faithful to the theorem: if within a model you can always find a larger number, then the model is infinite. But the theorem says that if there is an infinite number of finite models, there is also an infinite model (which is not an obvious consequence).
The statement you quote appears in a book I have (Computability and Logic by Boolos and Burgess) as the "Overspill Principle."

Overspill Principle: If a set of sentences has arbitrarily large finite models, then it has a denumerable model.

To prove this, let $\Gamma$ be a set of sentences with arbitrary large finite models. For each $m$ let $I_m$ be a sentence with no nonlogical symbols true in a model iff the model has size $m$ or larger. Let $\Gamma^*=\Gamma\cup\{I_1,I_2,\ldots\}$ be the result of adding every $I_m$ to $\Gamma$. Every finite subset of $\Gamma^*$ has a model, because every such subset is also a subset of $\Gamma\cup\{I_1,I_2,\ldots I_m\}$ for some $m$, and $\Gamma$ has arbitrarily large finite models. By compactness, $\Gamma^*$ itself has a model $M$. Then $M$ is a model of $\Gamma$, but also a model of $I_m$ for every $m$, meaning $M$ has size at least $m$ for every $m$, i.e. $M$ is infinite.

A:

The other answers are really quite good, but here is basically another variant.  Let's start with the logical mistake you're making, just to get it out of the way.  Consider the statement:

Let $\mathcal{C} = \{A_1,A_2,\ldots\}$ be a sequence of sets with $\#A_i \ge i$.  Then one of the $A_i$ is infinite.

This is not, in general, true.  Why?  Just take $A_i = [i]$.  These are all clearly finite. That $\mathcal{C}$ is infinite doesn't make the statement true.
Here, the idea is that we want $\mathcal{C}$ to be the set of models for $\phi$ and we want to somehow use the infinite sequence of finite models $A_i$ to find a single infinite model $A$.  
Since we've seen that this kind of statement isn't always true, clearly something about $\phi$ and things that are true about models of FO sentences that aren't true of arbitrary sets needs to come in.
This is where your second mistake comes in.  What you want to prove doesn't say what you think it does.  You say: 

"it basically states that if you can always name a number larger than mine arbitrary natural number then your model is infinite."

This is not what it says at all.  You are imagining a game played within one model.  That's wrong.
If you want to give the intuition as a game, it's like this: if for every number $n$ that I give you, you will be able to come back with a (different) finite model $A_n$ of size at least $n$, then there is an infinite model of $\phi$.
Now, we start to see why this might be difficult.  Nowhere was it said that any of these $A_n$ are related to each other in a way that lets you combine them into a larger model.  This is the crux of the matter.  To get around it, as in the other answer, the compactness theorem comes up, as does the hypothesis about $\phi$.
As a meta point, it is not bad to start with some intuition.  But when that either trivializes or clashes with the statement, it's a good idea to try and write a formal proof, using the definitions.  Usually, this will make clear what went wrong with the intuition, even if it seemed obvious.

