Model theory
From Wikipedia, the free encyclopedia
In mathematics, model theory is the study of (classes of) mathematical structures such as groups, fields, graphs or even models of set theory using tools from mathematical logic. Model theory has close ties to algebra and universal algebra. This article focuses on finitary first order model theory of infinite structures. The model theoretic study of finite structures (for which see finite model theory) diverges significantly from the study of infinite structures in both the problems studied and the techniques used. Model theory in higher-order logics or infinitary logics is hampered by the fact that completeness does not in general hold for these logics. However, a great deal of study has also been done in such languages. The role of model theoryModel theory recognises and is intimately concerned with a duality: It examines semantical elements by means of syntactical elements of a corresponding language. To quote the first page of Chang and Keisler (1990):
In a similar way as proof theory, model theory is situated in an area of interdisciplinarity between mathematics, philosophy, and computer science. The most important professional organization in the field of model theory is the Association for Symbolic Logic. The areas of model theoryAn incomplete and somewhat arbitrary subdivision of model theory is into classical model theory, model theory applied to groups and fields, and geometric model theory. A missing subdivision is computable model theory, but this can arguably be viewed as an independent subfield of logic. Examples of early theorems from classical model theory include Gödel's completeness theorem, the upward and downward Löwenheim–Skolem theorems, Vaught's two cardinal theorem, Scott's isomorphism theorem, the omitting types theorem, and the Ryll-Nardjewski theorem. Examples of early results from model theory applied to fields are Tarski's elimination of quantifiers for real closed fields, Ax's theorem on pseudo-finite fields, and Robinson's development of nonstandard analysis. An important step in the evolution of classical model theory occurred with the birth of stability theory (through Morley's theorem on totally categorical theories and Shelah's classification program), which developed a calculus of independence and rank based on syntactical conditions satisfied by theories. During the last several decades applied model theory has repeatedly merged with the more pure stability theory. The result of this synthesis is called geometric model theory in this article (which is taken to include o-minimality, for example, as well as classical geometric stability theory). An example of a theorem from geometric model theory is Hrushovski's proof of the Mordell-Lang conjecture for function fields. The ambition of geometric model theory is to provide a geography of mathematics by embarking on a detailed study of definable sets in various mathematical structures, aided by the substantial tools developed in the study of pure model theory. Universal algebraFundamental concepts in universal algebra are signatures σ and σ-algebras. Since these concepts are formally defined in the article on structures, the present article can content itself with an informal introduction which consists in examples of how these terms are used.
This is a very efficient way to define most classes of algebraic structures, because there is also the concept of σ-homomorphism, which correctly specializes to the usual notions of homomorphism for groups, semigroups, magmas and rings. For this to work, the signature must be chosen well. For example multiplication with a non-zero integer is a magma homomorphism on Failed to parse (Missing texvc executable; please see math/README to configure.): \mathbb Z which is not a group homomorphism. Using σ-congruences (equivalence relations that respect the operations of σ), which play the role of kernels of homomorphisms, universal algebra can state and prove the isomorphism theorems in great:
are two congruence relations on A, then (A/δ) / (ε/δ) is isomorphic to A/ε. Terms such as the σring-term t=t(u,v,w) given by (u + (v×w)) − 1 are used to define identities t=t', but also to construct free algebras. An equational class is a class of structures which, like the examples above and many others, is defined as the class of all σ-structures which satisfy a certain set of identities. An important non-trivial tool in universal algebra are ultraproducts Failed to parse (Missing texvc executable; please see math/README to configure.): \Pi_{i\in I}A_i/U , where I is an infinite set indexing a system of σ-structures Ai, and U is an ultrafilter on I. They are used in the proof of Birkhoff's theorem:
While model theory is generally considered a part of mathematical logic, universal algebra, which grew out of Alfred North Whitehead's (1898) work on abstract algebra, is part of algebra. This is reflected by their respective MSC classifications. Nevertheless model theory can be seen as an extension of universal algebra. Finite model theoryFinite model theory is the area of model theory which has the closest ties to universal algebra. Like some parts of universal algebra, and in contrast with the other areas of model theory, it is mainly concerned with finite algebras, or more generally, with finite σ-structures for signatures σ which may contain relation symbols as in the following example:
and Failed to parse (Missing texvc executable; please see math/README to configure.): \forall u\neg(uEu) . A σ-homomorphism is a map that commutes with the operations and preserves the relations in σ. This definition gives rise to the usual notion of graph homomorphism, which has the interesting property that a bijective homomorphism need not be invertible. Structures are also a part of universal algebra; after all, some algebraic structures such as ordered groups have a binary relation <. What distinguishes finite model theory from universal algebra is its use of more general logical sentences (as in the example above) in place of identities. (In a model-theoretic context an identity t=t' is written as a sentence Failed to parse (Missing texvc executable; please see math/README to configure.): \forall u_1u_2\dots u_n(t=t') .) The logics employed in finite model theory are often substantially more expressive than first-order logic, the standard logic for model theory of infinite structures. First-order logicWhereas universal algebra provides the semantics for a signature, logic provides the syntax. With terms, identities and quasi-identities, even universal algebra has some limited syntactic tools; first-order logic is the result of making quantification explicit and adding negation into the picture. A first-order formula is built out of atomic formulas such as R(f(x,y),z) or y = x + 1 by means of the Boolean connectives Failed to parse (Missing texvc executable; please see math/README to configure.): \neg,\land,\lor,\rightarrow and prefixing of quantifiers Failed to parse (Missing texvc executable; please see math/README to configure.): \forall v or Failed to parse (Missing texvc executable; please see math/README to configure.): \exists v . A sentence is a formula in which each occurrence of a variable is in the scope of a corresponding quantifier. Examples for formulas are φ (or φ(x) to mark the fact that at most x is an unbound variable in φ) and ψ defined as follows:
of the natural numbers, for example, an element n satisfies the formula φ iff it n a prime number. The formula ψ similarly defines irreducibility. Tarski gave a rigorous definition, sometimes called "Tarski's definition of truth", for the satisfaction relation Failed to parse (Missing texvc executable; please see math/README to configure.): \models , so that one easily proves:
is a prime number.
is irreducible. A set T of sentences is called a (first-order) theory. A theory is satisfiable if it has a model Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal M\models T , i.e. a structure (of the appropriate signature) which satisfies all the sentences in the set T. Consistency of a theory is usually defined in a syntactical way, but in first-order logic by the completeness theorem there is no need to distinguish between satisfiability and consistency. Therefore model theorists often use "consistent" as a synonym for "satisfiable". A theory is called categorical if it determines a structure up to isomorphism, but it turns out that this definition is not useful, due to serious restrictions in the expressivity of first-order logic. The Löwenheim-Skolem theorem implies that for every theory T[1] which has an infinite model and for every infinite cardinal number κ, there is a model Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal M\models T such that the number of elements of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal M is exactly κ. Therefore only finite structures can be described by a categorical theory. Lack of expressivity (when compared to higher logics such as second-order logic) has its advantages, though. For model theorists the Löwenheim-Skolem theorem is an important practical tool rather than the source of Skolem's paradox. First-order logic is in some sense the most expressive logic for which both the Löwenheim-Skolem theorem and the compactness theorem hold:
This important theorem, due to Gödel, is of central importance in infinite model theory, where the words "by compactness" are commonplace. One way to prove it is by means of ultraproducts. An important question when one wants to apply model theory to a specific class of structures is whether this class is an elementary class, i.e. whether its members can be characterized as those structures which satisfy a first-order theory. Axiomatizability, elimination of quantifiers, and model-completenessThe first step, often trivial, for applying the methods of model theory to a class of mathematical objects such as groups, or trees in the sense of graph theory, is to choose a signature σ and represent the objects as σ-structures. The next step is to show that the class is axiomatizable, i.e. there is a theory T such that a σ-structure is in the class if and only if it satisfies T. (This step fails for the trees, since connectedness cannot be expressed in first order.) Axiomatizability ensures that model theory can speak about the right objects. Quantifier elimination can be seen as a condition which ensures that model theory does not say too much about the objects. A theory T has quantifier elimination if every first-order formula φ(x1,...,xn) over its signature is equivalent modulo T to a first-order formula ψ(x1,...,xn) without quantifiers, i.e. Failed to parse (Missing texvc executable; please see math/README to configure.): \forall x_1\dots\forall x_n(\phi(x_1,\dots,x_n)\leftrightarrow \psi(x_1,\dots,x_n)) holds in all models of T. For example the theory of algebraically closed fields in the signature σring=(×,+,−,0,1) has quantifier elimination because every formula is equivalent to a Boolean combination of equations between polynomials. A substructure of a σ-structure is a subset of its domain, closed under all functions in its signature σ, which is regarded as a σ-structure by restricting all functions and relations in σ to the subset. An embedding of a σ-structure Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal A into another σ-structure Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal B is a map f: A → B between the domains which can be written as an isomorphism of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal A with a substructure of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal B . Every embedding is an injective homomorphism, but the converse holds only if the signature contains no relation symbols. If T has quantifier elimination, then every substructure of a model of T again satisfies T, and in fact something stronger holds: For every formula φ(x1,...,xn) and every tuple a1,...,an in the substructure, φ(a1,...,an) is true in the substructure if and only if it is true in the bigger structure. A substructure with this property is called an elementary substructure. If a theory does not have quantifier elimination, one can add additional symbols to its signature so that it does. Early model theory spent much effort on proving axiomatizability and quantifier elimination results for specific theories, especially in algebra. But often instead of quantifier elimination a weaker property suffices: A theory T is called model-complete if every substructure of a model of T which is itself a model of T is an elementary substructure. There is a useful criterion for testing whether a substructure is an elementary substructure, called the Tarski-Vaught test. It follows from this criterion that a theory T is model-complete if and only if every first-order formula φ(x1,...,xn) over its signature is equivalent modulo T to an existential first-order formula, i.e. a formula of the following form:
, where ψ is quantifier free. Model theory and set theorySet theory (which is expressed in a countable language) has a countable model; this is known as Skolem's paradox, since there are sentences in set theory which postulate the existence of uncountable sets and yet these sentences are true in our countable model. Particularly the proof of the independence of the continuum hypothesis requires considering sets in models which appear to be uncountable when viewed from within the model, but are countable to someone outside the model. The model-theoretic viewpoint has been useful in set theory; for example in Kurt Gödel's work on the constructible universe, which, along with the method of forcing developed by Paul Cohen can be shown to prove the (again philosophically interesting) independence of the axiom of choice and the continuum hypothesis from the other axioms of set theory. Computable model theoryOther basic notions of model theoryMaps between structuresFix a language Failed to parse (Missing texvc executable; please see math/README to configure.): L , and let Failed to parse (Missing texvc executable; please see math/README to configure.): M and Failed to parse (Missing texvc executable; please see math/README to configure.): N be two Failed to parse (Missing texvc executable; please see math/README to configure.): L -structures. For symbols from the language, such as a constant Failed to parse (Missing texvc executable; please see math/README to configure.): c , let Failed to parse (Missing texvc executable; please see math/README to configure.): c^M be the interpretation of Failed to parse (Missing texvc executable; please see math/README to configure.): c in Failed to parse (Missing texvc executable; please see math/README to configure.): M and similarly for the other classes of symbols (functions and relations). A map Failed to parse (Missing texvc executable; please see math/README to configure.): h from the domain of Failed to parse (Missing texvc executable; please see math/README to configure.): M to the domain of Failed to parse (Missing texvc executable; please see math/README to configure.): N is a homomorphism if the following conditions hold:
, we have Failed to parse (Missing texvc executable; please see math/README to configure.): h(c^M) = c^N,
and Failed to parse (Missing texvc executable; please see math/README to configure.): a_1,\ldots,a_n \in M^n , we have Failed to parse (Missing texvc executable; please see math/README to configure.): h(f^M(a_1,\ldots,a_n))=f^N(h(a_1),\ldots,h(a_n)), and
and Failed to parse (Missing texvc executable; please see math/README to configure.): a_1,\ldots,a_n \in M^n , we have Failed to parse (Missing texvc executable; please see math/README to configure.): M \models R(a_1,\ldots,a_n) \Rightarrow N \models R(h(a_1),\ldots,h(a_n)).
is injective and the third condition is modified to read:
and Failed to parse (Missing texvc executable; please see math/README to configure.): a_1,\ldots,a_n \in M^n, we have Failed to parse (Missing texvc executable; please see math/README to configure.): M \models R(a_1,\ldots,a_n) \Leftrightarrow N \models R(h(a_1),\ldots,h(a_n)),
is an embedding (of Failed to parse (Missing texvc executable; please see math/README to configure.): M into Failed to parse (Missing texvc executable; please see math/README to configure.): N ). Equivalent definitions of homomorphism and embedding are: If for all atomic formulas Failed to parse (Missing texvc executable; please see math/README to configure.): \phi and sequences of elements from Failed to parse (Missing texvc executable; please see math/README to configure.): M , Failed to parse (Missing texvc executable; please see math/README to configure.): \bar{a} = (a_1,a_2,\ldots,a_n)
is the image of Failed to parse (Missing texvc executable; please see math/README to configure.): \bar{a}
under
Failed to parse (Missing texvc executable; please see math/README to configure.): h
is a homomorphism. If instead:
is an embedding. Formulae and definable setsWe said earlier that when we fix an Failed to parse (Missing texvc executable; please see math/README to configure.): L -structure, all the sentences and formulae are given a meaning. The sentences are either true or false, but the formulae have a different meaning. Formulae contain free variables, and these must be assigned a meaning before we can ascertain their veracity. An example in plain English is the following: 'it is red' (applied to the real world). Only when we substitute the name of a particular object can we ascertain whether this formula is true. The above formula divides the world into the set of things which are red, and the set of things which are not red. This is the function of formulae: for a given Failed to parse (Missing texvc executable; please see math/README to configure.): L -formula Failed to parse (Missing texvc executable; please see math/README to configure.): \phi(x_1,\ldots,x_n) , Failed to parse (Missing texvc executable; please see math/README to configure.): L -structure Failed to parse (Missing texvc executable; please see math/README to configure.): M , and elements Failed to parse (Missing texvc executable; please see math/README to configure.): m_1,\ldots,m_n of Failed to parse (Missing texvc executable; please see math/README to configure.): M , we write Failed to parse (Missing texvc executable; please see math/README to configure.): m_1,\ldots,m_n \models \phi(x_1,\ldots,x_n) if Failed to parse (Missing texvc executable; please see math/README to configure.): m_1,\ldots,m_n satisfy Failed to parse (Missing texvc executable; please see math/README to configure.): \phi(x_1,\ldots,x_n) . Then we call Failed to parse (Missing texvc executable; please see math/README to configure.): \{m_1,\ldots,m_n \in M^n:m_1,\ldots,m_n \models \phi(x_1,\ldots,x_n)\} the set defined by Failed to parse (Missing texvc executable; please see math/README to configure.): \phi in Failed to parse (Missing texvc executable; please see math/README to configure.): M . Thus for each formula in Failed to parse (Missing texvc executable; please see math/README to configure.): L , and each Failed to parse (Missing texvc executable; please see math/README to configure.): L -structure Failed to parse (Missing texvc executable; please see math/README to configure.): M we have the set defined by the formula. For any given Failed to parse (Missing texvc executable; please see math/README to configure.): M , the collection of definable sets is the important semantical notion corresponding to the collection of formulae. Elimination of quantifiers and model completenessA theory T is said to admit elimination of quantifiers if every formula is provably equivalent to a quantifier-free formula under T. The theory T is model complete if every formula is provably equivalent to an existential formula. These definitions concerning the syntactics of T can be shown to be equivalent to the following statement concerning the models of T (i.e. the semantics of T):
One can see from the definition that quantifier elimination is stronger than model completeness. This is because formulas in model complete theories are equivalent containing only existential quantifiers. Any formula in a theory that admits quantifier elimination is equivalent to a quantifier-free formula which can be viewed as a special kind of existential formula. In early model theory, quantifier elimination was used to demonstrate that various theories possess certain model-theoretic properties like decidability and completeness. A common technique was to show first that a theory admits elimination of quantifiers and thereafter prove decidability or completeness by considering only the quantifier-free formulas. This technique is used to show that Presburger arithmetic, i.e. the theory of the additive natural numbers, is decidable. The demonstration of the decidability of Presburger arithmetic already hints at the limitations of this technique. Theories could be decidable yet not admit quantifier elimination. Strictly speaking, the theory of the additive natural numbers did not admit quantifier elimination, but it was an expansion of the additive natural numbers that was shown to be decidable. Example: Nullstellensatz in ACF and DCF InterpretabilityGiven a mathematical structure, there are very often associated structures which can be constructed as a quotient of part of the original structure via an equivalence relation. An important example is a quotient group of a group. One might say that to understand the full structure one must understand these quotients. When the equivalence relation is definable, we can give the previous sentence a precise meaning. We say that these structures are interpretable. A key fact is that one can translate sentences from the language of the interpreted structures to the language of the original structure. Thus one can show that if a structure M interprets another whose theory is undecidable, then M itself is undecidable. Ultraproduct constructionsAn ultraproduct is a quotient of the direct product of a family of structures of the same signature. To use the ultraproduct construction, one chooses a suitable ultrafilter Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal U on the index set Failed to parse (Missing texvc executable; please see math/README to configure.): I of a family Failed to parse (Missing texvc executable; please see math/README to configure.): \{\mathbb A_i | i \in I\} of structures, all with the same language. Then one forms the product Failed to parse (Missing texvc executable; please see math/README to configure.): \Pi_{i\in I}\mathbb A_i of the given family, and factors out the equivalence relation Failed to parse (Missing texvc executable; please see math/README to configure.): \sim_{\mathcal U} that is defined on Failed to parse (Missing texvc executable; please see math/README to configure.): \mathbb A by the rule
of the family Failed to parse (Missing texvc executable; please see math/README to configure.): \{\mathbb A_i | i \in I\}
of structures is said to be almost all of them if Failed to parse (Missing texvc executable; please see math/README to configure.): X
is an element of the ultrafilter Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal U
. Thus, in the definition of the equivalence relation above, two (usually infinitely long, in most applications) vectors, Failed to parse (Missing texvc executable; please see math/README to configure.): \vec x and Failed to parse (Missing texvc executable; please see math/README to configure.): \vec y are identified iff their projections onto almost all of the axes Failed to parse (Missing texvc executable; please see math/README to configure.): \mathbb A_i are identical. The choice of which ultrafilter to use is dependent upon the application, and for many applications of model theory, the first and foremost criterion for choosing an ultrafilter is somehow related to cardinality. (For example, a frequently used type of ultrafilter is a uniform ultrafilter. An ultrafilter Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal U on a set Failed to parse (Missing texvc executable; please see math/README to configure.): I is uniform provided that every element of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal U is a set of the same cardinality as the set Failed to parse (Missing texvc executable; please see math/README to configure.): I .) However, there are some `trivial' cases that are essentially always avoided: non-proper ultrafilters (which many authors do not even call ultrafilters at all), and principal ultrafilters. (Here again, cardinality comes into play, because every (ultra)filter on a finite set is necessarily principal.) A most important tool in the application of ultraproducts is a theorem of Łoś, which states that for any sentence Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma
in the language appropriate for the given structures, Failed to parse (Missing texvc executable; please see math/README to configure.): \Pi_{i\in I}\mathbb A_i/\mathcal U
satisfies Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma
if and only if Failed to parse (Missing texvc executable; please see math/README to configure.): \sigma
holds in almost all of the given structures.
Some striking applications of ultraproducts include very elegant proofs of the compactness theorem and the completeness theorem, Keisler's ultrapower theorem, which gives an algebraic characterization of the semantic notion of elementary equivalence, and the Robinson-Zakon presentation of the use of superstructures and their monomorphisms to construct nonstandard models of analysis, leading to the growth of the area of nonstandard analysis, which was pioneered (as an application of the compactness theorem) by Abraham Robinson. Using the compactness and completeness theoremsGödel's completeness theorem (not to be confused with his incompleteness theorems) says that a theory has a model if and only if it is consistent, i.e. no contradiction is proved by the theory. This is the heart of model theory as it lets us answer questions about theories by looking at models and vice-versa. One should not confuse the completeness theorem with the notion of a complete theory. A complete theory is a theory that contains every sentence or its negation. Importantly, one can find a complete consistent theory extending any consistent theory. However, as shown by Gödel's incompleteness theorems only in relatively simple cases will it be possible to have a complete consistent theory that is also recursive, i.e. that can be described by a recursively enumerable set of axioms. In particular, the theory of natural numbers has no recursive complete and consistent theory. Non-recursive theories are of little practical use, since it is undecidable if a proposed axiom is indeed an axiom, making proof-checking practically impossible. The compactness theorem states that a set of sentences S is satisfiable if every finite subset of S is satisfiable. In the context of proof theory the analogous statement is trivial, since every proof can have only a finite number of antecedents used in the proof. In the context of model theory, however, this proof is somewhat more difficult. There are two well known proofs, one by Gödel (which goes via proofs) and one by Malcev (which is more direct and allows us to restrict the cardinality of the resulting model). Model theory is usually concerned with first-order logic, and many important results (such as the completeness and compactness theorems) fail in second-order logic or other alternatives. In first-order logic all infinite cardinals look the same to a language which is countable. This is expressed in the Löwenheim-Skolem theorems, which state that any countable theory with an infinite model Failed to parse (Missing texvc executable; please see math/README to configure.): \mathfrak{A}
has models of all infinite cardinalities (at least that of the language) which agree with Failed to parse (Missing texvc executable; please see math/README to configure.): \mathfrak{A}
on all sentences, i.e. they are 'elementarily equivalent'.
TypesFix an Failed to parse (Missing texvc executable; please see math/README to configure.): L -structure Failed to parse (Missing texvc executable; please see math/README to configure.): M , and a natural number Failed to parse (Missing texvc executable; please see math/README to configure.): n . The set of definable subsets of Failed to parse (Missing texvc executable; please see math/README to configure.): M^n over some parameters Failed to parse (Missing texvc executable; please see math/README to configure.): A is a Boolean algebra. By Stone's representation theorem for Boolean algebras there is a natural dual notion to this. One can consider this to be the topological space consisting of maximal consistent sets of formulae over Failed to parse (Missing texvc executable; please see math/README to configure.): A . We call this the space of (complete) Failed to parse (Missing texvc executable; please see math/README to configure.): n -types over Failed to parse (Missing texvc executable; please see math/README to configure.): A , and write Failed to parse (Missing texvc executable; please see math/README to configure.): S_n(A) . Now consider an element Failed to parse (Missing texvc executable; please see math/README to configure.): m \in M^n . Then the set of all formulae Failed to parse (Missing texvc executable; please see math/README to configure.): \phi with parameters in Failed to parse (Missing texvc executable; please see math/README to configure.): A in free variables Failed to parse (Missing texvc executable; please see math/README to configure.): x_1,\ldots,x_n so that Failed to parse (Missing texvc executable; please see math/README to configure.): M \models \phi(m) is consistent and maximal such. It is called the type of Failed to parse (Missing texvc executable; please see math/README to configure.): m over Failed to parse (Missing texvc executable; please see math/README to configure.): A . One can show that for any Failed to parse (Missing texvc executable; please see math/README to configure.): n -type Failed to parse (Missing texvc executable; please see math/README to configure.): p , there exists some elementary extension Failed to parse (Missing texvc executable; please see math/README to configure.): N of Failed to parse (Missing texvc executable; please see math/README to configure.): M and some Failed to parse (Missing texvc executable; please see math/README to configure.): a \in N^n so that Failed to parse (Missing texvc executable; please see math/README to configure.): p is the type of Failed to parse (Missing texvc executable; please see math/README to configure.): a over Failed to parse (Missing texvc executable; please see math/README to configure.): A . Many important properties in model theory can be expressed with types. Further many proofs go via constructing models with elements that contain elements with certain types and then using these elements. Illustrative Example: Suppose Failed to parse (Missing texvc executable; please see math/README to configure.): M is an algebraically closed field. The theory has quantifier elimination . This allows us to show that a type is determined exactly by the polynomial equations it contains. Thus the space of Failed to parse (Missing texvc executable; please see math/README to configure.): n -types over a subfield Failed to parse (Missing texvc executable; please see math/README to configure.): A is bijective with the set of prime ideals of the polynomial ring Failed to parse (Missing texvc executable; please see math/README to configure.): A[x_1,\ldots,x_n] . This is the same set as the spectrum of Failed to parse (Missing texvc executable; please see math/README to configure.): A[x_1,\ldots,x_n] . Note however that the topology considered on the type space is the constructible topology: a set of types is basic open iff it is of the form Failed to parse (Missing texvc executable; please see math/README to configure.): \{p: f(x)=0 \in p\}
or of the form Failed to parse (Missing texvc executable; please see math/README to configure.): \{p: f(x) \neq 0 \in p\}
. This is finer than the Zariski topology. CategoricityIf Failed to parse (Missing texvc executable; please see math/README to configure.): T is a first order theory in the language Failed to parse (Missing texvc executable; please see math/README to configure.): L and Failed to parse (Missing texvc executable; please see math/README to configure.): \kappa is a cardinal, then Failed to parse (Missing texvc executable; please see math/README to configure.): T is said to be Failed to parse (Missing texvc executable; please see math/README to configure.): \kappa -categorical iff any two models of Failed to parse (Missing texvc executable; please see math/README to configure.): T which are of cardinality Failed to parse (Missing texvc executable; please see math/README to configure.): \kappa are isomorphic. Categorical theories are from many points of view the most well behaved theories. The study of categoricity led on to the wider programme of stability. For more detail see Morley's categoricity theorem. Model completion, model companionsGiven first-order σ-theories T and T', T' is a model companion for T if i) T' is model complete ii) Every model of T has an extension that is a model of T' iii) Every model of T' has an extension that is a model of T If Failed to parse (Missing texvc executable; please see math/README to configure.): T'
is a model companion for Failed to parse (Missing texvc executable; please see math/README to configure.): T
and Failed to parse (Missing texvc executable; please see math/README to configure.): T' \cup Diag(\mathcal{M})
is complete
for any Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{M} \models T then Failed to parse (Missing texvc executable; please see math/README to configure.): T' is a model completion for Failed to parse (Missing texvc executable; please see math/README to configure.): T
Early history of model theoryModel theory as a subject exists since approximately the middle of the 20th century. However some earlier research, especially in mathematical logic, is often regarded as being of a model-theoretical nature in retrospect. The first significant result in what is now model theory was a special case of the downward Löwenheim-Skolem theorem, published by Leopold Löwenheim in 1915. The compactness theorem was implicit in work by Thoralf Skolem,[2] but it was first published in 1930, as a lemma in Kurt Gödel's proof of his completeness theorem. The Löwenheim-Skolems theorem and the compactness theorem received their respective general forms in 1936 and 1941 from Anatoly Maltsev. See alsoNotes
ReferencesCanonical textbooks
Other textbooks
Free online texts
bn:মডেল তত্ত্ব cs:Teorie modelů de:Modelltheorie es:Teoría de modelos fa:نظریه مدل fr:Théorie des modèles ko:모형 이론 it:Modello (logica matematica) nl:Modeltheorie pl:Teoria modeli pt:Teoria dos modelos ru:Теория моделей sv:Modellteori tr:Model Teorisi |
