In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem.
The precise formulation is given below. It implies that if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ, and that no first-order theory with an infinite model can have a unique model up to isomorphism.
As a consequence, first-order theories are unable to control the cardinality of their infinite models.
The (downward) Löwenheim–Skolem theorem is one of the two key properties, along with the compactness theorem, that are used in Lindström's theorem to characterize first-order logic.
In general, the Löwenheim–Skolem theorem does not hold in stronger logics such as second-order logic.
Theorem
thumb|Illustration of the Löwenheim–Skolem theorem
In its general form, the Löwenheim–Skolem Theorem states that for every signature σ, every infinite σ-structure M and every infinite cardinal number , there is a σ-structure N such that and such that
- if then N is an elementary substructure of M;
- if then N is an elementary extension of M.
The theorem is often divided into two parts corresponding to the two cases above. The part of the theorem asserting that a structure has elementary substructures of all smaller infinite cardinalities is known as the downward Löwenheim–Skolem Theorem. The part of the theorem asserting that a structure has elementary extensions of all larger cardinalities is known as the upward Löwenheim–Skolem Theorem.
Discussion
Below we elaborate on the general concept of signatures and structures.
Concepts
Signatures
A signature consists of a set of function symbols S<sub>func</sub>, a set of relation symbols S<sub>rel</sub>, and a function <math>\operatorname{ar}: S_{\operatorname{func\cup S_{\operatorname{rel \rightarrow \mathbb{N}_0</math> representing the arity of function and relation symbols. (A nullary function symbol is called a constant symbol.) In the context of first-order logic, a signature is sometimes called a language. It is called countable if the set of function and relation symbols in it is countable, and in general the cardinality of a signature is the cardinality of the set of all the symbols it contains.
A first-order theory consists of a fixed signature and a fixed set of sentences (formulas with no free variables) in that signature. Theories are often specified by giving a list of axioms that generate the theory, or by giving a structure and taking the theory to consist of the sentences satisfied by the structure.
Structures / Models
Given a signature σ, a σ-structure M
is a concrete interpretation of the symbols in σ. It consists of an underlying set (often also denoted by "M") together with an interpretation of the function and relation symbols of σ. An interpretation of a constant symbol of σ in M is simply an element of M. More generally, an interpretation of an n-ary function symbol f is a function from M<sup>n</sup> to M. Similarly, an interpretation of a relation symbol R is an n-ary relation on M, i.e. a subset of M<sup>n</sup>.
A substructure of a σ-structure M is obtained by taking a subset N of M which is closed under the interpretations of all the function symbols in σ (hence includes the interpretations of all constant symbols in σ), and then restricting the interpretations of the relation symbols to N. An elementary substructure is a very special case of this; in particular an elementary substructure satisfies exactly the same first-order sentences as the original structure (its elementary extension).
Consequences
The statement given in the introduction follows immediately by taking M to be an infinite model of the theory. The proof of the upward part of the theorem also shows that a theory with arbitrarily large finite models must have an infinite model; sometimes this is considered to be part of the theorem.
Proof sketch
Downward part
For each first-order <math>\sigma </math>-formula <math>\varphi(y,x_{1}, \ldots, x_{n})</math>, the axiom of choice implies the existence of a function
<math display="block">f_{\varphi}: M^n\to M</math>
such that, for all <math>a_{1}, \ldots, a_{n} \in M</math>, either
<math display="block">M\models\varphi(f_{\varphi} (a_1, \dots, a_n), a_1, \dots, a_n)</math>
or
<math display="block">M\models\neg\exists y\, \varphi(y, a_1, \dots, a_n)</math>.
Applying the axiom of choice again we get a function from the first-order formulas <math>\varphi</math> to such functions <math>f_{\varphi}</math>.
The family of functions <math>f_{\varphi}</math> gives rise to a preclosure operator <math>F </math> on the power set of <math>M </math>
<math display="block">F(A) = \{f_{\varphi}(a_1, \dots, a_n) \in M \mid \varphi \in \sigma ; \, a_1, \dots, a_n \in A \} </math>
for <math>A \subseteq M</math>.
Iterating <math>F </math> countably many times results in a closure operator <math>F^{\omega}</math>. Taking an arbitrary subset <math>A \subseteq M</math> such that <math>\left\vert A \right\vert = \kappa</math>, and having defined <math>N = F^{\omega}(A)</math>, one can see that also <math>\left\vert N \right\vert = \kappa</math>. Then <math>N </math> is an elementary substructure of <math>M </math> by the Tarski–Vaught test.
The trick used in this proof is essentially due to Skolem, who introduced function symbols for the Skolem functions <math>f_{\varphi}</math> into the language. One could also define the <math>f_{\varphi}</math> as partial functions such that <math>f_{\varphi}</math> is defined if and only if <math>M \models \exists y\, \varphi(y,a_1,\ldots,a_n)</math>. The only important point is that <math>F</math> is a preclosure operator such that <math>F(A) </math> contains a solution for every formula with parameters in <math>A </math> which has a solution in <math>M</math> and that
<math display="block">\left\vert F(A) \right\vert \leq \left\vert A \right\vert + \left\vert \sigma \right\vert + \aleph_0.</math>
Upward part
First, one extends the signature by adding a new constant symbol for every element of <math>M</math>. The complete theory of <math>M</math> for the extended signature <math>\sigma'</math> is called the elementary diagram of <math>M</math>. In the next step one adds <math>\kappa</math> many new constant symbols to the signature and adds to the elementary diagram of <math>M</math> the sentences <math>c \neq c'</math> for any two distinct new constant symbols <math>c</math> and <math>c'</math>. Using the compactness theorem, the resulting theory is easily seen to be consistent. Since its models must have cardinality at least <math>\kappa</math>, the downward part of this theorem guarantees the existence of a model <math>N</math> which has cardinality exactly <math>\kappa</math>. It contains an isomorphic copy of <math>M</math> as an elementary substructure.
In other logics
Although the (classical) Löwenheim–Skolem theorem is tied very closely to first-order logic, variants hold for other logics. For example, every consistent theory in second-order logic has a model smaller than the first supercompact cardinal (assuming one exists). The minimum size at which a (downward) Löwenheim–Skolem–type theorem applies in a logic is known as the Löwenheim number, and can be used to characterize that logic's strength. Moreover, if we go beyond first-order logic, we must give up one of three things: countable compactness, the downward Löwenheim–Skolem Theorem, or the properties of an abstract logic.
Historical notes
This account is based mainly on . To understand the early history of model theory one must distinguish between syntactical consistency (no contradiction can be derived using the deduction rules for first-order logic) and satisfiability (there is a model). Somewhat surprisingly, even before the completeness theorem made the distinction unnecessary, the term consistent was used sometimes in one sense and sometimes in the other.
The first significant result in what later became model theory was Löwenheim's theorem in Leopold Löwenheim's publication [On possibilities in the calculus of relatives] (1915):
Löwenheim's paper was actually concerned with the more general Peirce–Schröder calculus of relatives (relation algebra with quantifiers).