In
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of forma ...
, the Löwenheim–Skolem theorem is a theorem on the existence and
cardinality of
models
A model is an informative representation of an object, person or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin ''modulus'', a measure.
Models c ...
, named after
Leopold Löwenheim and
Thoralf Skolem.
The precise formulation is given below. It implies that if a
countable first-order
In mathematics and other formal sciences, first-order or first order most often means either:
* "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of hig ...
theory
A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may ...
has an infinite
model, then for every infinite
cardinal number
In mathematics, cardinal numbers, or cardinals for short, are a generalization of the natural numbers used to measure the cardinality (size) of sets. The cardinality of a finite set is a natural number: the number of elements in the set. ...
''κ'' 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 In mathematical logic, Lindström's theorem (named after Swedish logician Per Lindström, who published it in 1969) states that first-order logic is the '' strongest logic'' (satisfying certain conditions, e.g. closure under classical negation) h ...
to characterize
first-order logic.
In general, the Löwenheim–Skolem theorem does not hold in stronger logics such as
second-order logic.
Theorem
In its general form, the Löwenheim–Skolem Theorem states that for every
signature
A signature (; from la, signare, "to sign") is a Handwriting, handwritten (and often Stylization, stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and ...
''σ'', every infinite ''σ''-
structure
A structure is an arrangement and organization of interrelated elements in a material object or system, or the object or system so organized. Material structures include man-made objects such as buildings and machines and natural objects such a ...
''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.
[Nourani, C. F., ''A Functorial Model Theory: Newer Applications to Algebraic Topology, Descriptive Sets, and Computing Categories Topos'' (]Toronto
Toronto ( ; or ) is the capital city of the Canadian province of Ontario. With a recorded population of 2,794,356 in 2021, it is the most populous city in Canada and the fourth most populous city in North America. The city is the anch ...
: Apple Academic Press; Boca Raton
Boca Raton ( ; es, Boca Ratón, link=no, ) is a city in Palm Beach County, Florida, United States. It was first incorporated on August 2, 1924, as "Bocaratone," and then incorporated as "Boca Raton" in 1925. The population was 97,422 in the ...
: CRC Press
The CRC Press, LLC is an American publishing group that specializes in producing technical books. Many of their books relate to engineering, science and mathematics. Their scope also includes books on business, forensics and information techn ...
, 2014)
pp. 160–161
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
A signature (; from la, signare, "to sign") is a Handwriting, handwritten (and often Stylization, stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and ...
consists of a set of function symbols ''S''
func, a set of relation symbols ''S''
rel, and a function
representing the
arity
Arity () is the number of arguments or operands taken by a function, operation or relation in logic, mathematics, and computer science. In mathematics, arity may also be named ''rank'', but this word can have many other meanings in mathematics. ...
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
A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may ...
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
A structure is an arrangement and organization of interrelated elements in a material object or system, or the object or system so organized. Material structures include man-made objects such as buildings and machines and natural objects such a ...
''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''
''n'' to ''M''. Similarly, an interpretation of a relation symbol ''R'' is an ''n''-ary relation on ''M'', i.e. a subset of ''M''
''n''.
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 In model theory, a branch of mathematical logic, two structures ''M'' and ''N'' of the same signature ''σ'' are called elementarily equivalent if they satisfy the same first-order ''σ''-sentences.
If ''N'' is a substructure of ''M'', one often ...
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.
A theory is called categorical if it has only one model, up to isomorphism. This term was introduced by , 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
In mathematical logic, true arithmetic is the set of all true first-order statements about the arithmetic of natural numbers. This is the theory associated with the standard model of the Peano axioms in the language of the first-order Peano a ...
, which satisfy every first-order
induction axiom but have non-inductive subsets.
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 fields) 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, in the theory of the real numbers, the completeness of a linear order used to characterize R as a complete ordered field, is a
non-first-order property.
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.
Cantor's theorem states that some sets are uncountable. This counterintuitive situation came to be known as
Skolem's paradox; it shows that the notion of countability is not
absolute Absolute may refer to:
Companies
* Absolute Entertainment, a video game publisher
* Absolute Radio, (formerly Virgin Radio), independent national radio station in the UK
* Absolute Software Corporation, specializes in security and data risk manag ...
.
Proof sketch
Downward part
For each first-order
-formula
the
axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
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
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. That is, a preclosure operator obeys only three of the four ...
on the
power set of
:
for
Iterating
countably many times results in a
closure operator In mathematics, a closure operator on a set ''S'' is a function \operatorname: \mathcal(S)\rightarrow \mathcal(S) from the power set of ''S'' to itself that satisfies the following conditions for all sets X,Y\subseteq S
:
Closure operators are de ...
Taking an arbitrary subset
such that
, and having defined
one can see that also
Then
is an elementary substructure of
by the
Tarski–Vaught test In model theory, a branch of mathematical logic, two structures ''M'' and ''N'' of the same signature ''σ'' are called elementarily equivalent if they satisfy the same first-order ''σ''-sentences.
If ''N'' is a substructure of ''M'', one of ...
.
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 functions 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
:
Upward 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'' ≠ ''c
''' 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.
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
''Abstract Logic'' is the first collaborative live album by bassist Jonas Hellborg and guitarist Shawn Lane, released in 1995 through Day Eight Music; a remastered and remixed edition, containing a revised track listing and two extra tracks, was r ...
.
[ Chang, C. C., & Keisler, H. J., ''Model Theory'', 3rd ed. ( Mineola & New York: ]Dover Publications
Dover Publications, also known as Dover Books, is an American book publisher founded in 1941 by Hayward and Blanche Cirker. It primarily reissues books that are out of print from their original publishers. These are often, but not always, books ...
, 1990)
p. 134
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
In mathematical logic, model theory is the study of the relationship between theory (mathematical logic), formal theories (a collection of Sentence (mathematical logic), sentences in a formal language expressing statements about a Structure (math ...
was ''Löwenheim's theorem'' in
Leopold Löwenheim's publication "Über Möglichkeiten im Relativkalkül" (1915):
:For every countable signature ''σ'', every ''σ''-sentence that is satisfiable is satisfiable in a countable model.
Löwenheim's paper was actually concerned with the more general
Peirce–Schröder ''
calculus of relatives
Calculus, originally called infinitesimal calculus or "the calculus of infinitesimals", is the mathematical study of continuous change, in the same way that geometry is the study of shape, and algebra is the study of generalizations of arit ...
'' (
relation algebra
In mathematics and abstract algebra, a relation algebra is a residuated Boolean algebra expanded with an involution called converse, a unary operation. The motivating example of a relation algebra is the algebra 2''X''² of all binary relations ...
with quantifiers).
He also used the now antiquated notations of
Ernst Schröder. For a summary of the paper in English and using modern notations see .
According to the received historical view, Löwenheim's proof was faulty because it implicitly used
Kőnig's lemma without proving it, although the lemma was not yet a published result at the time. In a
revisionist account, considers that Löwenheim's proof was complete.
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''.
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.
simplified . 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:
:''"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."'' – .
:''"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."'' – .
:''"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."'' – .
References
Sources
The Löwenheim–Skolem theorem is treated in all introductory texts on
model theory
In mathematical logic, model theory is the study of the relationship between theory (mathematical logic), formal theories (a collection of Sentence (mathematical logic), sentences in a formal language expressing statements about a Structure (math ...
or
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of forma ...
.
Historical publications
*
** ()
*
*
** ()
*
** ()
*
*
Secondary sources
* ; A more concise account appears in chapter 9 of
*
*
*
*
*
External links
*
* 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
{{DEFAULTSORT:Lowenheim-Skolem Theorem
Mathematical logic
Metatheorems
Model theory
Theorems in the foundations of mathematics