Löwenheim–Skolem theorem
Encyclopedia
In mathematical logic
, the Löwenheim–Skolem theorem, named for Leopold Löwenheim
and Thoralf Skolem
, states that if a countable first-order theory has an infinite model, then for every infinite cardinal number
κ it has a model of size κ. The result implies that first-order theories are unable to control the cardinality of their infinite models, and that no first-order theory with an infinite model can have exactly one model up to isomorphism.
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
.
consists of a set of function symbols Sfunc, a set of relation symbols Srel, and a function
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.
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 Mn to M. Similarly, an interpretation of a relation symbol R is an n-ary relation on M, i.e. a subset of Mn.
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).
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 |N| = κ and
The theorem is often divided into two parts corresponding to the two bullets 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.
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. For historical variants of the theorem, see the notes below.
s) has a countable model. There are, of course, axiomatizations characterizing (N, +, ×, 0, 1) and (R, +, ×, 0, 1) up to isomorphism. The Löwenheim–Skolem theorem shows that these axiomatizations cannot be first-order. For example, the completeness of a linear order, which is used to characterize the real numbers as a complete ordered field, is a non-first-order property.
A theory is called categorical if it has only one model, up to isomorphism. This term was introduced by Oswald Veblen
in 1904, and for some time thereafter mathematicians hoped they could put mathematics on a solid foundation by describing a categorical first-order theory of some version of set theory. The Löwenheim–Skolem theorem dealt a first blow to this hope, as it implies that a first-order theory which has an infinite model cannot be categorical. Later, in 1931, the hope was shattered completely by Gödel's incompleteness theorem.
Many consequences of the Löwenheim–Skolem theorem seemed counterintuitive to logicians in the early 20th century, as the distinction between first-order and non-first-order properties was not yet understood. One such consequence is the existence of uncountable models of true arithmetic
, which satisfy every first-order induction axiom
but have non-inductive subsets. Another consequence that was considered particularly troubling is the existence of a countable model of set theory, which nevertheless must satisfy the sentence saying the real numbers are uncountable. This counterintuitive situation came to be known as Skolem's paradox
; it shows that the notion of countability is not absolute
.
-formula 
the axiom of choice implies the existence of a function
such that, for all
, either
or
Applying the axiom of choice again we get a function from the first order formulas
to such functions 
The family of functions
gives rise to a preclosure operator
on the power set of 
for
Iterating
countably many times results in a closure operator
Taking an arbitrary subset 
such that 
, and having defined 
one can see that also 
is an elementary substructure of 
by the Tarski–Vaught test.
The trick used in this proof is essentially due to Skolem, who introduced function symbols for the Skolem functions
into the language. One could also define the 
as partial function
s such that
is defined if and only if 
The only important point is that 
is a preclosure operator such that 
contains a solution for every formula with parameters in 
which has a solution in 
and that
' for any two distinct new constant symbols c and c' . Using the compactness theorem
, the resulting theory is easily seen to be consistent. Since its models must have cardinality at least κ, the downward part of this theorem guarantees the existence of a model N which has cardinality exactly κ. It contains an isomorphic copy of M as an elementary substructure.
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 "Über Möglichkeiten im Relativkalkül" (1915):
Löwenheim's proof, however, was faulty. Thoralf Skolem
(1920) gave a correct proof using formulas in what would later be called Skolem normal form and relying on the axiom of choice:
Skolem (1923) also proved the following weaker version without the axiom of choice:
Skolem (1929) simplified Skolem (1920). Finally, Anatoly Ivanovich Maltsev
(Анато́лий Ива́нович Ма́льцев, 1936) proved the Löwenheim–Skolem theorem in its full generality. He cited a note by Skolem, according to which the theorem had been proved by Alfred Tarski
in a seminar in 1928. Therefore the general theorem is sometimes known as the Löwenheim–Skolem–Tarski theorem. But Tarski did not remember his proof, and it remains a mystery how he could do it without the compactness theorem
.
It is somewhat ironic that Skolem's name is connected with the upward direction of the theorem as well as with the downward direction:
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, the Löwenheim–Skolem theorem, named for Leopold Löwenheim
Leopold Löwenheim
Leopold Löwenheim was a German mathematician, known for his work in mathematical logic. The Nazi regime forced him to retire because under the Nuremberg Laws he was considered only three quarters Aryan. In 1943 much of his work was destroyed during a bombing raid on Berlin...
and Thoralf Skolem
Thoralf Skolem
Thoralf Albert Skolem was a Norwegian mathematician known mainly for his work on mathematical logic and set theory.-Life:...
, states that if a countable first-order theory has an infinite model, then for every infinite cardinal number
Cardinal number
In mathematics, cardinal numbers, or cardinals for short, are a generalization of the natural numbers used to measure the cardinality of sets. The cardinality of a finite set is a natural number – the number of elements in the set. The transfinite cardinal numbers describe the sizes of infinite...
κ it has a model of size κ. The result implies that first-order theories are unable to control the cardinality of their infinite models, and that no first-order theory with an infinite model can have exactly one model up to isomorphism.
The (downward) Löwenheim–Skolem theorem is one of the two key properties, along with the compactness theorem
Compactness theorem
In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model...
, that are used in Lindström's theorem
Lindström's theorem
In mathematical logic, Lindström's theorem states that first-order logic is the strongest logic In mathematical logic, Lindström's theorem (named after Swedish logician Per Lindström) states that first-order logic is the strongest logic In mathematical logic, Lindström's theorem (named after...
to characterize first-order logic. In general, the Löwenheim–Skolem theorem does not hold in stronger logics such as second-order logic
Second-order logic
In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory....
.
Background
A signatureSignature (logic)
In logic, especially mathematical logic, a signature lists and describes the non-logical symbols of a formal language. In universal algebra, a signature lists the operations that characterize an algebraic structure. In model theory, signatures are used for both purposes.Signatures play the same...
consists of a set of function symbols Sfunc, a set of relation symbols Srel, and a function
representing the arityArity
In logic, mathematics, and computer science, the arity of a function or operation is the number of arguments or operands that the function takes. The arity of a relation is the dimension of the domain in the corresponding Cartesian product...
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.
Given a signature σ, a σ-structure
Structure (mathematical logic)
In universal algebra and in model theory, a structure consists of a set along with a collection of finitary operations and relations which are defined on it....
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 Mn to M. Similarly, an interpretation of a relation symbol R is an n-ary relation on M, i.e. a subset of Mn.
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
Elementary substructure
In model theory, a field within mathematical logic, two structures M and N of the same signature σ are called elementarily equivalent if they satisfy the same first-order σ-sentences....
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).
Precise statement
The modern statement of the theorem is both more general and stronger than the version for countable signatures stated in the introduction.In its general form, the Löwenheim–Skolem Theorem states that for every signature
Signature (logic)
In logic, especially mathematical logic, a signature lists and describes the non-logical symbols of a formal language. In universal algebra, a signature lists the operations that characterize an algebraic structure. In model theory, signatures are used for both purposes.Signatures play the same...
σ, every infinite σ-structure
Structure (mathematical logic)
In universal algebra and in model theory, a structure consists of a set along with a collection of finitary operations and relations which are defined on it....
M and every infinite cardinal number κ ≥ |σ| there is a σ-structure N such that |N| = κ and
- if κ < |M| then N is an elementary substructure of M;
- if κ > |M| then N is an elementary extension of M.
The theorem is often divided into two parts corresponding to the two bullets 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.
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. For historical variants of the theorem, see the notes below.
Examples and consequences
Let N denote the natural numbers and R the reals. It follows from the theorem that the theory of (N, +, ×, 0, 1) (the theory of true first-order arithmetic) has uncountable models, and that the theory of (R, +, ×, 0, 1) (the theory of real closed fieldReal closed field
In mathematics, a real closed field is a field F that has the same first-order properties as the field of real numbers. Some examples are the field of real numbers, the field of real algebraic numbers, and the field of hyperreal numbers.-Definitions:...
s) has a countable model. There are, of course, axiomatizations characterizing (N, +, ×, 0, 1) and (R, +, ×, 0, 1) up to isomorphism. The Löwenheim–Skolem theorem shows that these axiomatizations cannot be first-order. For example, the completeness of a linear order, which is used to characterize the real numbers as a complete ordered field, is a non-first-order property.
A theory is called categorical if it has only one model, up to isomorphism. This term was introduced by Oswald Veblen
Oswald Veblen
Oswald Veblen was an American mathematician, geometer and topologist, whose work found application in atomic physics and the theory of relativity. He proved the Jordan curve theorem in 1905.-Life:...
in 1904, and for some time thereafter mathematicians hoped they could put mathematics on a solid foundation by describing a categorical first-order theory of some version of set theory. The Löwenheim–Skolem theorem dealt a first blow to this hope, as it implies that a first-order theory which has an infinite model cannot be categorical. Later, in 1931, the hope was shattered completely by Gödel's incompleteness theorem.
Many consequences of the Löwenheim–Skolem theorem seemed counterintuitive to logicians in the early 20th century, as the distinction between first-order and non-first-order properties was not yet understood. One such consequence is the existence of uncountable models of true arithmetic
True arithmetic
In mathematical logic, true arithmetic is the theory Th of the natural numbers in the language of first-order Peano arithmetic...
, which satisfy every first-order induction axiom
Peano axioms
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano...
but have non-inductive subsets. Another consequence that was considered particularly troubling is the existence of a countable model of set theory, which nevertheless must satisfy the sentence saying the real numbers are uncountable. This counterintuitive situation came to be known as Skolem's paradox
Skolem's paradox
In mathematical logic and philosophy, Skolem's paradox is a seeming contradiction that arises from the downward Löwenheim–Skolem theorem. Thoralf Skolem was the first to discuss the seemingly contradictory aspects of the theorem, and to discover the relativity of set-theoretic notions now known as...
; it shows that the notion of countability is not absolute
Absoluteness (mathematical logic)
In mathematical logic, a formula is said to be absolute if it has the same truth value in each of some class of structures . Theorems about absoluteness typically establish relationships between the absoluteness of formulas and their syntactic form.There are two weaker forms of partial absoluteness...
.
Downward part
For each first-order-formula the axiom of choice implies the existence of a functionsuch that, for all
, eitheror
Applying the axiom of choice again we get a function from the first order formulas
to such functions The family of functions
gives rise to a preclosure operatorPreclosure operator
In topology, a preclosure operator, or Čech closure operator is a map between subsets of a set, similar to a topological closure operator, except that it is not required to be idempotent...
on the power set of for
Iterating
countably many times results in a closure operatorClosure operator
In mathematics, a closure operator on a set S is a function cl: P → P from the power set of S to itself which satisfies the following conditions for all sets X,Y ⊆ S....
Taking an arbitrary subset such that , and having defined one can see that also is an elementary substructure of by the Tarski–Vaught test.The trick used in this proof is essentially due to Skolem, who introduced function symbols for the Skolem functions
into the language. One could also define the as partial functionPartial function
In mathematics, a partial function from X to Y is a function ƒ: X' → Y, where X' is a subset of X. It generalizes the concept of a function by not forcing f to map every element of X to an element of Y . If X' = X, then ƒ is called a total function and is equivalent to a function...
s such that
is defined if and only if The only important point is that is a preclosure operator such that contains a solution for every formula with parameters in which has a solution in and thatUpward part
First, one extends the signature by adding a new constant symbol for every element of M. The complete theory of M for the extended signature σ' is called the elementary diagram of M. In the next step one adds κ many new constant symbols to the signature and adds to the elementary diagram of M the sentences c ≠ cCompactness theorem
In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model...
, the resulting theory is easily seen to be consistent. Since its models must have cardinality at least κ, the downward part of this theorem guarantees the existence of a model N which has cardinality exactly κ. It contains an isomorphic copy of M as an elementary substructure.
Historical notes
This account is based mainly on Dawson (1993). 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 theoremGödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
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
Model theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
was Löwenheim's theorem in Leopold Löwenheim
Leopold Löwenheim
Leopold Löwenheim was a German mathematician, known for his work in mathematical logic. The Nazi regime forced him to retire because under the Nuremberg Laws he was considered only three quarters Aryan. In 1943 much of his work was destroyed during a bombing raid on Berlin...
's publication "Über Möglichkeiten im Relativkalkül" (1915):
- For every countable signature σ, every σ-sentence which is satisfiable is satisfiable in a countable model.
Löwenheim's proof, however, was faulty. Thoralf Skolem
Thoralf Skolem
Thoralf Albert Skolem was a Norwegian mathematician known mainly for his work on mathematical logic and set theory.-Life:...
(1920) gave a correct proof using formulas in what would later be called Skolem normal form and relying on the axiom of choice:
- Every countable theory which is satisfiable in a model M, is satisfiable in a countable substructure of M.
Skolem (1923) also proved the following weaker version without the axiom of choice:
- Every countable theory which is satisfiable in a model is also satisfiable in a countable model.
Skolem (1929) simplified Skolem (1920). Finally, Anatoly Ivanovich Maltsev
Anatoly Maltsev
Anatoly Ivanovich Maltsev was born in Misheronsky, near Moscow, and died in Novosibirsk, USSR. He was a mathematician noted for his work on the decidability of various algebraic groups...
(Анато́лий Ива́нович Ма́льцев, 1936) proved the Löwenheim–Skolem theorem in its full generality. He cited a note by Skolem, according to which the theorem had been proved by Alfred Tarski
Alfred Tarski
Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
in a seminar in 1928. Therefore the general theorem is sometimes known as the Löwenheim–Skolem–Tarski theorem. But Tarski did not remember his proof, and it remains a mystery how he could do it without the compactness theorem
Compactness theorem
In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model...
.
It is somewhat ironic that Skolem's name is connected with the upward direction of the theorem as well as with the downward direction:
- "I follow custom in calling Corollary 6.1.4 the upward Löwenheim-Skolem theorem. But in fact Skolem didn't even believe it, because he didn't believe in the existence of uncountable sets." – HodgesWilfrid HodgesWilfrid Augustine Hodges is a British mathematician, known for his work in model theory. He was Professor of Mathematics at Queen Mary, University of London from 1987 to 2006, and is the author of numerous books on logic....
(1993).
- "Skolem [...] rejected the result as meaningless; Tarski [...] very reasonably responded that Skolem's formalist viewpoint ought to reckon the downward Löwenheim-Skolem theorem meaningless just like the upward." – Hodges (1993).
- "Legend has it that Thoralf Skolem, up until the end of his life, was scandalized by the association of his name to a result of this type, which he considered an absurdity, nondenumerable sets being, for him, fictions without real existence." – Poizat (2000).
Historical publications
- Skolem, ThoralfThoralf SkolemThoralf Albert Skolem was a Norwegian mathematician known mainly for his work on mathematical logic and set theory.-Life:...
(1923) Einige Bemerkungen zu axiomatischen Begründung der Mengenlehre, Mathematikerkongressen i Helsingfors 4.–7. Juli 1922, Den femte skandinaviska matematikerkongressen, Redogoerelse, 217–232.
Secondary sources
- Burris, Stanley N., Contributions of the Logicians, Part II, From Richard Dedekind to Gerhard Gentzen
- Burris, Stanley N., Downward Löwenheim–Skolem theorem
- Simpson, Stephen G. (1998), Model Theory