Table of contents
1 What the theorem says
2 Examples
3 A terse sketch of the proof
4 More general "Löwenheim-Skolem theorems"

What the theorem says

In mathematical logic, the classic Löwenheim-Skolem theorem states that any "model" M has a countably infinite submodel N that satisfies exactly the same set of first-order sentences that M satisfies. A "model", in this sense, consists of an underlying set (often also denoted) "M" and a set of relations on the underlying set M and a set of functions (sometimes taking several arguments) from M into itself.

Examples

For example, the set of all real numbers could be the underlying set; the order relation "<" could be the one relation, and addition and multiplication could be the two functions belonging to the model. The axioms of ordered fields are first-order sentences; the least-upper-bound axiom is not first-order, but second-order. The theorem implies that some countably infinite subfield satisfies all first-order sentences satisfied by the real numbers. (Being a countable ordered field, it cannot satisfy the least-upper-bound axiom.) For example, the assertion that a particular polynomial equation has a real solution is a first-order sentence and therefore would be true in the countable submodel whose existence is asserted.

Another example of a "model" is the set of all affine subspaces of an affine space, as the underlying set, and the "incidence" relation as the one relation (e.g., a line is "incident" to a plane if the line lies within the plane; a point is incident to a plane if the point is on the plane, etc.; the incidence relation partially orders the underlying set).

By now the reader should begin to suspect that most mathematical structures, in particular, most members of most categories that mathematicians consider, are "models" in the sense defined here.

A terse sketch of the proof

For every first-order sentence of the form

or

that is true in the model M, there is a Skolem function g, i.e., a function that maps the x to the y whose existence is asserted, so that

is true in M. Since there may be many such values of y, the
axiom of choice must be invoked in order to infer the existence of the Skolem function.

Only countably many members of the model can be definable by first-order formulas.

[The claim above would bear elaboration!]

Here is the idea of the proof: Start with the set of all first-order-definable members of the model, and close under all Skolem functions. The closure must be at most countably infinite. That subset of the model is the submodel whose existence the theorem asserts.

More general "Löwenheim-Skolem theorems"

The theorem above assumes finite or countably infinite language. More general Löwenheim-Skolem theorems make other assumptions about cardinality. Some, like this classic one, assert the existence of smaller submodels; others assert the existence of models of larger cardinality.