Movatterモバイル変換


[0]ホーム

URL:


Jump to content
WikipediaThe Free Encyclopedia
Search

Löwenheim–Skolem theorem

From Wikipedia, the free encyclopedia
Existence and cardinality of models of logical theories

Inmathematical logic, theLöwenheim–Skolem theorem is a theorem on the existence andcardinality ofmodels, named afterLeopold Löwenheim andThoralf Skolem.

The precise formulation is given below. It implies that if acountablefirst-ordertheory has an infinitemodel, then for every infinitecardinal numberκ it has a model of sizeκ, and that no first-order theory with an infinite model can have a unique modelup 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 thecompactness theorem, that are used inLindström's theorem to characterizefirst-order logic. In general, the Löwenheim–Skolem theorem does not hold in stronger logics such assecond-order logic.

Theorem

[edit]
Illustration of the Löwenheim–Skolem theorem

In its general form, theLöwenheim–Skolem Theorem states that for everysignatureσ, every infiniteσ-structureM and every infinite cardinal numberκ ≥ |σ|, there is aσ-structureN such that|N| =κ and such that

  • ifκ < |M| thenN is an elementary substructure ofM;
  • ifκ ≥ |M| thenN is an elementary extension ofM.

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 thedownward Löwenheim–Skolem Theorem.[1]: 160–162  The part of the theorem asserting that a structure has elementary extensions of all larger cardinalities is known as theupward Löwenheim–Skolem Theorem.[2]

Discussion

[edit]

Below we elaborate on the general concept of signatures and structures.

Concepts

[edit]

Signatures

[edit]

Asignature consists of a set of function symbolsSfunc, a set of relation symbolsSrel, and a functionar:SfuncSrelN0{\displaystyle \operatorname {ar} :S_{\operatorname {func} }\cup S_{\operatorname {rel} }\rightarrow \mathbb {N} _{0}} representing thearity 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-ordertheory consists of a fixed signature and a fixed set of sentences (formulas with no free variables) in that signature.[3]: 40  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

[edit]

Given a signatureσ, aσ-structureMis 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σ inM is simply an element ofM. More generally, an interpretation of ann-ary function symbolf is a function fromMn toM. Similarly, an interpretation of a relation symbolR is ann-ary relation onM, i.e. a subset of Mn.

A substructure of aσ-structureM is obtained by taking a subsetN ofM 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 toN. Anelementary 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

[edit]

The statement given in the introduction follows immediately by takingM 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.[1]

A theory is calledcategorical if it has only one model, up to isomorphism. This term was introduced byVeblen (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 byGödel's incompleteness theorem.[1]

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 oftrue arithmetic, which satisfy every first-orderinduction axiom but have non-inductive subsets.

LetN denote the natural numbers andR 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 ofreal 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 characterizeR as a complete ordered field, is anon-first-order property.[1]: 161 

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 asSkolem's paradox; it shows that the notion of countability is notabsolute.[4]

Proof sketch

[edit]

Downward part

[edit]

For each first-orderσ{\displaystyle \sigma }-formulaφ(y,x1,,xn){\displaystyle \varphi (y,x_{1},\ldots ,x_{n})}, theaxiom of choice implies the existence of a function

fφ:MnM{\displaystyle f_{\varphi }:M^{n}\to M}

such that, for alla1,,anM{\displaystyle a_{1},\ldots ,a_{n}\in M}, either

Mφ(fφ(a1,,an),a1,,an){\displaystyle M\models \varphi (f_{\varphi }(a_{1},\dots ,a_{n}),a_{1},\dots ,a_{n})}

or

M¬yφ(y,a1,,an){\displaystyle M\models \neg \exists y\,\varphi (y,a_{1},\dots ,a_{n})}.

Applying the axiom of choice again we get a function from the first-order formulasφ{\displaystyle \varphi } to such functionsfφ{\displaystyle f_{\varphi }}.

The family of functionsfφ{\displaystyle f_{\varphi }} gives rise to apreclosure operatorF{\displaystyle F} on thepower set ofM{\displaystyle M}

F(A)={fφ(a1,,an)Mφσ;a1,,anA}{\displaystyle F(A)=\{f_{\varphi }(a_{1},\dots ,a_{n})\in M\mid \varphi \in \sigma ;\,a_{1},\dots ,a_{n}\in A\}}

forAM{\displaystyle A\subseteq M}.

IteratingF{\displaystyle F} countably many times results in aclosure operatorFω{\displaystyle F^{\omega }}. Taking an arbitrary subsetAM{\displaystyle A\subseteq M} such that|A|=κ{\displaystyle \left\vert A\right\vert =\kappa }, and having definedN=Fω(A){\displaystyle N=F^{\omega }(A)}, one can see that also|N|=κ{\displaystyle \left\vert N\right\vert =\kappa }. ThenN{\displaystyle N} is an elementary substructure ofM{\displaystyle M} by theTarski–Vaught test.

The trick used in this proof is essentially due to Skolem, who introduced function symbols for theSkolem functionsfφ{\displaystyle f_{\varphi }} into the language. One could also define thefφ{\displaystyle f_{\varphi }} aspartial functions such thatfφ{\displaystyle f_{\varphi }} is defined if and only ifMyφ(y,a1,,an){\displaystyle M\models \exists y\,\varphi (y,a_{1},\ldots ,a_{n})}. The only important point is thatF{\displaystyle F} is a preclosure operator such thatF(A){\displaystyle F(A)} contains a solution for every formula with parameters inA{\displaystyle A} which has a solution inM{\displaystyle M} and that

|F(A)||A|+|σ|+0{\displaystyle \left\vert F(A)\right\vert \leq \left\vert A\right\vert +\left\vert \sigma \right\vert +\aleph _{0}}.

Upward part

[edit]

First, one extends the signature by adding a new constant symbol for every element ofM{\displaystyle M}. The complete theory ofM{\displaystyle M} for the extended signatureσ{\displaystyle \sigma '} is called theelementary diagram ofM{\displaystyle M}. In the next step one addsκ{\displaystyle \kappa } many new constant symbols to the signature and adds to the elementary diagram ofM{\displaystyle M} the sentencescc{\displaystyle c\neq c'} for any two distinct new constant symbolsc{\displaystyle c} andc{\displaystyle c'}. Using thecompactness theorem, the resulting theory is easily seen to be consistent. Since its models must have cardinality at leastκ{\displaystyle \kappa }, the downward part of this theorem guarantees the existence of a modelN{\displaystyle N} which has cardinality exactlyκ{\displaystyle \kappa }. It contains an isomorphic copy ofM{\displaystyle M} as an elementary substructure.[5][6]: 100–102 

In other logics

[edit]
Main article:Löwenheim number

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 insecond-order logic has a model smaller than the firstsupercompact 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 anabstract logic.[7]: 134 

Historical notes

[edit]

This account is based mainly onDawson (1993). To understand the early history of model theory one must distinguish betweensyntactical consistency (no contradiction can be derived using the deduction rules for first-order logic) andsatisfiability (there is a model). Somewhat surprisingly, even before thecompleteness theorem made the distinction unnecessary, the termconsistent was used sometimes in one sense and sometimes in the other.

The first significant result in what later becamemodel theory wasLöwenheim's theorem inLeopold 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 generalPeirce–Schrödercalculus of relatives (relation algebra with quantifiers).[1] He also used the now antiquated notations ofErnst Schröder. For a summary of the paper in English and using modern notations seeBrady (2000, chapter 8).

According to the received historical view, Löwenheim's proof was faulty because it implicitly usedKőnig's lemma without proving it, although the lemma was not yet a published result at the time. In arevisionist account,Badesa (2004) considers that Löwenheim's proof was complete.

Skolem (1920) gave a (correct) proof using formulas in what would later be calledSkolem normal form and relying on the axiom of choice:

Every countable theory which is satisfiable in a modelM, is satisfiable in a countable substructure ofM.

Skolem (1922) 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) simplifiedSkolem (1920). Finally,Anatoly Ivanovich Maltsev (Анато́лий Ива́нович Ма́льцев, 1936) proved the Löwenheim–Skolem theorem in its full generality (Maltsev 1936). He cited a note by Skolem, according to which the theorem had been proved byAlfred Tarski in a seminar in 1928. Therefore, the general theorem is sometimes known as theLöwenheim–Skolem–Tarski theorem. But Tarski did not remember his proof, and it remains a mystery how he could do it without thecompactness 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."Hodges (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).

References

[edit]
  1. ^abcdeNourani, C. F.,A Functorial Model Theory: Newer Applications to Algebraic Topology, Descriptive Sets, and Computing Categories Topos (Toronto: Apple Academic Press;Boca Raton:CRC Press, 2014),pp. 160–162.
  2. ^Sheppard, B.,The Logic of Infinity (Cambridge:Cambridge University Press, 2014),p. 372.
  3. ^Haan, R. de,Parameterized Complexity in the Polynomial Hierarchy: Extending Parameterized Complexity Theory to Higher Levels of the Hierarchy (Berlin/Heidelberg:Springer, 2019),p. 40.
  4. ^Bays, T.,"Skolem's Paradox",Stanford Encyclopedia of Philosophy, Winter 2014.
  5. ^Church, A., &Langford, C. H., eds.,The Journal of Symbolic Logic (Storrs, CT:Association for Symbolic Logic, 1981), p. 529.
  6. ^Leary, C. C., & Kristiansen, L.,A Friendly Introduction to Mathematical Logic (Geneseo, NY: Milne Library, 2015),pp. 100–102.
  7. ^Chang, C. C., &Keisler, H. J.,Model Theory, 3rd ed. (Mineola &New York:Dover Publications, 1990),p. 134.

Sources

[edit]

The Löwenheim–Skolem theorem is treated in all introductory texts onmodel theory ormathematical logic.

Historical publications

[edit]

Secondary sources

[edit]

External links

[edit]
General
Theorems (list)
 and paradoxes
Logics
Traditional
Propositional
Predicate
Set theory
Types ofsets
Maps and cardinality
Set theories
Formal systems (list),
language and syntax
Example axiomatic
systems
 (list)
Proof theory
Model theory
Computability theory
Related
Retrieved from "https://en.wikipedia.org/w/index.php?title=Löwenheim–Skolem_theorem&oldid=1249338274"
Categories:
Hidden categories:

[8]ページ先頭

©2009-2025 Movatter.jp