{"history":[],"article":{"id":"5d442b40-6187-49ec-a39c-81c521259fb2","title":"Model theory","slug":"model-theory","content":":::summary\n:::\n\n# \nIn [mathematical logic](https://bliptext.com/articles/mathematical-logic), **model theory** is the study of the relationship between [formal theories](https://bliptext.com/articles/theory-mathematical-logic) (a collection of [sentences](https://bliptext.com/articles/sentence-mathematical-logic) in a [formal language](https://bliptext.com/articles/formal-language) expressing statements about a [mathematical structure](https://bliptext.com/articles/structure-mathematical-logic)), and their [models](https://bliptext.com/articles/structure-mathematical-logic) (those [structures](https://bliptext.com/articles/structure-mathematical-logic) in which the statements of the theory hold).\nThe aspects investigated include the number and size of models of a theory, the relationship of different models to each other, and their interaction with the formal language itself.\nIn particular, model theorists also investigate the sets that can be [defined](https://bliptext.com/articles/definable-set) in a model of a theory, and the relationship of such definable sets to each other.\nAs a separate discipline, model theory goes back to [Alfred Tarski](https://bliptext.com/articles/alfred-tarski), who first used the term \"Theory of Models\" in publication in 1954.\nSince the 1970s, the subject has been shaped decisively by [Saharon Shelah](https://bliptext.com/articles/saharon-shelah)'s [stability theory](https://bliptext.com/articles/stable-theory).\nCompared to other areas of mathematical logic such as [proof theory](https://bliptext.com/articles/proof-theory), model theory is often less concerned with formal rigour and closer in spirit to classical mathematics.\nThis has prompted the comment that \"if [proof theory](https://bliptext.com/articles/proof-theory) is about the sacred, then model theory is about the profane\".\nThe applications of model theory to [algebraic](https://bliptext.com/articles/algebraic-geometry) and [Diophantine geometry](https://bliptext.com/articles/diophantine-geometry) reflect this proximity to classical mathematics, as they often involve an integration of [algebraic](https://bliptext.com/articles/algebraic-geometry) and model-theoretic results and techniques.\nConsequently, proof theory is [syntactic](https://bliptext.com/articles/syntax-logic) in nature, in contrast to model theory, which is [semantic](https://bliptext.com/articles/formal-semantics-logic) in nature.\nThe most prominent scholarly organization in the field of model theory is the [Association for Symbolic Logic](https://bliptext.com/articles/association-for-symbolic-logic).\n\n# Overview\nThis page focuses on [finitary](https://bliptext.com/articles/finitary) [first order](https://bliptext.com/articles/first-order-logic) model theory of infinite structures.\nThe relative emphasis placed on the class of models of a theory as opposed to the class of definable sets within a model fluctuated in the history of the subject, and the two directions are summarised by the pithy characterisations from 1973 and 1997 respectively:\nwhere universal algebra stands for mathematical structures and logic for logical theories; and\nwhere logical formulas are to definable sets what equations are to varieties over a field.\nNonetheless, the interplay of classes of models and the sets definable in them has been crucial to the development of model theory throughout its history.\nFor instance, while stability was originally introduced to classify theories by their numbers of models in a given [cardinality](https://bliptext.com/articles/cardinality), stability theory proved crucial to understanding the geometry of definable sets.\n\n# Fundamental notions of first-order model theory\n\n## First-order logic\nA first-order formula is built out of [atomic formulas](https://bliptext.com/articles/atomic-formula) such as R(f(x,y),z) or y=x+1 by means of the [Boolean connectives](https://bliptext.com/articles/table-of-logic-symbols) and prefixing of quantifiers \\forall v or \\exists v. A sentence is a formula in which each occurrence of a variable is in the scope of a corresponding quantifier.\nExamples for formulas are \\varphi (or \\varphi(x) to indicate x is the unbound variable in \\varphi) and \\psi (or \\psi(x)), defined as follows:\n(Note that the equality symbol has a double meaning here.) It is intuitively clear how to translate such formulas into mathematical meaning.\nIn the semiring of natural numbers \\mathcal N, viewed as a structure with binary functions for addition and multiplication and constants for 0 and 1 of the natural numbers, for example, an element n satisfies the formula \\varphi if and only if n is a prime number.\nThe formula \\psi similarly defines [irreducibility](https://bliptext.com/articles/irreducible-element).\nTarski gave a rigorous definition, sometimes called [\"Tarski's definition of truth\"](https://bliptext.com/articles/t-schema), for the satisfaction relation \\models, so that one easily proves:\nA set T of sentences is called a (first-order) [theory](https://bliptext.com/articles/theory-mathematical-logic), which takes the sentences in the set as its axioms.\nA theory is satisfiable if it has a model, i.e. a structure (of the appropriate signature) which satisfies all the [sentence](https://bliptext.com/articles/sentence-mathematical-logic)s in the set T. A complete theory is a theory that contains every [sentence](https://bliptext.com/articles/sentence-mathematical-logic) or its negation.\nThe complete theory of all sentences satisfied by a structure is also called the theory of that structure.\nIt's a consequence of Gödel's [completeness theorem](https://bliptext.com/articles/completeness-theorem) (not to be confused with his in[completeness theorem](https://bliptext.com/articles/completeness-theorem)s) that a theory has a model if and only if it is [consistent](https://bliptext.com/articles/consistency), i.e. no contradiction is proved by the theory.\nTherefore, model theorists often use \"consistent\" as a synonym for \"satisfiable\".\n\n## Basic model-theoretic concepts\nA [signature](https://bliptext.com/articles/signature-logic) or [language](https://bliptext.com/articles/signature-logic) is a set of [non-logical symbols](https://bliptext.com/articles/non-logical-symbols) such that each symbol is either a constant symbol, or a function or relation symbol with a specified [arity](https://bliptext.com/articles/arity).\nNote that in some literature, constant symbols are considered as function symbols with zero arity, and hence are omitted.\nA [structure](https://bliptext.com/articles/structure-mathematical-logic) is a set M together with [interpretations](https://bliptext.com/articles/[interpretation](https://bliptext.com/articles/interpretation-model-theory)-logic) of each of the symbols of the signature as relations and functions on M (not to be confused with the formal notion of an \"[interpretation](https://bliptext.com/articles/interpretation-model-theory)\" of one [structure](https://bliptext.com/articles/structure-mathematical-logic) in another).\n**Example:** A common signature for ordered rings is, where 0 and 1 are 0-ary function symbols (also known as constant symbols), + and \\times are binary (= 2-ary) function symbols, - is a unary (= 1-ary) function symbol, and < is a binary relation symbol.\nThen, when these symbols are interpreted to correspond with their usual meaning on \\Q (so that e.g. + is a function from \\Q^2 to \\Q and < is a subset of \\Q^2), one obtains a structure.\nA structure \\mathcal{N} is said to model a set of first-order sentences T in the given language if each sentence in T is true in \\mathcal{N} with respect to the [interpretation](https://bliptext.com/articles/interpretation-logic) of the signature previously specified for \\mathcal{N}.\n(Again, not to be confused with the formal notion of an \"[interpretation](https://bliptext.com/articles/interpretation-model-theory)\" of one structure in another) A model of T is a structure that models T.\nA [substructure](https://bliptext.com/articles/substructure-mathematics) \\mathcal A of a σ-structure \\mathcal B 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.\nThis generalises the analogous concepts from algebra; for instance, a subgroup is a substructure in the signature with multiplication and inverse.\nA substructure is said to be elementary if for any first-order formula \\varphi and any elements a1, ..., an of \\mathcal A, In particular, if \\varphi is a sentence and \\mathcal A an elementary substructure of \\mathcal B, then if and only if.\nThus, an elementary substructure is a model of a theory exactly when the superstructure is a model.\n**Example:** While the field of algebraic numbers is an elementary substructure of the field of complex numbers \\mathbb{C}, the rational field \\mathbb{Q} is not, as we can express \"There is a square root of 2\" as a first-order sentence satisfied by \\mathbb{C} but not by \\mathbb{Q}.\nAn [embedding](https://bliptext.com/articles/embedding) of a σ-structure \\mathcal A into another σ-structure \\mathcal B is a map f: A → B between the domains which can be written as an isomorphism of \\mathcal A with a substructure of \\mathcal B. If it can be written as an isomorphism with an elementary substructure, it is called an elementary [embedding](https://bliptext.com/articles/embedding).\nEvery embedding is an [injective](https://bliptext.com/articles/injective) homomorphism, but the converse holds only if the signature contains no relation symbols, such as in groups or fields.\nA field or a vector space can be regarded as a (commutative) group by simply ignoring some of its structure.\nThe corresponding notion in model theory is that of a reduct of a structure to a subset of the original signature.\nThe opposite relation is called an expansion - e.g. the (additive) group of the [rational numbers](https://bliptext.com/articles/rational-numbers), regarded as a structure in the signature {+,0} can be expanded to a field with the signature {×,+,1,0} or to an ordered group with the signature {+,0,<}.\nSimilarly, if σ' is a signature that extends another signature σ, then a complete σ'-theory can be restricted to σ by intersecting the set of its sentences with the set of σ-formulas.\nConversely, a complete σ-theory can be regarded as a σ'-theory, and one can extend it (in more than one way) to a complete σ'-theory.\nThe terms reduct and expansion are sometimes applied to this relation as well.\n\n## Compactness and the Löwenheim-Skolem theorem\nThe [compactness theorem](https://bliptext.com/articles/compactness-theorem) states that a set of sentences S is satisfiable if every finite subset of S is satisfiable.\nThe analogous statement with consistent instead of satisfiable is trivial, since every proof can have only a finite number of antecedents used in the proof.\nThe completeness theorem allows us to transfer this to satisfiability.\nHowever, there are also several direct (semantic) proofs of the compactness theorem.\nAs a corollary (i.e., its contrapositive), the [compactness theorem](https://bliptext.com/articles/compactness-theorem) says that every unsatisfiable first-order theory has a finite unsatisfiable subset.\nThis theorem is of central importance in model theory, where the words \"by compactness\" are commonplace.\nAnother cornerstone of first-order model theory is the [Löwenheim-Skolem theorem](https://bliptext.com/articles/l-wenheim-skolem-theorem).\nAccording to the Löwenheim-Skolem Theorem, every infinite structure in a countable signature has a countable elementary substructure.\nConversely, for any infinite cardinal κ every infinite structure in a countable signature that is of cardinality less than κ can be elementarily embedded in another structure of cardinality κ (There is a straightforward generalisation to uncountable signatures).\nIn particular, the Löwenheim-Skolem Theorem implies that any theory in a countable signature with infinite models has a countable model as well as arbitrarily large models.\nIn a certain sense made precise by [Lindström's theorem](https://bliptext.com/articles/lindstr-m-s-theorem), first-order logic is the most expressive logic for which both the Löwenheim–Skolem theorem and the compactness theorem hold.\n\n# Definability\n\n## Definable sets\nIn model theory, [definable sets](https://bliptext.com/articles/definable-set) are important objects of study.\nFor instance, in \\mathbb N the formula\ndefines the subset of prime numbers, while the formula\ndefines the subset of even numbers.\nIn a similar way, formulas with n free variables define subsets of.\nFor example, in a field, the formula\ndefines the curve of all (x,y) such that y = x^2.\nBoth of the definitions mentioned here are parameter-free, that is, the defining formulas don't mention any fixed domain elements.\nHowever, one can also consider definitions with parameters from the model.\nFor instance, in \\mathbb{R}, the formula\nuses the parameter \\pi from \\mathbb{R} to define a curve.\n\n## Eliminating quantifiers\nIn general, definable sets without quantifiers are easy to describe, while definable sets involving possibly nested quantifiers can be much more complicated.\nThis makes [quantifier elimination](https://bliptext.com/articles/quantifier-elimination) a crucial tool for analysing definable sets:\nA 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. holds in all models of T.\nIf the theory of a structure has quantifier elimination, every set definable in a structure is definable by a quantifier-free formula over the same parameters as the original definition.\nFor example, the theory of algebraically closed fields in the signature σring = (×,+,−,0,1) has quantifier elimination.\nThis means that in an algebraically closed field, every formula is equivalent to a Boolean combination of equations between polynomials.\nIf a theory does not have quantifier elimination, one can add additional symbols to its signature so that it does.\nAxiomatisability and quantifier elimination results for specific theories, especially in algebra, were among the early landmark results of model theory.\nBut often instead of quantifier elimination a weaker property suffices:\nA theory T is called [model-complete](https://bliptext.com/articles/model-complete) if every substructure of a model of T which is itself a model of T is an elementary substructure.\nThere is a useful criterion for testing whether a substructure is an elementary substructure, called the [Tarski–Vaught test](https://bliptext.com/articles/tarski-vaught-test).\nIt 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:\nwhere ψ is quantifier free.\nA theory that is not model-complete may have a [model completion](https://bliptext.com/articles/model-completion), which is a related model-complete theory that is not, in general, an extension of the original theory.\nA more general notion is that of a [model companion](https://bliptext.com/articles/model-companion).\n\n## Minimality\nIn every structure, every finite subset is definable with parameters: Simply use the formula\nSince we can negate this formula, every cofinite subset (which includes all but finitely many elements of the domain) is also always definable.\nThis leads to the concept of a minimal structure.\nA structure \\mathcal{M} is called minimal if every subset definable with parameters from \\mathcal{M} is either finite or cofinite.\nThe corresponding concept at the level of theories is called strong minimality:\nA theory T is called [strongly minimal](https://bliptext.com/articles/strongly-minimal-theory) if every model of T is minimal.\nA structure is called strongly minimal if the theory of that structure is strongly minimal.\nEquivalently, a structure is strongly minimal if every elementary extension is minimal.\nSince the theory of algebraically closed fields has quantifier elimination, every definable subset of an algebraically closed field is definable by a quantifier-free formula in one variable.\nQuantifier-free formulas in one variable express Boolean combinations of polynomial equations in one variable, and since a nontrivial polynomial equation in one variable has only a finite number of solutions, the theory of algebraically closed fields is strongly minimal.\nOn the other hand, the field \\mathbb{R} of real numbers is not minimal: Consider, for instance, the definable set\nThis defines the subset of non-negative real numbers, which is neither finite nor cofinite.\nOne can in fact use \\varphi to define arbitrary intervals on the real number line.\nIt turns out that these suffice to represent every definable subset of \\mathbb{R}.\nThis generalisation of minimality has been very useful in the model theory of ordered structures.\nA [densely totally ordered](https://bliptext.com/articles/dense-linear-order) structure \\mathcal{M} in a signature including a symbol for the order relation is called [o-minimal](https://bliptext.com/articles/o-minimal) if every subset definable with parameters from \\mathcal{M} is a finite union of points and intervals.\n\n## Definable and interpretable structures\nParticularly important are those definable sets that are also substructures, i. e. contain all constants and are closed under function application.\nFor instance, one can study the definable subgroups of a certain group.\nHowever, there is no need to limit oneself to substructures in the same signature.\nSince formulas with n free variables define subsets of, n-ary relations can also be definable.\nFunctions are definable if the function graph is a definable relation, and constants are definable if there is a formula \\varphi(x) such that a is the only element of \\mathcal{M} such that \\varphi(a) is true.\nIn this way, one can study definable groups and fields in general structures, for instance, which has been important in geometric stability theory.\nOne can even go one step further, and move beyond immediate substructures.\nGiven 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.\nAn important example is a quotient group of a group.\nOne might say that to understand the full structure one must understand these quotients.\nWhen the equivalence relation is definable, we can give the previous sentence a precise meaning.\nWe say that these structures are interpretable.\nA key fact is that one can translate sentences from the language of the interpreted structures to the language of the original structure.\nThus one can show that if a structure \\mathcal{M} interprets another whose theory is undecidable, then \\mathcal{M} itself is undecidable.\n\n# Types\n\n## Basic notions\nFor a sequence of elements of a structure \\mathcal{M} and a subset A of \\mathcal{M}, one can consider the set of all first-order formulas with parameters in A that are satisfied by.\nThis is called the complete (n-)type realised by over A.\nIf there is an [automorphism](https://bliptext.com/articles/automorphism) of \\mathcal{M} that is constant on A and sends to respectively, then and realise the same complete type over A.\nThe real number line \\mathbb{R}, viewed as a structure with only the order relation {<}, will serve as a running example in this section.\nEvery element satisfies the same 1-type over the empty set.\nThis is clear since any two real numbers a and b are connected by the order automorphism that shifts all numbers by b-a.\nThe complete 2-type over the empty set realised by a pair of numbers a_1, a_2 depends on their order: either a_1 < a_2, a_1 = a_2 or a_2 < a_1.\nOver the subset of integers, the 1-type of a non-integer real number a depends on its value rounded down to the nearest integer.\nMore generally, whenever \\mathcal{M} is a structure and A a subset of \\mathcal{M}, a (partial) n-type over A is a set of formulas p with at most n free variables that are realised in an elementary extension \\mathcal{N} of \\mathcal{M}.\nIf p contains every such formula or its negation, then p is complete.\nThe set of complete n-types over A is often written as.\nIf A is the empty set, then the type space only depends on the theory T of \\mathcal{M}.\nThe notation S_n(T) is commonly used for the set of types over the empty set consistent with T. If there is a single formula \\varphi such that the theory of \\mathcal{M} implies for every formula \\psi in p, then p is called isolated.\nSince the real numbers \\mathbb{R} are [Archimedean](https://bliptext.com/articles/archimedean-field), there is no real number larger than every integer.\nHowever, a compactness argument shows that there is an elementary extension of the real number line in which there is an element larger than any integer.\nTherefore, the set of formulas is a 1-type over that is not realised in the real number line \\mathbb{R}.\nA subset of that can be expressed as exactly those elements of realising a certain type over A is called type-definable over A.\nFor an algebraic example, suppose M is an [algebraically closed field](https://bliptext.com/articles/algebraically-closed-field).\nThe theory has quantifier elimination.\nThis allows us to show that a type is determined exactly by the polynomial equations it contains.\nThus the set of complete n-types over a subfield A corresponds to the set of [prime ideals](https://bliptext.com/articles/prime-ideal) of the [polynomial ring](https://bliptext.com/articles/polynomial-ring), and the type-definable sets are exactly the affine varieties.\n\n## Structures and types\nWhile not every type is realised in every structure, every structure realises its isolated types.\nIf the only types over the empty set that are realised in a structure are the isolated types, then the structure is called atomic.\nOn the other hand, no structure realises every type over every parameter set; if one takes all of \\mathcal{M} as the parameter set, then every 1-type over \\mathcal{M} realised in \\mathcal{M} is isolated by a formula of the form a = x for an.\nHowever, any proper elementary extension of \\mathcal{M} contains an element that is not in \\mathcal{M}.\nTherefore, a weaker notion has been introduced that captures the idea of a structure realising all types it could be expected to realise.\nA structure is called saturated if it realises every type over a parameter set that is of smaller cardinality than \\mathcal{M} itself.\nWhile an automorphism that is constant on A will always preserve types over A, it is generally not true that any two sequences and that satisfy the same type over A can be mapped to each other by such an automorphism.\nA structure \\mathcal{M} in which this converse does hold for all A of smaller cardinality than \\mathcal{M} is called **homogeneous**.\nThe real number line is atomic in the language that contains only the order <, since all n-types over the empty set realised by in \\mathbb{R} are isolated by the order relations between the.\nIt is not saturated, however, since it does not realise any 1-type over the countable set \\mathbb{Z} that implies x to be larger than any integer.\nThe rational number line \\mathbb{Q} is saturated, in contrast, since \\mathbb{Q} is itself countable and therefore only has to realise types over finite subsets to be saturated.\n\n## Stone spaces\nThe set of definable subsets of over some parameters A is a [Boolean algebra](https://bliptext.com/articles/boolean-algebra-structure).\nBy [Stone's representation theorem for Boolean algebras](https://bliptext.com/articles/stone-s-representation-theorem-for-boolean-algebras) there is a natural dual [topological space](https://bliptext.com/articles/topological-space), which consists exactly of the complete n-types over A. The topology [generated](https://bliptext.com/articles/base-topology) by sets of the form for single formulas \\varphi.\nThis is called the Stone space of n-types over A.\nThis topology explains some of the terminology used in model theory: The compactness theorem says that the Stone space is a compact topological space, and a type p is isolated if and only if p is an isolated point in the Stone topology.\nWhile types in algebraically closed fields correspond to the spectrum of the polynomial ring, the topology on the type space is the [constructible topology](https://bliptext.com/articles/constructible-topology): a set of types is basic [open](https://bliptext.com/articles/open-set) iff it is of the form or of the form.\nThis is finer than the [Zariski topology](https://bliptext.com/articles/zariski-topology).\n\n# Constructing models\n\n## Realising and omitting types\nConstructing models that realise certain types and do not realise others is an important task in model theory.\nNot realising a type is referred to as omitting it, and is generally possible by the (Countable) Omitting types theorem:\nThis implies that if a theory in a countable signature has only countably many types over the empty set, then this theory has an atomic model.\nOn the other hand, there is always an elementary extension in which any set of types over a fixed parameter set is realised:\nHowever, since the parameter set is fixed and there is no mention here of the cardinality of \\mathcal{N}, this does not imply that every theory has a saturated model.\nIn fact, whether every theory has a saturated model is independent of the [Zermelo-Fraenkel axioms](https://bliptext.com/articles/zermelo-fraenkel-axioms) of set theory, and is true if the [generalised continuum hypothesis](https://bliptext.com/articles/generalised-continuum-hypothesis) holds.\n\n## Ultraproducts\n[Ultraproducts](https://bliptext.com/articles/ultraproduct) are used as a general technique for constructing models that realise certain types.\nAn ultraproduct is obtained from the [direct product](https://bliptext.com/articles/direct-product) of a set of structures over an index set I by identifying those tuples that agree on almost all entries, where almost all is made precise by an [ultrafilter](https://bliptext.com/articles/ultrafilter-set-theory) U on I. An ultraproduct of copies of the same structure is known as an ultrapower.\nThe key to using ultraproducts in model theory is Łoś's theorem:\nIn particular, any ultraproduct of models of a theory is itself a model of that theory, and thus if two models have isomorphic ultrapowers, they are elementarily equivalent.\nThe Keisler-Shelah theorem provides a converse:\nTherefore, ultraproducts provide a way to talk about elementary equivalence that avoids mentioning first-order theories at all.\nBasic theorems of model theory such as the compactness theorem have alternative proofs using ultraproducts, and they can be used to construct saturated elementary extensions if they exist.\n\n# Categoricity\nA theory was originally called categorical if it determines a structure up to isomorphism.\nIt turns out that this definition is not useful, due to serious restrictions in the expressivity of first-order logic.\nThe Löwenheim–Skolem theorem implies that if a theory T has an infinite model for some infinite [cardinal number](https://bliptext.com/articles/cardinal-number), then it has a model of size κ for any sufficiently large [cardinal number](https://bliptext.com/articles/cardinal-number) κ.\nSince two models of different sizes cannot possibly be isomorphic, only finite structures can be described by a categorical theory.\nHowever, the weaker notion of κ-categoricity for a cardinal κ has become a key concept in model theory.\nA theory T is called κ-categorical if any two models of T that are of cardinality κ are isomorphic.\nIt turns out that the question of κ-categoricity depends critically on whether κ is bigger than the cardinality of the language (i.e., where\nis the cardinality of the signature). For finite or countable signatures this means that there is a fundamental difference between ω-cardinality and κ-cardinality for uncountable κ.\n\n## ω-categoricity\n[ω-categorical theories](https://bliptext.com/articles/omega-categorical-theory) can be characterised by properties of their type space:\nThe theory of, which is also the theory of , is ω-categorical, as every n-type over the empty set is isolated by the pairwise order relation between the x_i.\nThis means that every countable [dense linear order](https://bliptext.com/articles/dense-linear-order) is order-isomorphic to the rational number line.\nOn the other hand, the theories of, and as fields are not \\omega-categorical.\nThis follows from the fact that in all those fields, any of the infinitely many natural numbers can be defined by a formula of the form.\n\\aleph_0-categorical theories and their countable models also have strong ties with [oligomorphic groups](https://bliptext.com/articles/oligomorphic-group):\nThe equivalent characterisations of this subsection, due independently to [Engeler](https://bliptext.com/articles/erwin-engeler), [Ryll-Nardzewski](https://bliptext.com/articles/czes-aw-ryll-nardzewski) and [Svenonius](https://bliptext.com/articles/lars-svenonius), are sometimes referred to as the [Ryll-Nardzewski](https://bliptext.com/articles/czes-aw-ryll-nardzewski) theorem.\nIn combinatorial signatures, a common source of ω-categorical theories are [Fraïssé limits](https://bliptext.com/articles/fra-ss-limit), which are obtained as the limit of amalgamating all possible configurations of a class of finite relational structures.\n\n## Uncountable categoricity\n[Michael Morley](https://bliptext.com/articles/michael-d-morley) showed in 1963 that there is only one notion of uncountable categoricity for theories in countable languages.\nMorley's proof revealed deep connections between uncountable categoricity and the internal structure of the models, which became the starting point of classification theory and stability theory.\nUncountably categorical theories are from many points of view the most well-behaved theories.\nIn particular, complete strongly minimal theories are uncountably categorical.\nThis shows that the theory of algebraically closed fields of a given characteristic is uncountably categorical, with the transcendence degree of the field determining its isomorphism type.\nA theory that is both ω-categorical and uncountably categorical is called totally categorical.\n\n# Stability theory\nA key factor in the structure of the class of models of a first-order theory is its place in the stability hierarchy.\nA theory is called stable if it is \\lambda-stable for some infinite cardinal \\lambda.\nTraditionally, theories that are \\aleph_0-stable are called \\omega-stable.\n\n## The stability hierarchy\nA fundamental result in stability theory is the [stability spectrum theorem](https://bliptext.com/articles/stability-spectrum), which implies that every complete theory T in a countable signature falls in one of the following classes:\nA theory of the first type is called unstable, a theory of the second type is called strictly stable and a theory of the third type is called superstable.\nFurthermore, if a theory is \\omega-stable, it is stable in every infinite cardinal, so \\omega-stability is stronger than superstability.\nMany construction in model theory are easier when restricted to stable theories; for instance, every model of a stable theory has a saturated elementary extension, regardless of whether the generalised continuum hypothesis is true.\nShelah's original motivation for studying stable theories was to decide how many models a countable theory has of any uncountable cardinality.\nIf a theory is uncountably categorical, then it is \\omega-stable.\nMore generally, the [Main gap theorem](https://bliptext.com/articles/spectrum-of-a-theory) implies that if there is an uncountable cardinal \\lambda such that a theory T has less than 2^{\\lambda} models of cardinality \\lambda, then T is superstable.\n\n## Geometric stability theory\nThe stability hierarchy is also crucial for analysing the geometry of definable sets within a model of a theory.\nIn \\omega-stable theories, [Morley rank](https://bliptext.com/articles/morley-rank) is an important dimension notion for definable sets S within a model.\nIt is defined by [transfinite induction](https://bliptext.com/articles/transfinite-induction):\nA theory T in which every definable set has well-defined Morley Rank is called totally transcendental; if T is countable, then T is totally transcendental if and only if T is \\omega-stable.\nMorley Rank can be extended to types by setting the Morley Rank of a type to be the minimum of the Morley ranks of the formulas in the type.\nThus, one can also speak of the Morley rank of an element a over a parameter set A, defined as the Morley rank of the type of a over A.\nThere are also analogues of Morley rank which are well-defined if and only if a theory is superstable ([U-rank](https://bliptext.com/articles/u-rank)) or merely stable (Shelah's \\infty-rank).\nThose dimension notions can be used to define notions of independence and of generic extensions.\nMore recently, stability has been decomposed into simplicity and \"not the independence property\" (NIP).\n[Simple theories](https://bliptext.com/articles/simple-theory) are those theories in which a well-behaved notion of independence can be defined, while [NIP theories](https://bliptext.com/articles/nip-model-theory) generalise o-minimal structures.\nThey are related to stability since a theory is stable if and only if it is NIP and simple, and various aspects of stability theory have been generalised to theories in one of these classes.\n\n# Non-elementary model theory\nModel-theoretic results have been generalised beyond elementary classes, that is, classes axiomatisable by a first-order theory.\nModel theory in [higher-order logics](https://bliptext.com/articles/higher-order-logic) or [infinitary logics](https://bliptext.com/articles/infinitary-logic) is hampered by the fact that [completeness](https://bliptext.com/articles/g-del-s-completeness-theorem) and [compactness](https://bliptext.com/articles/compactness-theorem) do not in general hold for these logics.\nThis is made concrete by [Lindstrom's theorem](https://bliptext.com/articles/lindstrom-s-theorem), stating roughly that first-order logic is essentially the strongest logic in which both the Löwenheim-Skolem theorems and compactness hold.\nHowever, model theoretic techniques have been developed extensively for these logics too.\nIt turns out, however, that much of the model theory of more expressive logical languages is independent of [Zermelo-Fraenkel set theory](https://bliptext.com/articles/zermelo-fraenkel-set-theory).\nMore recently, alongside the shift in focus to complete stable and categorical theories, there has been work on classes of models defined semantically rather than axiomatised by a logical theory.\nOne example is homogeneous model theory, which studies the class of substructures of arbitrarily large homogeneous models.\nFundamental results of stability theory and geometric stability theory generalise to this setting.\nAs a generalisation of strongly minimal theories, [quasiminimally excellent](https://bliptext.com/articles/quasiminimal-excellence) classes are those in which every definable set is either countable or co-countable.\nThey are key to the model theory of the [complex exponential function](https://bliptext.com/articles/complex-exponential-function).\nThe most general semantic framework in which stability is studied are [abstract elementary classes](https://bliptext.com/articles/abstract-elementary-class), which are defined by a strong substructure relation generalising that of an elementary substructure.\nEven though its definition is purely semantic, every abstract elementary class can be presented as the models of a first-order theory which omit certain types.\nGeneralising stability-theoretic notions to abstract elementary classes is an ongoing research program.\n\n# Selected applications\nAmong the early successes of model theory are Tarski's proofs of quantifier elimination for various algebraically interesting classes, such as the [real closed fields](https://bliptext.com/articles/real-closed-field), [Boolean algebras](https://bliptext.com/articles/boolean-algebra-structure) and [algebraically closed fields](https://bliptext.com/articles/algebraically-closed-field) of a given [characteristic](https://bliptext.com/articles/characteristic-algebra).\nQuantifier elimination allowed Tarski to show that the first-order theories of real-closed and algebraically closed fields as well as the first-order theory of Boolean algebras are decidable, classify the Boolean algebras up to elementary equivalence and show that the theories of real-closed fields and algebraically closed fields of a given characteristic are unique.\nFurthermore, quantifier elimination provided a precise description of definable relations on algebraically closed fields as [algebraic varieties](https://bliptext.com/articles/algebraic-varieties) and of the definable relations on real-closed fields as [semialgebraic sets](https://bliptext.com/articles/semialgebraic-sets)\nIn the 1960s, the introduction of the [ultraproduct](https://bliptext.com/articles/ultraproduct) construction led to new applications in algebra.\nThis includes [Ax's](https://bliptext.com/articles/james-ax) work on [pseudofinite fields](https://bliptext.com/articles/pseudofinite-field), proving that the theory of finite fields is decidable, and Ax and [Kochen's](https://bliptext.com/articles/simon-b-kochen) proof of as special case of Artin's conjecture on diophantine equations, the [Ax-Kochen theorem](https://bliptext.com/articles/ax-kochen-theorem).\nThe ultraproduct construction also led to [Abraham Robinson](https://bliptext.com/articles/abraham-robinson)'s development of [nonstandard analysis](https://bliptext.com/articles/nonstandard-analysis), which aims to provide a rigorous calculus of [infinitesimals](https://bliptext.com/articles/infinitesimals).\nMore recently, the connection between stability and the geometry of definable sets led to several applications from algebraic and diophantine geometry, including [Ehud Hrushovski](https://bliptext.com/articles/ehud-hrushovski)'s 1996 proof of the geometric [Mordell-Lang conjecture](https://bliptext.com/articles/mordell-lang-conjecture) in all characteristics In 2001, similar methods were used to prove a generalisation of the Manin-Mumford conjecture.\nIn 2011, [Jonathan Pila](https://bliptext.com/articles/jonathan-pila) applied techniques around [o-minimality](https://bliptext.com/articles/o-minimality) to prove the [André-Oort conjecture](https://bliptext.com/articles/andr-oort-conjecture) for products of Modular curves.\nIn a separate strand of inquiries that also grew around stable theories, Laskowski showed in 1992 that [NIP theories](https://bliptext.com/articles/nip-model-theory) describe exactly those definable classes that are [PAC-learnable](https://bliptext.com/articles/probably-approximately-correct-learning) in machine learning theory.\nThis has led to several interactions between these separate areas.\nIn 2018, the correspondence was extended as Hunter and Chase showed that stable theories correspond to [online learnable classes](https://bliptext.com/articles/online-machine-learning).\n\n# History\nModel theory as a subject has existed since approximately the middle of the 20th century, and the name was coined by [Alfred Tarski](https://bliptext.com/articles/alfred-tarski), a member of the [Lwów–Warsaw school](https://bliptext.com/articles/lw-w-warsaw-school), in 1954.\nHowever some earlier research, especially in [mathematical logic](https://bliptext.com/articles/mathematical-logic), is often regarded as being of a model-theoretical nature in retrospect.\nThe 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](https://bliptext.com/articles/leopold-l-wenheim) in 1915.\nThe [compactness theorem](https://bliptext.com/articles/compactness-theorem) was implicit in work by [Thoralf Skolem](https://bliptext.com/articles/thoralf-skolem), but it was first published in 1930, as a lemma in [Kurt Gödel](https://bliptext.com/articles/kurt-g-del)'s proof of his [completeness theorem](https://bliptext.com/articles/g-del-s-completeness-theorem).\nThe Löwenheim–Skolem theorem and the compactness theorem received their respective general forms in 1936 and 1941 from [Anatoly Maltsev](https://bliptext.com/articles/anatoly-maltsev).\nThe development of model theory as an independent discipline was brought on by Alfred Tarski during the [interbellum](https://bliptext.com/articles/interwar-period).\nTarski's work included [logical consequence](https://bliptext.com/articles/logical-consequence), [deductive systems](https://bliptext.com/articles/deductive-system), the algebra of logic, the theory of definability, and the [semantic definition of truth](https://bliptext.com/articles/semantic-theory-of-truth), among other topics.\nHis semantic methods culminated in the model theory he and a number of his [Berkeley](https://bliptext.com/articles/university-of-california-berkeley) students developed in the 1950s and '60s.\nIn the further history of the discipline, different strands began to emerge, and the focus of the subject shifted.\nIn the 1960s, techniques around ultraproducts became a popular tool in model theory.\nAt the same time, researchers such as [James Ax](https://bliptext.com/articles/james-ax) were investigating the first-order model theory of various algebraic classes, and others such as [H. Jerome Keisler](https://bliptext.com/articles/h-jerome-keisler) were extending the concepts and results of first-order model theory to other logical systems.\nThen, inspired by [Morley's problem](https://bliptext.com/articles/morley-s-problem), Shelah developed [stability theory](https://bliptext.com/articles/stable-theory).\nHis work around stability changed the complexion of model theory, giving rise to a whole new class of concepts.\nThis is known as the paradigm shift.\nOver the next decades, it became clear that the resulting stability hierarchy is closely connected to the geometry of sets that are definable in those models; this gave rise to the subdiscipline now known as geometric stability theory.\nAn example of an influential proof from geometric model theory is [Hrushovski](https://bliptext.com/articles/ehud-hrushovski)'s proof of the [Mordell–Lang conjecture](https://bliptext.com/articles/mordell-lang-conjecture) for function fields.\n\n# Connections to related branches of mathematical logic\n\n## Finite model theory\n[Finite model theory](https://bliptext.com/articles/finite-model-theory), which concentrates on finite structures, diverges significantly from the study of infinite structures in both the problems studied and the techniques used.\nIn particular, many central results of classical model theory that fail when restricted to finite structures.\nThis includes the [compactness theorem](https://bliptext.com/articles/compactness-theorem), [Gödel's completeness theorem](https://bliptext.com/articles/g-del-s-completeness-theorem), and the method of [ultraproducts](https://bliptext.com/articles/ultraproducts) for [first-order logic](https://bliptext.com/articles/first-order-logic).\nAt the interface of finite and infinite model theory are algorithmic or [computable model theory](https://bliptext.com/articles/computable-model-theory) and the study of [0-1 laws](https://bliptext.com/articles/zero-one-law-model-theory), where the infinite models of a generic theory of a class of structures provide information on the distribution of finite models.\nProminent application areas of FMT are [descriptive complexity theory](https://bliptext.com/articles/descriptive-complexity-theory), [database theory](https://bliptext.com/articles/database-theory) and [formal language theory](https://bliptext.com/articles/formal-language-theory).\n\n## Set theory\nAny [set theory](https://bliptext.com/articles/formal-system) (which is expressed in a [countable](https://bliptext.com/articles/countable) language), if it is consistent, has a [countable](https://bliptext.com/articles/countable) model; this is known as [Skolem's paradox](https://bliptext.com/articles/skolem-s-paradox), since there are sentences in [set theory](https://bliptext.com/articles/formal-system) which postulate the existence of un[countable](https://bliptext.com/articles/countable) sets and yet these sentences are true in our [countable](https://bliptext.com/articles/countable) model.\nParticularly the proof of the independence of the [continuum hypothesis](https://bliptext.com/articles/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.\nThe model-theoretic viewpoint has been useful in [set theory](https://bliptext.com/articles/set-theory); for example in [Kurt Gödel](https://bliptext.com/articles/kurt-g-del)'s work on the constructible universe, which, along with the method of [forcing](https://bliptext.com/articles/forcing-mathematics) developed by [Paul Cohen](https://bliptext.com/articles/paul-cohen-mathematician) can be shown to prove the (again philosophically interesting) [independence](https://bliptext.com/articles/independence-mathematical-logic) of the [axiom of choice](https://bliptext.com/articles/axiom-of-choice) and the continuum hypothesis from the other axioms of [set theory](https://bliptext.com/articles/set-theory).\nIn the other direction, model theory is itself formalised within Zermelo-Fraenkel set theory.\nFor instance, the development of the fundamentals of model theory (such as the compactness theorem) rely on the axiom of choice, and is in fact equivalent over Zermelo-Fraenkel set theory without choice to the Boolean prime ideal theorem.\nOther results in model theory depend on set-theoretic axioms beyond the standard ZFC framework.\nFor example, if the Continuum Hypothesis holds then every countable model has an ultrapower which is saturated (in its own cardinality).\nSimilarly, if the Generalized Continuum Hypothesis holds then every model has a saturated elementary extension.\nNeither of these results are provable in ZFC alone.\nFinally, some questions arising from model theory (such as compactness for infinitary logics) have been shown to be equivalent to large cardinal axioms.\n\n# Canonical textbooks\n\n## Other textbooks\n\n## Free online texts","current_revision":null,"created_by":"kACnuQmH5k9Nr5VNVEpVeg7XpvUmMctD","created_at":"2025-01-25T16:31:37.177Z","updated_at":"2025-01-25T16:31:37.177Z","search_vector":"'model':1 'theori':2","search_content":" \n \n\n# \nIn [mathematical logic](https://bliptext.com/articles/mathematical-logic), **model theory** is the study of the relationship between [formal theories](https://bliptext.com/articles/theory-mathematical-logic) (a collection of [sentences](https://bliptext.com/articles/sentence-mathematical-logic) in a [formal language](https://bliptext.com/articles/formal-language) expressing statements about a [mathematical structure](https://bliptext.com/articles/structure-mathematical-logic)), and their [models](https://bliptext.com/articles/structure-mathematical-logic) (those [structures](https://bliptext.com/articles/structure-mathematical-logic) in which the statements of the theory hold).\nThe aspects investigated include the number and size of models of a theory, the relationship of different models to each other, and their interaction with the formal language itself.\nIn particular, model theorists also investigate the sets that can be [defined](https://bliptext.com/articles/definable-set) in a model of a theory, and the relationship of such definable sets to each other.\nAs a separate discipline, model theory goes back to [Alfred Tarski](https://bliptext.com/articles/alfred-tarski), who first used the term \"Theory of Models\" in publication in 1954.\nSince the 1970s, the subject has been shaped decisively by [Saharon Shelah](https://bliptext.com/articles/saharon-shelah)'s [stability theory](https://bliptext.com/articles/stable-theory).\nCompared to other areas of mathematical logic such as [proof theory](https://bliptext.com/articles/proof-theory), model theory is often less concerned with formal rigour and closer in spirit to classical mathematics.\nThis has prompted the comment that \"if [proof theory](https://bliptext.com/articles/proof-theory) is about the sacred, then model theory is about the profane\".\nThe applications of model theory to [algebraic](https://bliptext.com/articles/algebraic-geometry) and [Diophantine geometry](https://bliptext.com/articles/diophantine-geometry) reflect this proximity to classical mathematics, as they often involve an integration of [algebraic](https://bliptext.com/articles/algebraic-geometry) and model-theoretic results and techniques.\nConsequently, proof theory is [syntactic](https://bliptext.com/articles/syntax-logic) in nature, in contrast to model theory, which is [semantic](https://bliptext.com/articles/formal-semantics-logic) in nature.\nThe most prominent scholarly organization in the field of model theory is the [Association for Symbolic Logic](https://bliptext.com/articles/association-for-symbolic-logic).\n\n# Overview\nThis page focuses on [finitary](https://bliptext.com/articles/finitary) [first order](https://bliptext.com/articles/first-order-logic) model theory of infinite structures.\nThe relative emphasis placed on the class of models of a theory as opposed to the class of definable sets within a model fluctuated in the history of the subject, and the two directions are summarised by the pithy characterisations from 1973 and 1997 respectively:\nwhere universal algebra stands for mathematical structures and logic for logical theories; and\nwhere logical formulas are to definable sets what equations are to varieties over a field.\nNonetheless, the interplay of classes of models and the sets definable in them has been crucial to the development of model theory throughout its history.\nFor instance, while stability was originally introduced to classify theories by their numbers of models in a given [cardinality](https://bliptext.com/articles/cardinality), stability theory proved crucial to understanding the geometry of definable sets.\n\n# Fundamental notions of first-order model theory\n\n## First-order logic\nA first-order formula is built out of [atomic formulas](https://bliptext.com/articles/atomic-formula) such as R(f(x,y),z) or y=x+1 by means of the [Boolean connectives](https://bliptext.com/articles/table-of-logic-symbols) and prefixing of quantifiers \\forall v or \\exists v. A sentence is a formula in which each occurrence of a variable is in the scope of a corresponding quantifier.\nExamples for formulas are \\varphi (or \\varphi(x) to indicate x is the unbound variable in \\varphi) and \\psi (or \\psi(x)), defined as follows:\n(Note that the equality symbol has a double meaning here.) It is intuitively clear how to translate such formulas into mathematical meaning.\nIn the semiring of natural numbers \\mathcal N, viewed as a structure with binary functions for addition and multiplication and constants for 0 and 1 of the natural numbers, for example, an element n satisfies the formula \\varphi if and only if n is a prime number.\nThe formula \\psi similarly defines [irreducibility](https://bliptext.com/articles/irreducible-element).\nTarski gave a rigorous definition, sometimes called [\"Tarski's definition of truth\"](https://bliptext.com/articles/t-schema), for the satisfaction relation \\models, so that one easily proves:\nA set T of sentences is called a (first-order) [theory](https://bliptext.com/articles/theory-mathematical-logic), which takes the sentences in the set as its axioms.\nA theory is satisfiable if it has a model, i.e. a structure (of the appropriate signature) which satisfies all the [sentence](https://bliptext.com/articles/sentence-mathematical-logic)s in the set T. A complete theory is a theory that contains every [sentence](https://bliptext.com/articles/sentence-mathematical-logic) or its negation.\nThe complete theory of all sentences satisfied by a structure is also called the theory of that structure.\nIt's a consequence of Gödel's [completeness theorem](https://bliptext.com/articles/completeness-theorem) (not to be confused with his in[completeness theorem](https://bliptext.com/articles/completeness-theorem)s) that a theory has a model if and only if it is [consistent](https://bliptext.com/articles/consistency), i.e. no contradiction is proved by the theory.\nTherefore, model theorists often use \"consistent\" as a synonym for \"satisfiable\".\n\n## Basic model-theoretic concepts\nA [signature](https://bliptext.com/articles/signature-logic) or [language](https://bliptext.com/articles/signature-logic) is a set of [non-logical symbols](https://bliptext.com/articles/non-logical-symbols) such that each symbol is either a constant symbol, or a function or relation symbol with a specified [arity](https://bliptext.com/articles/arity).\nNote that in some literature, constant symbols are considered as function symbols with zero arity, and hence are omitted.\nA [structure](https://bliptext.com/articles/structure-mathematical-logic) is a set M together with [[interpretation](https://bliptext.com/articles/interpretation-model-theory)s](https://bliptext.com/articles/[interpretation](https://bliptext.com/articles/interpretation-model-theory)-logic) of each of the symbols of the signature as relations and functions on M (not to be confused with the formal notion of an \"[interpretation](https://bliptext.com/articles/interpretation-model-theory)\" of one [structure](https://bliptext.com/articles/structure-mathematical-logic) in another).\n**Example:** A common signature for ordered rings is, where 0 and 1 are 0-ary function symbols (also known as constant symbols), + and \\times are binary (= 2-ary) function symbols, - is a unary (= 1-ary) function symbol, and < is a binary relation symbol.\nThen, when these symbols are interpreted to correspond with their usual meaning on \\Q (so that e.g. + is a function from \\Q^2 to \\Q and < is a subset of \\Q^2), one obtains a structure.\nA structure \\mathcal{N} is said to model a set of first-order sentences T in the given language if each sentence in T is true in \\mathcal{N} with respect to the [interpretation](https://bliptext.com/articles/interpretation-logic) of the signature previously specified for \\mathcal{N}.\n(Again, not to be confused with the formal notion of an \"[interpretation](https://bliptext.com/articles/interpretation-model-theory)\" of one structure in another) A model of T is a structure that models T.\nA [substructure](https://bliptext.com/articles/substructure-mathematics) \\mathcal A of a σ-structure \\mathcal B 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.\nThis generalises the analogous concepts from algebra; for instance, a subgroup is a substructure in the signature with multiplication and inverse.\nA substructure is said to be elementary if for any first-order formula \\varphi and any elements a1, ..., an of \\mathcal A, In particular, if \\varphi is a sentence and \\mathcal A an elementary substructure of \\mathcal B, then if and only if.\nThus, an elementary substructure is a model of a theory exactly when the superstructure is a model.\n**Example:** While the field of algebraic numbers is an elementary substructure of the field of complex numbers \\mathbb{C}, the rational field \\mathbb{Q} is not, as we can express \"There is a square root of 2\" as a first-order sentence satisfied by \\mathbb{C} but not by \\mathbb{Q}.\nAn [embedding](https://bliptext.com/articles/embedding) of a σ-structure \\mathcal A into another σ-structure \\mathcal B is a map f: A → B between the domains which can be written as an isomorphism of \\mathcal A with a substructure of \\mathcal B. If it can be written as an isomorphism with an elementary substructure, it is called an elementary [embedding](https://bliptext.com/articles/embedding).\nEvery embedding is an [injective](https://bliptext.com/articles/injective) homomorphism, but the converse holds only if the signature contains no relation symbols, such as in groups or fields.\nA field or a vector space can be regarded as a (commutative) group by simply ignoring some of its structure.\nThe corresponding notion in model theory is that of a reduct of a structure to a subset of the original signature.\nThe opposite relation is called an expansion - e.g. the (additive) group of the [rational numbers](https://bliptext.com/articles/rational-numbers), regarded as a structure in the signature {+,0} can be expanded to a field with the signature {×,+,1,0} or to an ordered group with the signature {+,0,<}.\nSimilarly, if σ' is a signature that extends another signature σ, then a complete σ'-theory can be restricted to σ by intersecting the set of its sentences with the set of σ-formulas.\nConversely, a complete σ-theory can be regarded as a σ'-theory, and one can extend it (in more than one way) to a complete σ'-theory.\nThe terms reduct and expansion are sometimes applied to this relation as well.\n\n## Compactness and the Löwenheim-Skolem theorem\nThe [compactness theorem](https://bliptext.com/articles/compactness-theorem) states that a set of sentences S is satisfiable if every finite subset of S is satisfiable.\nThe analogous statement with consistent instead of satisfiable is trivial, since every proof can have only a finite number of antecedents used in the proof.\nThe completeness theorem allows us to transfer this to satisfiability.\nHowever, there are also several direct (semantic) proofs of the compactness theorem.\nAs a corollary (i.e., its contrapositive), the [compactness theorem](https://bliptext.com/articles/compactness-theorem) says that every unsatisfiable first-order theory has a finite unsatisfiable subset.\nThis theorem is of central importance in model theory, where the words \"by compactness\" are commonplace.\nAnother cornerstone of first-order model theory is the [Löwenheim-Skolem theorem](https://bliptext.com/articles/l-wenheim-skolem-theorem).\nAccording to the Löwenheim-Skolem Theorem, every infinite structure in a countable signature has a countable elementary substructure.\nConversely, for any infinite cardinal κ every infinite structure in a countable signature that is of cardinality less than κ can be elementarily embedded in another structure of cardinality κ (There is a straightforward generalisation to uncountable signatures).\nIn particular, the Löwenheim-Skolem Theorem implies that any theory in a countable signature with infinite models has a countable model as well as arbitrarily large models.\nIn a certain sense made precise by [Lindström's theorem](https://bliptext.com/articles/lindstr-m-s-theorem), first-order logic is the most expressive logic for which both the Löwenheim–Skolem theorem and the compactness theorem hold.\n\n# Definability\n\n## Definable sets\nIn model theory, [definable sets](https://bliptext.com/articles/definable-set) are important objects of study.\nFor instance, in \\mathbb N the formula\ndefines the subset of prime numbers, while the formula\ndefines the subset of even numbers.\nIn a similar way, formulas with n free variables define subsets of.\nFor example, in a field, the formula\ndefines the curve of all (x,y) such that y = x^2.\nBoth of the definitions mentioned here are parameter-free, that is, the defining formulas don't mention any fixed domain elements.\nHowever, one can also consider definitions with parameters from the model.\nFor instance, in \\mathbb{R}, the formula\nuses the parameter \\pi from \\mathbb{R} to define a curve.\n\n## Eliminating quantifiers\nIn general, definable sets without quantifiers are easy to describe, while definable sets involving possibly nested quantifiers can be much more complicated.\nThis makes [quantifier elimination](https://bliptext.com/articles/quantifier-elimination) a crucial tool for analysing definable sets:\nA 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. holds in all models of T.\nIf the theory of a structure has quantifier elimination, every set definable in a structure is definable by a quantifier-free formula over the same parameters as the original definition.\nFor example, the theory of algebraically closed fields in the signature σring = (×,+,−,0,1) has quantifier elimination.\nThis means that in an algebraically closed field, every formula is equivalent to a Boolean combination of equations between polynomials.\nIf a theory does not have quantifier elimination, one can add additional symbols to its signature so that it does.\nAxiomatisability and quantifier elimination results for specific theories, especially in algebra, were among the early landmark results of model theory.\nBut often instead of quantifier elimination a weaker property suffices:\nA theory T is called [model-complete](https://bliptext.com/articles/model-complete) if every substructure of a model of T which is itself a model of T is an elementary substructure.\nThere is a useful criterion for testing whether a substructure is an elementary substructure, called the [Tarski–Vaught test](https://bliptext.com/articles/tarski-vaught-test).\nIt 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:\nwhere ψ is quantifier free.\nA theory that is not model-complete may have a [model completion](https://bliptext.com/articles/model-completion), which is a related model-complete theory that is not, in general, an extension of the original theory.\nA more general notion is that of a [model companion](https://bliptext.com/articles/model-companion).\n\n## Minimality\nIn every structure, every finite subset is definable with parameters: Simply use the formula\nSince we can negate this formula, every cofinite subset (which includes all but finitely many elements of the domain) is also always definable.\nThis leads to the concept of a minimal structure.\nA structure \\mathcal{M} is called minimal if every subset definable with parameters from \\mathcal{M} is either finite or cofinite.\nThe corresponding concept at the level of theories is called strong minimality:\nA theory T is called [strongly minimal](https://bliptext.com/articles/strongly-minimal-theory) if every model of T is minimal.\nA structure is called strongly minimal if the theory of that structure is strongly minimal.\nEquivalently, a structure is strongly minimal if every elementary extension is minimal.\nSince the theory of algebraically closed fields has quantifier elimination, every definable subset of an algebraically closed field is definable by a quantifier-free formula in one variable.\nQuantifier-free formulas in one variable express Boolean combinations of polynomial equations in one variable, and since a nontrivial polynomial equation in one variable has only a finite number of solutions, the theory of algebraically closed fields is strongly minimal.\nOn the other hand, the field \\mathbb{R} of real numbers is not minimal: Consider, for instance, the definable set\nThis defines the subset of non-negative real numbers, which is neither finite nor cofinite.\nOne can in fact use \\varphi to define arbitrary intervals on the real number line.\nIt turns out that these suffice to represent every definable subset of \\mathbb{R}.\nThis generalisation of minimality has been very useful in the model theory of ordered structures.\nA [densely totally ordered](https://bliptext.com/articles/dense-linear-order) structure \\mathcal{M} in a signature including a symbol for the order relation is called [o-minimal](https://bliptext.com/articles/o-minimal) if every subset definable with parameters from \\mathcal{M} is a finite union of points and intervals.\n\n## Definable and interpretable structures\nParticularly important are those definable sets that are also substructures, i. e. contain all constants and are closed under function application.\nFor instance, one can study the definable subgroups of a certain group.\nHowever, there is no need to limit oneself to substructures in the same signature.\nSince formulas with n free variables define subsets of, n-ary relations can also be definable.\nFunctions are definable if the function graph is a definable relation, and constants are definable if there is a formula \\varphi(x) such that a is the only element of \\mathcal{M} such that \\varphi(a) is true.\nIn this way, one can study definable groups and fields in general structures, for instance, which has been important in geometric stability theory.\nOne can even go one step further, and move beyond immediate substructures.\nGiven 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.\nAn important example is a quotient group of a group.\nOne might say that to understand the full structure one must understand these quotients.\nWhen the equivalence relation is definable, we can give the previous sentence a precise meaning.\nWe say that these structures are interpretable.\nA key fact is that one can translate sentences from the language of the interpreted structures to the language of the original structure.\nThus one can show that if a structure \\mathcal{M} interprets another whose theory is undecidable, then \\mathcal{M} itself is undecidable.\n\n# Types\n\n## Basic notions\nFor a sequence of elements of a structure \\mathcal{M} and a subset A of \\mathcal{M}, one can consider the set of all first-order formulas with parameters in A that are satisfied by.\nThis is called the complete (n-)type realised by over A.\nIf there is an [automorphism](https://bliptext.com/articles/automorphism) of \\mathcal{M} that is constant on A and sends to respectively, then and realise the same complete type over A.\nThe real number line \\mathbb{R}, viewed as a structure with only the order relation {<}, will serve as a running example in this section.\nEvery element satisfies the same 1-type over the empty set.\nThis is clear since any two real numbers a and b are connected by the order automorphism that shifts all numbers by b-a.\nThe complete 2-type over the empty set realised by a pair of numbers a_1, a_2 depends on their order: either a_1 < a_2, a_1 = a_2 or a_2 < a_1.\nOver the subset of integers, the 1-type of a non-integer real number a depends on its value rounded down to the nearest integer.\nMore generally, whenever \\mathcal{M} is a structure and A a subset of \\mathcal{M}, a (partial) n-type over A is a set of formulas p with at most n free variables that are realised in an elementary extension \\mathcal{N} of \\mathcal{M}.\nIf p contains every such formula or its negation, then p is complete.\nThe set of complete n-types over A is often written as.\nIf A is the empty set, then the type space only depends on the theory T of \\mathcal{M}.\nThe notation S_n(T) is commonly used for the set of types over the empty set consistent with T. If there is a single formula \\varphi such that the theory of \\mathcal{M} implies for every formula \\psi in p, then p is called isolated.\nSince the real numbers \\mathbb{R} are [Archimedean](https://bliptext.com/articles/archimedean-field), there is no real number larger than every integer.\nHowever, a compactness argument shows that there is an elementary extension of the real number line in which there is an element larger than any integer.\nTherefore, the set of formulas is a 1-type over that is not realised in the real number line \\mathbb{R}.\nA subset of that can be expressed as exactly those elements of realising a certain type over A is called type-definable over A.\nFor an algebraic example, suppose M is an [algebraically closed field](https://bliptext.com/articles/algebraically-closed-field).\nThe theory has quantifier elimination.\nThis allows us to show that a type is determined exactly by the polynomial equations it contains.\nThus the set of complete n-types over a subfield A corresponds to the set of [prime ideals](https://bliptext.com/articles/prime-ideal) of the [polynomial ring](https://bliptext.com/articles/polynomial-ring), and the type-definable sets are exactly the affine varieties.\n\n## Structures and types\nWhile not every type is realised in every structure, every structure realises its isolated types.\nIf the only types over the empty set that are realised in a structure are the isolated types, then the structure is called atomic.\nOn the other hand, no structure realises every type over every parameter set; if one takes all of \\mathcal{M} as the parameter set, then every 1-type over \\mathcal{M} realised in \\mathcal{M} is isolated by a formula of the form a = x for an.\nHowever, any proper elementary extension of \\mathcal{M} contains an element that is not in \\mathcal{M}.\nTherefore, a weaker notion has been introduced that captures the idea of a structure realising all types it could be expected to realise.\nA structure is called saturated if it realises every type over a parameter set that is of smaller cardinality than \\mathcal{M} itself.\nWhile an automorphism that is constant on A will always preserve types over A, it is generally not true that any two sequences and that satisfy the same type over A can be mapped to each other by such an automorphism.\nA structure \\mathcal{M} in which this converse does hold for all A of smaller cardinality than \\mathcal{M} is called **homogeneous**.\nThe real number line is atomic in the language that contains only the order <, since all n-types over the empty set realised by in \\mathbb{R} are isolated by the order relations between the.\nIt is not saturated, however, since it does not realise any 1-type over the countable set \\mathbb{Z} that implies x to be larger than any integer.\nThe rational number line \\mathbb{Q} is saturated, in contrast, since \\mathbb{Q} is itself countable and therefore only has to realise types over finite subsets to be saturated.\n\n## Stone spaces\nThe set of definable subsets of over some parameters A is a [Boolean algebra](https://bliptext.com/articles/boolean-algebra-structure).\nBy [Stone's representation theorem for Boolean algebras](https://bliptext.com/articles/stone-s-representation-theorem-for-boolean-algebras) there is a natural dual [topological space](https://bliptext.com/articles/topological-space), which consists exactly of the complete n-types over A. The topology [generated](https://bliptext.com/articles/base-topology) by sets of the form for single formulas \\varphi.\nThis is called the Stone space of n-types over A.\nThis topology explains some of the terminology used in model theory: The compactness theorem says that the Stone space is a compact topological space, and a type p is isolated if and only if p is an isolated point in the Stone topology.\nWhile types in algebraically closed fields correspond to the spectrum of the polynomial ring, the topology on the type space is the [constructible topology](https://bliptext.com/articles/constructible-topology): a set of types is basic [open](https://bliptext.com/articles/open-set) iff it is of the form or of the form.\nThis is finer than the [Zariski topology](https://bliptext.com/articles/zariski-topology).\n\n# Constructing models\n\n## Realising and omitting types\nConstructing models that realise certain types and do not realise others is an important task in model theory.\nNot realising a type is referred to as omitting it, and is generally possible by the (Countable) Omitting types theorem:\nThis implies that if a theory in a countable signature has only countably many types over the empty set, then this theory has an atomic model.\nOn the other hand, there is always an elementary extension in which any set of types over a fixed parameter set is realised:\nHowever, since the parameter set is fixed and there is no mention here of the cardinality of \\mathcal{N}, this does not imply that every theory has a saturated model.\nIn fact, whether every theory has a saturated model is independent of the [Zermelo-Fraenkel axioms](https://bliptext.com/articles/zermelo-fraenkel-axioms) of set theory, and is true if the [generalised continuum hypothesis](https://bliptext.com/articles/generalised-continuum-hypothesis) holds.\n\n## Ultraproducts\n[Ultraproducts](https://bliptext.com/articles/ultraproduct) are used as a general technique for constructing models that realise certain types.\nAn ultraproduct is obtained from the [direct product](https://bliptext.com/articles/direct-product) of a set of structures over an index set I by identifying those tuples that agree on almost all entries, where almost all is made precise by an [ultrafilter](https://bliptext.com/articles/ultrafilter-set-theory) U on I. An ultraproduct of copies of the same structure is known as an ultrapower.\nThe key to using ultraproducts in model theory is Łoś's theorem:\nIn particular, any ultraproduct of models of a theory is itself a model of that theory, and thus if two models have isomorphic ultrapowers, they are elementarily equivalent.\nThe Keisler-Shelah theorem provides a converse:\nTherefore, ultraproducts provide a way to talk about elementary equivalence that avoids mentioning first-order theories at all.\nBasic theorems of model theory such as the compactness theorem have alternative proofs using ultraproducts, and they can be used to construct saturated elementary extensions if they exist.\n\n# Categoricity\nA theory was originally called categorical if it determines a structure up to isomorphism.\nIt turns out that this definition is not useful, due to serious restrictions in the expressivity of first-order logic.\nThe Löwenheim–Skolem theorem implies that if a theory T has an infinite model for some infinite [[cardinal number](https://bliptext.com/articles/cardinal-number)](https://bliptext.com/articles/cardinal-number), then it has a model of size κ for any sufficiently large [[cardinal number](https://bliptext.com/articles/cardinal-number)](https://bliptext.com/articles/cardinal-number) κ.\nSince two models of different sizes cannot possibly be isomorphic, only finite structures can be described by a categorical theory.\nHowever, the weaker notion of κ-categoricity for a cardinal κ has become a key concept in model theory.\nA theory T is called κ-categorical if any two models of T that are of cardinality κ are isomorphic.\nIt turns out that the question of κ-categoricity depends critically on whether κ is bigger than the cardinality of the language (i.e., where\nis the cardinality of the signature). For finite or countable signatures this means that there is a fundamental difference between ω-cardinality and κ-cardinality for uncountable κ.\n\n## ω-categoricity\n[ω-categorical theories](https://bliptext.com/articles/omega-categorical-theory) can be characterised by properties of their type space:\nThe theory of, which is also the theory of , is ω-categorical, as every n-type over the empty set is isolated by the pairwise order relation between the x_i.\nThis means that every countable [dense linear order](https://bliptext.com/articles/dense-linear-order) is order-isomorphic to the rational number line.\nOn the other hand, the theories of, and as fields are not \\omega-categorical.\nThis follows from the fact that in all those fields, any of the infinitely many natural numbers can be defined by a formula of the form.\n\\aleph_0-categorical theories and their countable models also have strong ties with [oligomorphic groups](https://bliptext.com/articles/oligomorphic-group):\nThe equivalent characterisations of this subsection, due independently to [Engeler](https://bliptext.com/articles/erwin-engeler), [Ryll-Nardzewski](https://bliptext.com/articles/czes-aw-ryll-nardzewski) and [Svenonius](https://bliptext.com/articles/lars-svenonius), are sometimes referred to as the [Ryll-Nardzewski](https://bliptext.com/articles/czes-aw-ryll-nardzewski) theorem.\nIn combinatorial signatures, a common source of ω-categorical theories are [Fraïssé limits](https://bliptext.com/articles/fra-ss-limit), which are obtained as the limit of amalgamating all possible configurations of a class of finite relational structures.\n\n## Uncountable categoricity\n[Michael Morley](https://bliptext.com/articles/michael-d-morley) showed in 1963 that there is only one notion of uncountable categoricity for theories in countable languages.\nMorley's proof revealed deep connections between uncountable categoricity and the internal structure of the models, which became the starting point of classification theory and stability theory.\nUncountably categorical theories are from many points of view the most well-behaved theories.\nIn particular, complete strongly minimal theories are uncountably categorical.\nThis shows that the theory of algebraically closed fields of a given characteristic is uncountably categorical, with the transcendence degree of the field determining its isomorphism type.\nA theory that is both ω-categorical and uncountably categorical is called totally categorical.\n\n# Stability theory\nA key factor in the structure of the class of models of a first-order theory is its place in the stability hierarchy.\nA theory is called stable if it is \\lambda-stable for some infinite cardinal \\lambda.\nTraditionally, theories that are \\aleph_0-stable are called \\omega-stable.\n\n## The stability hierarchy\nA fundamental result in stability theory is the [stability spectrum theorem](https://bliptext.com/articles/stability-spectrum), which implies that every complete theory T in a countable signature falls in one of the following classes:\nA theory of the first type is called unstable, a theory of the second type is called strictly stable and a theory of the third type is called superstable.\nFurthermore, if a theory is \\omega-stable, it is stable in every infinite cardinal, so \\omega-stability is stronger than superstability.\nMany construction in model theory are easier when restricted to stable theories; for instance, every model of a stable theory has a saturated elementary extension, regardless of whether the generalised continuum hypothesis is true.\nShelah's original motivation for studying stable theories was to decide how many models a countable theory has of any uncountable cardinality.\nIf a theory is uncountably categorical, then it is \\omega-stable.\nMore generally, the [Main gap theorem](https://bliptext.com/articles/spectrum-of-a-theory) implies that if there is an uncountable cardinal \\lambda such that a theory T has less than 2^{\\lambda} models of cardinality \\lambda, then T is superstable.\n\n## Geometric stability theory\nThe stability hierarchy is also crucial for analysing the geometry of definable sets within a model of a theory.\nIn \\omega-stable theories, [Morley rank](https://bliptext.com/articles/morley-rank) is an important dimension notion for definable sets S within a model.\nIt is defined by [transfinite induction](https://bliptext.com/articles/transfinite-induction):\nA theory T in which every definable set has well-defined Morley Rank is called totally transcendental; if T is countable, then T is totally transcendental if and only if T is \\omega-stable.\nMorley Rank can be extended to types by setting the Morley Rank of a type to be the minimum of the Morley ranks of the formulas in the type.\nThus, one can also speak of the Morley rank of an element a over a parameter set A, defined as the Morley rank of the type of a over A.\nThere are also analogues of Morley rank which are well-defined if and only if a theory is superstable ([U-rank](https://bliptext.com/articles/u-rank)) or merely stable (Shelah's \\infty-rank).\nThose dimension notions can be used to define notions of independence and of generic extensions.\nMore recently, stability has been decomposed into simplicity and \"not the independence property\" (NIP).\n[Simple theories](https://bliptext.com/articles/simple-theory) are those theories in which a well-behaved notion of independence can be defined, while [NIP theories](https://bliptext.com/articles/nip-model-theory) generalise o-minimal structures.\nThey are related to stability since a theory is stable if and only if it is NIP and simple, and various aspects of stability theory have been generalised to theories in one of these classes.\n\n# Non-elementary model theory\nModel-theoretic results have been generalised beyond elementary classes, that is, classes axiomatisable by a first-order theory.\nModel theory in [higher-order logics](https://bliptext.com/articles/higher-order-logic) or [infinitary logics](https://bliptext.com/articles/infinitary-logic) is hampered by the fact that [completeness](https://bliptext.com/articles/g-del-s-completeness-theorem) and [compactness](https://bliptext.com/articles/compactness-theorem) do not in general hold for these logics.\nThis is made concrete by [Lindstrom's theorem](https://bliptext.com/articles/lindstrom-s-theorem), stating roughly that first-order logic is essentially the strongest logic in which both the Löwenheim-Skolem theorems and compactness hold.\nHowever, model theoretic techniques have been developed extensively for these logics too.\nIt turns out, however, that much of the model theory of more expressive logical languages is independent of [Zermelo-Fraenkel set theory](https://bliptext.com/articles/zermelo-fraenkel-set-theory).\nMore recently, alongside the shift in focus to complete stable and categorical theories, there has been work on classes of models defined semantically rather than axiomatised by a logical theory.\nOne example is homogeneous model theory, which studies the class of substructures of arbitrarily large homogeneous models.\nFundamental results of stability theory and geometric stability theory generalise to this setting.\nAs a generalisation of strongly minimal theories, [quasiminimally excellent](https://bliptext.com/articles/quasiminimal-excellence) classes are those in which every definable set is either countable or co-countable.\nThey are key to the model theory of the [complex exponential function](https://bliptext.com/articles/complex-exponential-function).\nThe most general semantic framework in which stability is studied are [abstract elementary classes](https://bliptext.com/articles/abstract-elementary-class), which are defined by a strong substructure relation generalising that of an elementary substructure.\nEven though its definition is purely semantic, every abstract elementary class can be presented as the models of a first-order theory which omit certain types.\nGeneralising stability-theoretic notions to abstract elementary classes is an ongoing research program.\n\n# Selected applications\nAmong the early successes of model theory are Tarski's proofs of quantifier elimination for various algebraically interesting classes, such as the [real closed fields](https://bliptext.com/articles/real-closed-field), [Boolean algebras](https://bliptext.com/articles/boolean-algebra-structure) and [algebraically closed fields](https://bliptext.com/articles/algebraically-closed-field) of a given [characteristic](https://bliptext.com/articles/characteristic-algebra).\nQuantifier elimination allowed Tarski to show that the first-order theories of real-closed and algebraically closed fields as well as the first-order theory of Boolean algebras are decidable, classify the Boolean algebras up to elementary equivalence and show that the theories of real-closed fields and algebraically closed fields of a given characteristic are unique.\nFurthermore, quantifier elimination provided a precise description of definable relations on algebraically closed fields as [algebraic varieties](https://bliptext.com/articles/algebraic-varieties) and of the definable relations on real-closed fields as [semialgebraic sets](https://bliptext.com/articles/semialgebraic-sets)\nIn the 1960s, the introduction of the [ultraproduct](https://bliptext.com/articles/ultraproduct) construction led to new applications in algebra.\nThis includes [Ax's](https://bliptext.com/articles/james-ax) work on [pseudofinite fields](https://bliptext.com/articles/pseudofinite-field), proving that the theory of finite fields is decidable, and Ax and [Kochen's](https://bliptext.com/articles/simon-b-kochen) proof of as special case of Artin's conjecture on diophantine equations, the [Ax-Kochen theorem](https://bliptext.com/articles/ax-kochen-theorem).\nThe ultraproduct construction also led to [Abraham Robinson](https://bliptext.com/articles/abraham-robinson)'s development of [nonstandard analysis](https://bliptext.com/articles/nonstandard-analysis), which aims to provide a rigorous calculus of [infinitesimals](https://bliptext.com/articles/infinitesimals).\nMore recently, the connection between stability and the geometry of definable sets led to several applications from algebraic and diophantine geometry, including [Ehud Hrushovski](https://bliptext.com/articles/ehud-hrushovski)'s 1996 proof of the geometric [Mordell-Lang conjecture](https://bliptext.com/articles/mordell-lang-conjecture) in all characteristics In 2001, similar methods were used to prove a generalisation of the Manin-Mumford conjecture.\nIn 2011, [Jonathan Pila](https://bliptext.com/articles/jonathan-pila) applied techniques around [o-minimality](https://bliptext.com/articles/o-minimality) to prove the [André-Oort conjecture](https://bliptext.com/articles/andr-oort-conjecture) for products of Modular curves.\nIn a separate strand of inquiries that also grew around stable theories, Laskowski showed in 1992 that [NIP theories](https://bliptext.com/articles/nip-model-theory) describe exactly those definable classes that are [PAC-learnable](https://bliptext.com/articles/probably-approximately-correct-learning) in machine learning theory.\nThis has led to several interactions between these separate areas.\nIn 2018, the correspondence was extended as Hunter and Chase showed that stable theories correspond to [online learnable classes](https://bliptext.com/articles/online-machine-learning).\n\n# History\nModel theory as a subject has existed since approximately the middle of the 20th century, and the name was coined by [Alfred Tarski](https://bliptext.com/articles/alfred-tarski), a member of the [Lwów–Warsaw school](https://bliptext.com/articles/lw-w-warsaw-school), in 1954.\nHowever some earlier research, especially in [mathematical logic](https://bliptext.com/articles/mathematical-logic), is often regarded as being of a model-theoretical nature in retrospect.\nThe 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](https://bliptext.com/articles/leopold-l-wenheim) in 1915.\nThe [compactness theorem](https://bliptext.com/articles/compactness-theorem) was implicit in work by [Thoralf Skolem](https://bliptext.com/articles/thoralf-skolem), but it was first published in 1930, as a lemma in [Kurt Gödel](https://bliptext.com/articles/kurt-g-del)'s proof of his [completeness theorem](https://bliptext.com/articles/g-del-s-completeness-theorem).\nThe Löwenheim–Skolem theorem and the compactness theorem received their respective general forms in 1936 and 1941 from [Anatoly Maltsev](https://bliptext.com/articles/anatoly-maltsev).\nThe development of model theory as an independent discipline was brought on by Alfred Tarski during the [interbellum](https://bliptext.com/articles/interwar-period).\nTarski's work included [logical consequence](https://bliptext.com/articles/logical-consequence), [deductive systems](https://bliptext.com/articles/deductive-system), the algebra of logic, the theory of definability, and the [semantic definition of truth](https://bliptext.com/articles/semantic-theory-of-truth), among other topics.\nHis semantic methods culminated in the model theory he and a number of his [Berkeley](https://bliptext.com/articles/university-of-california-berkeley) students developed in the 1950s and '60s.\nIn the further history of the discipline, different strands began to emerge, and the focus of the subject shifted.\nIn the 1960s, techniques around ultraproducts became a popular tool in model theory.\nAt the same time, researchers such as [James Ax](https://bliptext.com/articles/james-ax) were investigating the first-order model theory of various algebraic classes, and others such as [H. Jerome Keisler](https://bliptext.com/articles/h-jerome-keisler) were extending the concepts and results of first-order model theory to other logical systems.\nThen, inspired by [Morley's problem](https://bliptext.com/articles/morley-s-problem), Shelah developed [stability theory](https://bliptext.com/articles/stable-theory).\nHis work around stability changed the complexion of model theory, giving rise to a whole new class of concepts.\nThis is known as the paradigm shift.\nOver the next decades, it became clear that the resulting stability hierarchy is closely connected to the geometry of sets that are definable in those models; this gave rise to the subdiscipline now known as geometric stability theory.\nAn example of an influential proof from geometric model theory is [Hrushovski](https://bliptext.com/articles/ehud-hrushovski)'s proof of the [Mordell–Lang conjecture](https://bliptext.com/articles/mordell-lang-conjecture) for function fields.\n\n# Connections to related branches of mathematical logic\n\n## Finite model theory\n[Finite model theory](https://bliptext.com/articles/finite-model-theory), which concentrates on finite structures, diverges significantly from the study of infinite structures in both the problems studied and the techniques used.\nIn particular, many central results of classical model theory that fail when restricted to finite structures.\nThis includes the [compactness theorem](https://bliptext.com/articles/compactness-theorem), [Gödel's completeness theorem](https://bliptext.com/articles/g-del-s-completeness-theorem), and the method of [ultraproducts](https://bliptext.com/articles/ultraproducts) for [first-order logic](https://bliptext.com/articles/first-order-logic).\nAt the interface of finite and infinite model theory are algorithmic or [computable model theory](https://bliptext.com/articles/computable-model-theory) and the study of [0-1 laws](https://bliptext.com/articles/zero-one-law-model-theory), where the infinite models of a generic theory of a class of structures provide information on the distribution of finite models.\nProminent application areas of FMT are [descriptive complexity theory](https://bliptext.com/articles/descriptive-complexity-theory), [database theory](https://bliptext.com/articles/database-theory) and [formal language theory](https://bliptext.com/articles/formal-language-theory).\n\n## Set theory\nAny [set theory](https://bliptext.com/articles/formal-system) (which is expressed in a [countable](https://bliptext.com/articles/countable) language), if it is consistent, has a [countable](https://bliptext.com/articles/countable) model; this is known as [Skolem's paradox](https://bliptext.com/articles/skolem-s-paradox), since there are sentences in [set theory](https://bliptext.com/articles/formal-system) which postulate the existence of un[countable](https://bliptext.com/articles/countable) sets and yet these sentences are true in our [countable](https://bliptext.com/articles/countable) model.\nParticularly the proof of the independence of the [continuum hypothesis](https://bliptext.com/articles/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.\nThe model-theoretic viewpoint has been useful in [set theory](https://bliptext.com/articles/set-theory); for example in [Kurt Gödel](https://bliptext.com/articles/kurt-g-del)'s work on the constructible universe, which, along with the method of [forcing](https://bliptext.com/articles/forcing-mathematics) developed by [Paul Cohen](https://bliptext.com/articles/paul-cohen-mathematician) can be shown to prove the (again philosophically interesting) [independence](https://bliptext.com/articles/independence-mathematical-logic) of the [axiom of choice](https://bliptext.com/articles/axiom-of-choice) and the continuum hypothesis from the other axioms of [set theory](https://bliptext.com/articles/set-theory).\nIn the other direction, model theory is itself formalised within Zermelo-Fraenkel set theory.\nFor instance, the development of the fundamentals of model theory (such as the compactness theorem) rely on the axiom of choice, and is in fact equivalent over Zermelo-Fraenkel set theory without choice to the Boolean prime ideal theorem.\nOther results in model theory depend on set-theoretic axioms beyond the standard ZFC framework.\nFor example, if the Continuum Hypothesis holds then every countable model has an ultrapower which is saturated (in its own cardinality).\nSimilarly, if the Generalized Continuum Hypothesis holds then every model has a saturated elementary extension.\nNeither of these results are provable in ZFC alone.\nFinally, some questions arising from model theory (such as compactness for infinitary logics) have been shown to be equivalent to large cardinal axioms.\n\n# Canonical textbooks\n\n## Other textbooks\n\n## Free online texts","revisionCount":0},"hasMore":false,"nextCursor":null}