The basic theorem:

**Theorem.**
If a system of axioms has **models** of arbitrarily large finite sizes, then it has an infinite model.

Using the modern-day machinery of **mathematical logic**, this theorem is merely a somewhat trite consequence of the **compactness theorem** for **first-order logic**. But don't misjudge the people who discovered this amazing mix of logic and **set theory**!

**Proof:**

Let **A** be the system of axioms. Define the proposition P_{k} to be "there exist at least k different elements in the model". This can easily be written in first order logic as

∃x_{1}., ..., ∃x_{k}.
x_{1}≠x_{2} & ... & x_{1}≠x_{k} & ... & x_{k-1} ≠ x_{k},

and it works in any language since it uses nothing from the language. Let **A'** be the set **A** union {P_{k} : k >= 1}.
Any *finite* subset of **A'** has a model (since it contains some P_{l} with largest l, so any model for **A** with at least l elements is a model for that finite subset). By compactness, **A'** has a model!

But a model for **A'** must have infinitely many elements, as it has "at least k elements" for all k, and is also a model for **A**.

QED.

There are more powerful versions of the theorem around, that give you models of arbitrarily large *infinite* cardinalities.