In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models, taken as interpretations that satisfy the sentences of that theory.^{[1]} The 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. In particular, model theorists also investigate the sets that can be defined in a model of a theory, and the relationship of such definable sets to each other.As a separate discipline, model theory goes back to Alfred Tarski, who first used the term "Theory of Models" in publication in 1954.^{[2]} Since the 1970s, the subject has been shaped decisively by Saharon Shelah's stability theory. The 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:
model theory = universal algebra + logic^{[3]}
where universal algebra stands for mathematical structures and logic for logical theories; and
model theory = algebraic geometry − fields.
where logical formulas are to definable sets what equations are to varieties over a field.^{[4]}
Nonetheless, the interplay of classes of models and the sets definable in them has been crucial to the development of model theory throughout its history. For instance, while stability was originally introduced to classify theories by their numbers of models in a given cardinality, stability theory proved crucial to understanding the geometry of definable sets.
Compared to other areas of mathematical logic such as proof theory, model theory is often less concerned with formal rigour and closer in spirit to classical mathematics.This has prompted the comment that "if proof theory is about the sacred, then model theory is about the profane".^{[5]} The applications of model theory to algebraic and diophantine geometry reflect this proximity to classical mathematics, as they often involve an integration of algebraic and modeltheoretic results and techniques.
The most prominent scholarly organization in the field of model theory is the Association for Symbolic Logic.
This page focuses on finitary first order model theory of infinite structures. 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. Model theory in higherorder logics or infinitary logics is hampered by the fact that completeness and compactness do not in general hold for these logics. However, a great deal of study has also been done in such logics.
Informally, model theory can be divided into classical model theory, model theory applied to groups and fields, and geometric model theory. A missing subdivision is computable model theory, but this can arguably be viewed as an independent subfield of logic.
Examples of early theorems from classical model theory include Gödel's completeness theorem, the upward and downward Löwenheim–Skolem theorems, Vaught's twocardinal theorem, Scott's isomorphism theorem, the omitting types theorem, and the RyllNardzewski theorem. Examples of early results from model theory applied to fields are Tarski's elimination of quantifiers for real closed fields, Ax's theorem on pseudofinite fields, and Robinson's development of nonstandard analysis. An important step in the evolution of classical model theory occurred with the birth of stability theory (through Morley's theorem on uncountably categorical theories and Shelah's classification program), which developed a calculus of independence and rank based on syntactical conditions satisfied by theories.
During the last several decades applied model theory has repeatedly merged with the more pure stability theory. The result of this synthesis is called geometric model theory in this article (which is taken to include ominimality, for example, as well as classical geometric stability theory). An example of a proof from geometric model theory is Hrushovski's proof of the Mordell–Lang conjecture for function fields. The ambition of geometric model theory is to provide a geography of mathematics by embarking on a detailed study of definable sets in various mathematical structures, aided by the substantial tools developed in the study of pure model theory.
See main article: Firstorder logic.
\neg,\land,\lor, →
\forallv
\existsv
{\varphi = \forallu\forallv(\existsw(x x w=u x v) → (\existsw(x x w=u)\lor\existsw(x x w=v)))\landx\ne0\landx\ne1,}
\psi = \forallu\forallv((u x v=x) → (u=x)\lor(v=x))\landx\ne0\landx\ne1.
(Note that the equality symbol has a double meaning here.) It is intuitively clear how to translate such formulas into mathematical meaning. In the σ_{smr}structure
lN
\models
lN\models\varphi(n)\iffn
lN\models\psi(n)\iffn
A set T of sentences is called a (firstorder) theory. A theory is satisfiable if it has a model
lM\modelsT
Gödel's completeness theorem (not to be confused with his incompleteness theorems) says that a theory has a model if and only if it is consistent, i.e. no contradiction is proved by the theory.Therefore, model theorists often use "consistent" as a synonym for "satisfiable".
A signature or language is a set of nonlogical symbols such that each symbol is either a function symbol or a relation symbol and has a specified arity. A structure is a set
M
M
\sigma_{or}=\{0,1,+, x ,,<\}
0
1
+
x

<
\Q
+
\Q^{2}
\Q
<
\Q^{2}
(\Q,\sigma_{or})
l{N}
T
T
l{N}
l{N}
lA
lB
A substructure is said to be elementary if for any firstorder formula φ and any elements a_{1}, ..., a_{n} of
lA
lA\models\varphi(a_{1,}...,a_{n)}
lB\models\varphi(a_{1,}...,a_{n)}
lA
lB
lA\models\varphi
lB\models\varphi
\overline{Q
C
Q
C
Q
An embedding of a σstructure
lA
lB
lA
lB
A field or a vector space can be regarded as a (commutative) group by simply ignoring some of its structure. The corresponding notion in model theory is that of a reduct of a structure to a subset of the original signature. The opposite relation is called an expansion  e.g. the (additive) group of the rational numbers, regarded as a structure in the signature can be expanded to a field with the signature or to an ordered group with the signature .
Similarly, 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. Conversely, a complete σtheory can be regarded as a σ'theory, and one can extend it (in more than one way) to a complete σ'theory. The terms reduct and expansion are sometimes applied to this relation as well.
The compactness theorem states that a set of sentences S is satisfiable if every finite subset of S is satisfiable. The analogous statement with consistent instead of satisfiable is trivial, since every proof can have only a finite number of antecedents used in the proof. The completeness theorem allows us to transfer this to satsifiability. However, there are also several direct (semantic) proofs of the compactness theorem.As a corollary (i.e., its contrapositive), the compactness theorem says that every unsatisfiable firstorder theory has a finite unsatisfiable subset. This theorem is of central importance in model theory, where the words "by compactness" are commonplace.
Another cornerstone of firstorder model theory is the LöwenheimSkolem theorem. According to the LöwenheimSkolem Theorem, every infinite structure in a countable signature has a countable elementary substructure. Conversely, 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). In particular, the LöwenheimSkolem Theorem implies that any theory in a countable signature with infinite models has a countable model as well as arbitrarily large models.
In a certain sense made precise by Lindström's theorem, firstorder logic is the most expressive logic for which both the Löwenheim–Skolem theorem and the compactness theorem hold.
In model theory, definable sets are important objects of study. For instance, in
N
\forallu\forallv(\existsw(x x w=u x v) → (\existsw(x x w=u)\lor\existsw(x x w=v)))\landx\ne0\landx\ne1
\existsy(2 x y=x)
l{M}^{n}
y=x x x
(x,y)
y=x^{2}
Both of the definitions mentioned here are parameterfree, that is, the defining formulas don't mention any fixed domain elements. However, one can also consider definitions with parameters from the model.For instance, in
R
y=x x x+\pi
\pi
R
In general, definable sets without quantifiers are easy to describe, while definable sets involving possibly nested quantifiers can be much more complicated.
This makes quantifier elimination a crucial tool for analysing definable sets: A theory T has quantifier elimination if every firstorder formula φ(x_{1}, ..., x_{n}) over its signature is equivalent modulo T to a firstorder formula ψ(x_{1}, ..., x_{n}) without quantifiers, i.e.
\forallx_{1...\forall}x_{n(\phi(x}_{1,...,x}_{n)\leftrightarrow}\psi(x_{1,...,x}_{n))}
If a theory does not have quantifier elimination, one can add additional symbols to its signature so that it does. Early model theory spent much effort on proving axiomatizability and quantifier elimination results for specific theories, especially in algebra. But often instead of quantifier elimination a weaker property suffices:
A theory T is called modelcomplete if every substructure of a model of T which is itself a model of T is an elementary substructure. There is a useful criterion for testing whether a substructure is an elementary substructure, called the Tarski–Vaught test. It follows from this criterion that a theory T is modelcomplete if and only if every firstorder formula φ(x_{1}, ..., x_{n}) over its signature is equivalent modulo T to an existential firstorder formula, i.e. a formula of the following form:
\existsv_{1...\exists}v_{m\psi(x}_{1,...,x}_{n,v}_{1,...,v}_{m)}
In every structure, every finite subset
\{a_{1,}...,a_{n\}}
x=a_{1}\vee...\veea_{n}
This leads to the concept of a minimal structure. A structure
l{M}
A\subseteql{M}
l{M}
On the other hand, the field
R
\varphi(x) = \existsy(y x y=x)
\varphi
R
l{M}
A\subseteql{M}
l{M}
See main article: Interpretation (model theory). Particularly important are those definable sets that are also substructures, i. e. contain all constants and are closed under function application. For instance, one can study the definable subgroups of a certain group.However, there is no need to limit oneself to substructures in the same signature. Since formulas with n free variables define subsets of
l{M}^{n}
a\inl{M}
\varphi(x)
l{M}
\varphi(a)
One can even go one step further, and move beyond immediate substructures.Given a mathematical structure, there are very often associated structures which can be constructed as a quotient of part of the original structure via an equivalence relation. An important example is a quotient group of a group. One might say that to understand the full structure one must understand these quotients. When the equivalence relation is definable, we can give the previous sentence a precise meaning. We say that these structures are interpretable.A key fact is that one can translate sentences from the language of the interpreted structures to the language of the original structure. Thus one can show that if a structure
l{M}
l{M}
See main article: Type (model theory).
For a sequence of elements
a_{1,}...,a_{n}
l{M}
l{M}
\varphi(x_{1,}...,x_{n)}
a_{1,}...,a_{n}
a_{1,}...,a_{n}
l{M}
a_{1,}...,a_{n}
b_{1,}...,b_{n}
a_{1,}...,a_{n}
b_{1,}...,b_{n}
The real number line
R
a\inR
a_{1,}a_{2}
a_{1}<a_{2}
a_{1}=a_{2}
a_{2}<a_{1}
Z\subseteqR
More generally, whenever
l{M}
l{M}
l{N}
l{M}
l{M  
S  
n 
l{M}
S_{n(T)}
\varphi
l{M}
\varphi → \psi
\psi
Since the real numbers
R
\{n<xn\inZ\}
Z\subseteqR
R
A subset of
l{M}^{n}
l{M}^{n}
M
n
A
A[x_{1,\ldots,x}_{n]}
While not every type is realised in every structure, every structure realises its isolated types.If the only types over the empty set that are realised in a structure are the isolated types, then the structure is called atomic.
On the other hand, no structure realises every type over every parameter set; if one takes all of
l{M}
l{M}
l{M}
a\inl{M}
l{M}
l{M}
A\subsetl{M}
l{M}
While an automorphism that is constant on A will always preserve types over A, it is generally not true that any two sequences
a_{1,}...,a_{n}
b_{1,}...,b_{n}
l{M}
l{M}
The real number line is atomic in the language that contains only the order
<
a_{1,}...,a_{n}
R
a_{1,}...,a_{n}
Z
Q
Q
The set of definable subsets of
l{M}^{n}
A
n
A
\{p\varphi\inp\}
\varphi
While types in algebraically closed fields correspond to the spectrum of the polynomial ring, the topology on the type space is the constructible topology: a set of types is basic open iff it is of the form
\{p:f(x)=0\inp\}
\{p:f(x) ≠ 0\inp\}
See main article: Categorical theory.
A theory was originally called categorical if it determines a structure up to isomorphism. It turns out that this definition is not useful, due to serious restrictions in the expressivity of firstorder logic. The Löwenheim–Skolem theorem implies that if a theory T has an infinite model for some infinite cardinal number, then it has a model of size κ for any sufficiently large cardinal number κ. Since two models of different sizes cannot possibly be isomorphic, only finite structures can be described by a categorical theory.
However, the weaker notion of κcategoricity for a cardinal κ has become a key concept in model theory. A theory T is called κcategorical if any two models of T that are of cardinality κ are isomorphic. It turns out that the question of κcategoricity depends critically on whether κ is bigger than the cardinality of the language (i.e.
\aleph_{0}
\omega
\omega
\omega
For a complete firstorder theory T in a finite or countable signature the following conditions are equivalent:
\omega
The theory of
(Q,<)
(R,<)
\omega
p(x_{1,}...,x_{n)}
x_{i}
Q
R
C
\omega
x=1+...+1
\aleph_{0}
A complete firstorder theory T in a finite or countable signature is
\omega
The equivalent charcaterisations of this subsection, due independently to Engeler, RyllNardzewski and Svenonius, are sometimes referred to as the RyllNardzewski theorem.
In combinatorial signatures, a common source of
\omega
Michael Morley showed in 1963 that there is only one notion of uncountable categoricity for theories in countable languages.^{[6]}
If a firstorder theory T in a finite or countable signature is κcategorical for some uncountable cardinal κ, then T is κcategorical for all uncountable cardinals κ.
Morley'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. Uncountably categorical theories are from many points of view the most wellbehaved theories.In particular, complete strongly minimal theories are uncountably categorical. This 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.
A theory that is both
\omega
Among the early successes of model theory are Tarski's proofs of the decidability of various algebraically interesting classes, such as the real closed fields, Boolean algebras and algebraically closed fields of a given characteristic.
In the 1960s, considerations around saturated models and the ultraproduct construction lead to the Abraham Robinson's development of nonstandard analysis.
In 1965, James Ax and Simon B. Kochen showed a special case of Artin's conjecture on diophantine equations, the AxKochen theorem, again using an ultraproduct construction.^{[7]}
More recently, the connection between stability and the geometry of definable sets led to several applications from algebraic and diophantine geometry, including Ehud Hrushovski's 1996 proof of the geometric MordellLang conjecture in all characteristics^{[8]}
In 2011, Jonathan Pila applied techniques around ominimality to prove the AndréOort conjecture for products of Modular curves. ^{[9]}
In a separate strand of inquiries that also grew around stable theories, Laskowski showed in 1992 that NIP theories describe exactly those definable classes that are PAClearnable in machine learning theory. ^{[10]}
Model theory as a subject has existed since approximately the middle of the 20th century. However some earlier research, especially in mathematical logic, is often regarded as being of a modeltheoretical nature in retrospect. The first significant result in what is now model theory was a special case of the downward Löwenheim–Skolem theorem, published by Leopold Löwenheim in 1915. The compactness theorem was implicit in work by Thoralf Skolem,^{[11]} but it was first published in 1930, as a lemma in Kurt Gödel's proof of his completeness theorem. The Löwenheim–Skolem theorem and the compactness theorem received their respective general forms in 1936 and 1941 from Anatoly Maltsev.The development of model theory as an independent discipline was brought on by Alfred Tarski, a member of the Lwów–Warsaw school during the interbellum. Tarski's work included logical consequence, deductive systems, the algebra of logic, the theory of definability, and the semantic definition of truth, among other topics. His semantic methods culminated in the model theory he and a number of his Berkeley students developed in the 1950s and '60s.
In the further history of the discipline, different strands began to emerge, and the focus of the subject shifted. In the 1960s, techniques around ultraproducts became a popular tool in model theory. At the same time, researchers such as James Ax were investigating the firstorder model theory of various algebraic classes, and others such as H. Jerome Keisler were extending the concepts and results of firstorder model theory to other logical systems. Then, Saharon Shelah's work around categoricity and Morley's problem changed the complexion of model theory, giving rise to a whole new class of concepts. The stability theory (classification theory) Shelah developed since the late 1960s aims to classify theories by the number of different models they have of any given cardinality. Over 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.
See main article: Finite model theory. Finite model theory (FMT) is the subarea of model theory (MT) that deals with its restriction to interpretations on finite structures, which have a finite universe.
Since many central theorems of model theory do not hold when restricted to finite structures, FMT is quite different from MT in its methods of proof. Central results of classical model theory that fail for finite structures under FMT include the compactness theorem, Gödel's completeness theorem, and the method of ultraproducts for firstorder logic.
The main application areas of FMT are descriptive complexity theory, database theory and formal language theory.
Any set theory (which is expressed in a countable language), if it is consistent, has a countable model; this is known as Skolem's paradox, since there are sentences in set theory which postulate the existence of uncountable sets and yet these sentences are true in our countable model. Particularly the proof of the independence of the continuum hypothesis requires considering sets in models which appear to be uncountable when viewed from within the model, but are countable to someone outside the model.
The modeltheoretic viewpoint has been useful in set theory; for example in Kurt Gödel's work on the constructible universe, which, along with the method of forcing developed by Paul Cohen can be shown to prove the (again philosophically interesting) independence of the axiom of choice and the continuum hypothesis from the other axioms of set theory.
In the other direction, model theory itself can be formalized within ZFC set theory. For instance, the formalization of satisfaction in ZFC is done inductively, based on Tarski's Tschema and observation of where the members of the range of variable assignments lie.^{[12]} The development of the fundamentals of model theory (such as the compactness theorem) rely on the axiom of choice, or more exactly the Boolean prime ideal theorem. Other results in model theory depend on settheoretic axioms beyond the standard ZFC framework. For example, if the Continuum Hypothesis holds then every countable model has an ultrapower which is saturated (in its own cardinality). Similarly, if the Generalized Continuum Hypothesis holds then every model has a saturated elementary extension. Neither of these results are provable in ZFC alone. Finally, some questions arising from model theory (such as compactness for infinitary logics) have been shown to be equivalent to large cardinal axioms.