Model theory

Model theory recognizes and is intimately concerned with a duality: it examines semantical elements (meaning and truth) by means of syntactical elements (formulas and proofs) of a corresponding language. In a summary definition, dating from 1973:

model theory = universal algebra + logic.[2]

Model theory developed rapidly during the 1990s, and a more modern definition is provided by Wilfrid Hodges (1997):

model theory = algebraic geometry − fields.

This is a clever slogan, implying that there are many commonalities: so, for example, an algebraic variety can be informally described as the locus of points where a collection of polynomials are zero. Likewise, a model can be described as a locus of interpretations where a collection of sentences are true. There are further analogies extending to varying depths.

Another commonly recurring slogan states that "if proof theory is about the sacred, then model theory is about the profane",[3] indicating that these two topics are in a sense dual to each-other. Much like proof theory, model theory is situated in an area of interdisciplinarity among mathematics, philosophy, and computer science. Model theory is used in a variety of settings, both academic and industrial. These include:

• Proving results on axiom systems. For example, the proof that the continuum hypothesis is independent from the other axioms of Zermelo–Fraenkel set theory (ZFC) is done by building inside ZFC a model of ZFC where the continuum hypothesis is true, and another model where it is false (see Continuum hypothesis § Independence from ZFC).
• Providing the foundation for satisfiability modulo theories solvers, which are commonly deployed for functional verification in electronic design automation. Such solvers search for sentences that are satisfiable, up to equivalent statements in some specific theory, such as the theory of equality or the theory of linear algebra.
• Providing the foundation for relational models, which are the fragment consisting of structures whose signatures consist entirely of relations. Well-known results include that SQL and noSQL are categorical duals to each other.

The most prominent professional 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 higher-order 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 two-cardinal theorem, Scott's isomorphism theorem, the omitting types theorem, and the Ryll-Nardzewski theorem. Examples of early results from model theory applied to fields are Tarski's elimination of quantifiers for real closed fields, Ax's theorem on pseudo-finite fields, and Robinson's development of non-standard 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 o-minimality, 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.

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 first-order logic.

The main application areas of FMT are descriptive complexity theory, database theory and formal language theory.

Whereas universal algebra provides the semantics for a signature, logic provides the syntax. With terms, identities and quasi-identities, even universal algebra has some limited syntactic tools; first-order logic is the result of making quantification explicit and adding negation into the picture.

A first-order formula is built out of atomic formulas such as R(f(x,y),z) or y = x + 1 by means of the Boolean connectives ${\displaystyle \neg ,\land ,\lor ,\rightarrow }$ and prefixing of quantifiers ${\displaystyle \forall v}$ or ${\displaystyle \exists v}$. A sentence is a formula in which each occurrence of a variable is in the scope of a corresponding quantifier. Examples for formulas are φ (or φ(x) to mark the fact that at most x is an unbound variable in φ) and ψ defined as follows:

${\displaystyle {\varphi \;=\;\forall u\forall v(\exists w(x\times w=u\times v)\rightarrow (\exists w(x\times w=u)\lor \exists w(x\times w=v)))\land x\neq 0\land x\neq 1,}}$

${\displaystyle \psi \;=\;\forall u\forall v((u\times v=x)\rightarrow (u=x)\lor (v=x))\land x\neq 0\land x\neq 1.}$

(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 ${\displaystyle {\mathcal {N}}}$ of the natural numbers, for example, an element n satisfies the formula φ if and only if n is a prime number. The formula ψ similarly defines irreducibility. Tarski gave a rigorous definition, sometimes called "Tarski's definition of truth", for the satisfaction relation ${\displaystyle \models }$, so that one easily proves:

${\displaystyle {\mathcal {N}}\models \varphi (n)\iff n}$ is a prime number.

${\displaystyle {\mathcal {N}}\models \psi (n)\iff n}$ is irreducible.

A set T of sentences is called a (first-order) theory. A theory is satisfiable if it has a model ${\displaystyle {\mathcal {M}}\models T}$, i.e. a structure (of the appropriate signature) which satisfies all the sentences in the set T. Consistency of a theory is usually defined in a syntactical way, but in first-order logic by the completeness theorem there is no need to distinguish between satisfiability and consistency. Therefore, model theorists often use "consistent" as a synonym for "satisfiable".

A theory is called categorical if it determines a structure up to isomorphism, but it turns out that this definition is not useful, due to serious restrictions in the expressivity of first-order logic. The Löwenheim–Skolem theorem implies that for every theory T having a countable signature[4] which has an infinite model for some infinite cardinal number, then it has a model of size κ for any infinite cardinal number κ. Since two models of different sizes cannot possibly be isomorphic, only finitary structures can be described by a categorical theory.

Lack of expressivity (when compared to higher logics such as second-order logic) has its advantages, though. For model theorists, the Löwenheim–Skolem theorem is an important practical tool rather than the source of Skolem's paradox. In a certain sense made precise by 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.

As a corollary (i.e., its contrapositive), the compactness theorem says that every unsatisfiable first-order theory has a finite unsatisfiable subset. This theorem is of central importance in infinite model theory, where the words "by compactness" are commonplace. One way to prove it is by means of ultraproducts. An alternative proof uses the completeness theorem, which is otherwise reduced to a marginal role in most of modern model theory.

The first step, often trivial, for applying the methods of model theory to a class of mathematical objects such as groups, or trees in the sense of graph theory, is to choose a signature σ and represent the objects as σ-structures. The next step is to show that the class is an elementary class, i.e. axiomatizable in first-order logic (i.e. there is a theory T such that a σ-structure is in the class if and only if it satisfies T ). E.g. this step fails for the trees, since connectedness cannot be expressed in first-order logic. Axiomatizability ensures that model theory can speak about the right objects. Quantifier elimination can be seen as a condition which ensures that model theory does not say too much about the objects.

A theory T has quantifier elimination if every first-order formula φ(x₁, ..., x_n) over its signature is equivalent modulo T to a first-order formula ψ(x₁, ..., x_n) without quantifiers, i.e. ${\displaystyle \forall x_{1}\dots \forall x_{n}(\phi (x_{1},\dots ,x_{n})\leftrightarrow \psi (x_{1},\dots ,x_{n}))}$ holds in all models of T. For example, the theory of algebraically closed fields in the signature σ_ring = (×,+,−,0,1) has quantifier elimination because every formula is equivalent to a Boolean combination of equations between polynomials.

A substructure of a σ-structure is a subset of its domain, closed under all functions in its signature σ, which is regarded as a σ-structure by restricting all functions and relations in σ to the subset. An embedding of a σ-structure ${\displaystyle {\mathcal {A}}}$ into another σ-structure ${\displaystyle {\mathcal {B}}}$ is a map f: A → B between the domains which can be written as an isomorphism of ${\displaystyle {\mathcal {A}}}$ with a substructure of ${\displaystyle {\mathcal {B}}}$. Every embedding is an injective homomorphism, but the converse holds only if the signature contains no relation symbols.

If a theory does not have quantifier elimination, one can add additional symbols to its signature so that it does. Early model theory spent much effort on proving axiomatizability and quantifier elimination results for specific theories, especially in algebra. But often instead of quantifier elimination a weaker property suffices:

A theory T is called model-complete if every substructure of a model of T which is itself a model of T is an elementary substructure. There is a useful criterion for testing whether a substructure is an elementary substructure, called the Tarski–Vaught test. It follows from this criterion that a theory T is model-complete if and only if every first-order formula φ(x₁, ..., x_n) over its signature is equivalent modulo T to an existential first-order formula, i.e. a formula of the following form:

${\displaystyle \exists v_{1}\dots \exists v_{m}\psi (x_{1},\dots ,x_{n},v_{1},\dots ,v_{m})}$,

where ψ is quantifier free. A theory that is not model-complete may or may not have a model completion, which is a related model-complete theory that is not, in general, an extension of the original theory. A more general notion is that of model companions.

As observed in the section on first-order logic, first-order theories cannot be categorical, i.e. they cannot describe a unique model up to isomorphism, unless that model is finite. But two famous model-theoretic theorems deal with the weaker notion of κ-categoricity for a cardinal κ. 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. ${\displaystyle \aleph _{0}}$ + |σ|, where |σ| is the cardinality of the signature). For finite or countable signatures this means that there is a fundamental difference between ${\displaystyle \aleph _{0}}$-cardinality and κ-cardinality for uncountable κ.

A few characterizations of ${\displaystyle \aleph _{0}}$-categoricity include:

For a complete first-order theory T in a finite or countable signature the following conditions are equivalent:

1. T is ${\displaystyle \aleph _{0}}$-categorical.
2. For every natural number n, the Stone space S_n(T) is finite.
3. For every natural number n, the number of formulas φ(x₁, ..., x_n) in n free variables, up to equivalence modulo T, is finite.

This result, due independently to Engeler, Ryll-Nardzewski and Svenonius, is sometimes referred to as the Ryll-Nardzewski theorem.

Further, ${\displaystyle \aleph _{0}}$-categorical theories and their countable models have strong ties with oligomorphic groups. They are often constructed as Fraïssé limits.

Michael Morley's highly non-trivial result that (for countable languages) there is only one notion of uncountable categoricity was the starting point for modern model theory, and in particular classification theory and stability theory:

Morley's categoricity theorem

If a first-order theory T in a finite or countable signature is κ-categorical for some uncountable cardinal κ, then T is κ-categorical for all uncountable cardinals κ.

Uncountably categorical (i.e. κ-categorical for all uncountable cardinals κ) theories are from many points of view the most well-behaved theories. A theory that is both ${\displaystyle \aleph _{0}}$-categorical and uncountably categorical is called totally categorical.

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 model-theoretic viewpoint has been useful in set theory; for example in Kurt Gödel's work on the constructible universe, which, along with the method of forcing developed by Paul Cohen can be shown to prove the (again philosophically interesting) independence of the axiom of choice and the continuum hypothesis from the other axioms of set theory.

In the other direction, model theory itself can be formalized within ZFC set theory. 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 set-theoretic 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.

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 model-theoretical nature in retrospect. The first significant result in what is now model theory was a special case of the downward Löwenheim–Skolem theorem, published by Leopold Löwenheim in 1915. The compactness theorem was implicit in work by Thoralf Skolem,[5] 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 can be traced to 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. These modern concepts of model theory influenced Hilbert's program and modern mathematics.

• Map of the Universe - Small database of theories and its properties.