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