In this note I sketch the proof of the Löwenheim-Skølem (or Löwenheim-Skølem-Tarski) theorem for first order theories. This basic result of model theory is really a consequence of a set theoretic combinatorial lemma, as the proof will demonstrate.
Let be a first order language, understood as a set of constant, function, and relation symbols. Let
so is
unless
is finite, in which case we take
Talking about
rather than
simplifies the presentation slightly.
The Löwenheim-Skølem theorem is concerned with the possible infinite sizes of models of first order theories. Of course, a theory could only have finite models; the result does not say anything about
if that is the case.
Theorem 1 If
is a first order theory in a language
and there is at least one infinite model of
then there are models of
of size
for all
We will prove a more precise statement. Before stating it, note that it is possible to have a theory in some uncountable language
such that
has models of certain infinite sizes, but not all. Theorem 1 does not say anything about infinite models of
of size
What cardinals in this range are the possible sizes of models of
is actually a rather difficult problem, and we will not address it.
To state the more precise version that we will prove, we need to review the notion of elementary substructure. Thoughout the note we use the notational convention that if is a
-structure, its underlying universe is
Recall that if and
are
-structures, we say that
( is a substructure of
) iff:
-
.
-
for any
and any
-ary relation symbol
in
-
for all constant symbols
in
-
for any
and any
-ary function symbol
in
For example, a subgroup of a group is simply a subset
such that
and
is closed under
A subgroup may have significantly different properties than the group it comes from. Consider, for example,
A substructure of
is elementary, in symbols
iff for any -formula
and any
we have that
iff
This is a much more strict notion than simply being a substructure. It is easy to check that is not elementary in
for example.
Note that if then, for any
-theory
we have that
iff
(Simply consider sentences
in the definition above.)
Here is a natural example of how to obtain elementary extensions of a given model Expand the language
into a larger language
by adding to
a set of
many new constant symbols
for
We can expand
to an
-structure simply by setting
Let
denote this expanded structure. Consider the theory
where the theory is of course considered in the language
Let
be any model of
Then there is a natural way of identifying
with an elementary extension of
More precisely, the map
given by
is elementary, meaning that
iff
for any -formula
and any
It easily follows that the pointwise image is the universe of an elementary substructure of
that is isomorphic to
so we might as well assume that
is the identity. By considering the restriction of
to language
(i.e., by “forgetting” about the new constant symbols), we obtain this way an elementary extension of
In fact, it is easy to check that if then there is a natural expansion of
to an
-structure that models
so all elementary extensions of
arise in this fashion. From the observations above, Theorem 1 then follows from the following more precise version, where we write
for
and say that
is infinite iff
is.
Theorem 2 Let
be an infinite
-structure.
- For any cardinal
there is
with
- For any cardinal
and any
with
there is
such that
and
We note first that item 1 follows from item 2 and compactness: Consider the language obtained by adding to
a set of
many new constant symbols
and
many new constant symbols
In this language, consider the theory
obtained by adding to
the axioms
for all
where
is as above. This theory is consistent, by compactness (using that
is infinite), so it has models. But any model
of
can be naturally identified with an elementary extension of
and has size at least
By item 2, there is an elementary substructure of
that contains
and has size precisely
Since
it follows that the reduct of
to language
is indeed an elementary extension of
of size
To prove item 2, we expand the language in a different manner.
For this, we need the notion of Skølem functions. Syntactically, a Skølem function for a formula is simply a new function symbol
for an
-ary function. Semantically: Given a structure
in a language containing
and
we call the interpretaion
a Skølem function iff, whenever
and
then in fact
We say that a language is closed under Skølem functions if a function symbol
is in the language for each
in the language. We say that a structure
in this language has Skølem functions if it satisfies all axioms of the form
Note that using the axiom of choice it is straightforward to define interpretations of all the function symbols so that these axioms are satisfied: Simply fix a well-ordering of
and take
as the least
(in the sense of the well-ordering) that witnesses
if such is the case, or as the least element of
otherwise.
It is straightforward to expand a language to one closed under Skølem functions: Given let
and set
is an
-formula
for all
Finally, set
and note that
is as wanted.
Moreover, as is easily verified by induction on
This means that to prove item 2, we may as well assume that
is closed under Skølem functions and
has Skølem functions to begin with.
The point of all this is that if has Skølem functions and
, then automatically
This follows from the following test for elementarity:
Lemma 3 (Tarski-Vaught criterion) Suppose
and that whenever
and
then there exists
such that
Then
![]()
Proof: By induction in the complexity of
The usefulness of the test derives from the fact that it only mentions satisfaction in rather than in both
and
To see how Lemma 3 allows us to conclude the claim made above, suppose that has Skølem functions, and that
is a substructure of
Then, automatically, the hypothesis of Lemma 3 is satisfied, since
must be closed under the restrictions of all the functions
being a substructure, meaning that
whenever
It then follows that
as claimed.
Moreover, note that if and
is (nonempty and) closed under all the Skølem functions from
then
is the universe of a (necessarily elementary) substructure of
To see this, note that from the definition of substructure given above, all that we require is that
for all constant symbols
in
and that
whenever
for all function symbols
in
But consider Then
for any
so if
is nonempty and as above, then
contains the interpretaions of all the constant symbols from the language. (The only reason we added
to the formula
rather than just taking
is to avoid having
to be
-ary, since our official definition of function symbols requires this not to be the case. Similarly, consider
Then
We have finally arrived at the combinatorial core of Theorem 2. Some notation is useful (we follow Kunen Set theory. An introduction to independence proofs in the remainder of this note).
For say that
is an
-ary function on a set
iff
and, as usual,
or
and
(This is a natural extension of the notion for
Note that
and any
is simply picking an element of
here we are just identifying
and this element.) Say that
is a finitary function on
iff
is
-ary on
for some
Say that is closed under a finitary function
iff
where
if
is
-ary, and
if
is
-ary,
If
is a set of finitary functions on
we say that
is closed under
iff
for all
The closure of
under
is the
-smallest
such that
and
is closed under
From the preliminaries above, it is clear that the following completes the proof of Theorem 2, since we can take as the set
in item 2 (or rather, a superset of
of size exactly
), as
the cardinal
as
the set
and as
the set of (interpretations of) Skølem functions on
Lemma 4 Suppose that
is infinite, that
![]()
and that
is a set of at most
many finitary functions on
Then the closure of
under
exists and has size at most
![]()
Proof: Given write
for
Set
and
for all
Finally, set
Then, by induction on
each
is contained in any subset of
closed under
that contains
Since
itself is closed under
it follows that
is the closure of
By induction,
for all
and so the same holds for
Typeset using LaTeX2WP. Here is a printable version of this post.
[…] This can be established by an argument very similar to the one we used in the notes on the Löwenheim-Sko lem theorem. Namely, for and each of its subformulas consider Sko lem functions from Let be the set of […]
[…] This can be established by an argument very similar to the one we used in the notes on the Löwenheim-Sko lem theorem. Namely, for and each of its subformulas consider Sko lem functions from Let be the set of […]