Model Theory

Model theory is the study of the relationship between formal languages and the mathematical structures that give them meaning. Where proof theory examines what can be derived from axioms syntactically, model theory asks what those axioms say — which structures satisfy them, how those structures relate to one another, and what properties of structures are expressible in a given language. It is, in the deepest sense, where syntax meets semantics: the bridge between formulas as strings of symbols and the rich mathematical worlds they describe. The field’s central insight is that the interplay between a theory (a set of sentences) and its class of models reveals profound structural information about both.

Structures and Elementary Equivalence

A first-order structure (or model) $\mathcal{A} = (A, \sigma^{\mathcal{A}})$ consists of a nonempty underlying set $A$ (the domain or universe) together with an interpretation $\sigma^{\mathcal{A}}$ that assigns to each constant symbol $c$ an element $c^{\mathcal{A}} \in A$, to each $n$-ary function symbol $f$ a function $f^{\mathcal{A}} : A^n \to A$, and to each $n$-ary relation symbol $R$ a relation $R^{\mathcal{A}} \subseteq A^n$. This definition reprises what appears in first-order logic, but model theory treats structures as primary objects of study rather than mere backdrops for evaluating formulas. The notions of isomorphism ($\mathcal{A} \cong \mathcal{B}$, a bijection preserving all structure), homomorphism (a map preserving relations and operations, not necessarily injective), and embedding (an injective homomorphism) provide the basic morphisms between structures, analogous to morphisms in algebra.

Two structures $\mathcal{A}$ and $\mathcal{B}$ in the same signature are elementarily equivalent, written $\mathcal{A} \equiv \mathcal{B}$, if they satisfy exactly the same first-order sentences: for every sentence $\varphi$, $\mathcal{A} \models \varphi$ if and only if $\mathcal{B} \models \varphi$. Isomorphic structures are always elementarily equivalent, but the converse fails spectacularly: the rational numbers $(\mathbb{Q}, <)$ and the real numbers $(\mathbb{R}, <)$ as dense linear orders without endpoints are elementarily equivalent yet not isomorphic (they have different cardinalities). This gap between elementary equivalence and isomorphism is one of model theory’s central concerns.

A substructure $\mathcal{A} \subseteq \mathcal{B}$ is an elementary substructure, written $\mathcal{A} \preceq \mathcal{B}$, if for every first-order formula $\varphi(\bar{x})$ and every tuple $\bar{a}$ from $A$, $\mathcal{A} \models \varphi(\bar{a})$ if and only if $\mathcal{B} \models \varphi(\bar{a})$. The Tarski-Vaught test gives a practical criterion: $\mathcal{A} \preceq \mathcal{B}$ if and only if for every formula $\exists y \, \psi(\bar{a}, y)$ with parameters from $A$ that $\mathcal{B}$ satisfies, there exists a witness $b \in A$ such that $\mathcal{B} \models \psi(\bar{a}, b)$. The diagram lemma provides another fundamental tool: the elementary diagram of $\mathcal{A}$ — the set of all first-order sentences with parameters from $A$ that $\mathcal{A}$ satisfies — characterizes elementary extensions of $\mathcal{A}$ up to isomorphism over $A$.

A theory $T$ is $\kappa$-categorical if all models of $T$ with cardinality $\kappa$ are isomorphic. For instance, the theory of dense linear orders without endpoints is $\aleph_0$-categorical (Cantor’s back-and-forth argument, 1895), but not $\kappa$-categorical for any uncountable $\kappa$. Categoricity captures the idea that a theory determines its models completely at a given cardinality. The field of model theory was shaped by Alfred Tarski, who laid its semantic foundations in the 1930s-50s with his definition of truth in a structure, and Abraham Robinson, who in the 1960s developed non-standard analysis and introduced model-theoretic algebra — demonstrating that model theory could be a powerful tool for working mathematicians, not merely a branch of logic.

Compactness and Lowenheim-Skolem Theorems

The compactness theorem is the single most important tool in model theory. Stated model-theoretically: a set of first-order sentences $\Sigma$ has a model if and only if every finite subset of $\Sigma$ has a model. Equivalently, if $\Sigma \models \varphi$, then there exists a finite $\Sigma_0 \subseteq \Sigma$ with $\Sigma_0 \models \varphi$. This was first proved by Godel in 1930 as a consequence of the completeness theorem for first-order logic, and later given a purely algebraic proof by Malcev (1936) using ultraproducts. Compactness is a finiteness principle — it says first-order logic cannot “see” genuinely infinite conditions — and this limitation is also its greatest source of power.

The classical application of compactness is the construction of non-standard models. Consider the theory of Peano arithmetic $\text{PA}$ together with the set of sentences $\{c > \bar{n} : n \in \mathbb{N}\}$, where $\bar{n}$ is the numeral for $n$ and $c$ is a new constant symbol. Every finite subset has a model (interpret $c$ as a sufficiently large standard natural number), so by compactness the whole set has a model — a model of PA containing an element greater than every standard natural number. This yields non-standard models of arithmetic, whose study reveals the limits of first-order axiomatizability: no first-order theory with an infinite model can pin down its intended model up to isomorphism. Abraham Robinson exploited the same technique to build non-standard analysis (1966): the hyperreal number field ${}^*\!\mathbb{R}$ is an elementary extension of $\mathbb{R}$ containing infinitesimals and infinite numbers, providing rigorous foundations for Leibniz-style calculus with actual infinitesimals.

The Lowenheim-Skolem theorems complement compactness by controlling the sizes of models. The downward Lowenheim-Skolem theorem states: if $\mathcal{A}$ is a structure in a countable language and $B \subseteq A$ is any subset, then there exists an elementary substructure $\mathcal{B} \preceq \mathcal{A}$ with $B \subseteq B'$ and $|B'| = |B| + \aleph_0$. In particular, every structure in a countable language has a countable elementary substructure. The upward Lowenheim-Skolem theorem states: if a theory $T$ in a language of cardinality $\kappa$ has an infinite model, then it has a model of every cardinality $\lambda \geq \kappa + \aleph_0$. Together, these theorems show that first-order logic cannot fix the cardinality of infinite models.

This leads to Skolem’s paradox (1922): the Zermelo-Fraenkel axioms of set theory, if consistent, have a countable model — yet those axioms prove the existence of uncountable sets. The resolution is that “uncountable” is relative to a model: the countable model contains a set $S$ and no bijection from $S$ to $\omega$ within the model, even though externally such a bijection exists. Skolem’s paradox vividly illustrates the gap between first-order expressibility and absolute mathematical truth, and it remains one of the most philosophically provocative consequences of the Lowenheim-Skolem theorems. Together with compactness, these results constitute the fundamental toolkit of model theory — any serious application of the subject begins from these three theorems.

Types and Saturated Models

The concept of a type is the central notion of modern model theory, introduced systematically by Tarski and later developed in depth by Morley, Shelah, and others. Let $T$ be a complete theory in a language $\mathcal{L}$, let $\mathcal{A} \models T$, and let $A \subseteq \mathcal{A}$ be a parameter set. The complete type of a tuple $\bar{a}$ over $A$, written $\text{tp}(\bar{a}/A)$, is the set of all $\mathcal{L}(A)$-formulas $\varphi(\bar{x})$ satisfied by $\bar{a}$ in $\mathcal{A}$. More abstractly, an $n$-type over $A$ is a consistent set of formulas in $n$ free variables with parameters from $A$ that is maximal (complete) with respect to $T \cup \text{Diag}(A)$. Types capture the “complete first-order description” of elements relative to a parameter set.

The set of all complete $n$-types over $A$ is denoted $S_n^T(A)$, or simply $S_n(A)$ when $T$ is understood. This set carries a natural topology — the Stone space — defined by taking basic open sets $[\varphi] = \{p \in S_n(A) : \varphi \in p\}$ for each formula $\varphi$. The Stone space $S_n(A)$ is a compact, totally disconnected Hausdorff space (a Boolean space). The topological and cardinality properties of type spaces encode deep information about the theory. A type $p \in S_n(A)$ is realized in a model $\mathcal{A}$ if some tuple $\bar{a} \in A^n$ satisfies every formula in $p$; otherwise $p$ is omitted by $\mathcal{A}$.

The omitting types theorem (Henkin, Orey; later sharpened by Vaught) states: if $T$ is a complete countable theory and $\{p_i : i \in \omega\}$ is a countable collection of non-isolated types (types not determined by a single formula), then there exists a countable model of $T$ omitting all of them simultaneously. This result has no analogue for uncountable languages and is proved by a careful Baire category argument on type space.

A model $\mathcal{A} \models T$ is $\kappa$-saturated if for every parameter set $A \subseteq \mathcal{A}$ with $|A| < \kappa$, every type in $S_1(A)$ is realized in $\mathcal{A}$. A model is saturated if it is $|A|$-saturated (saturated over sets of size equal to its own cardinality). Saturated models are the “universal” models of a theory at a given cardinality: they realize every type that could possibly be realized. If $T$ is a complete theory in a countable language, then $T$ has a saturated model of cardinality $\kappa$ for every $\kappa$ such that $\kappa^{\aleph_0} = \kappa$ (assuming GCH, this holds for all uncountable $\kappa$). A weaker notion, $\omega$-saturation, requires only that all types over finite parameter sets are realized; $\omega$-saturated models exist for every complete countable theory without any set-theoretic assumptions.

In practice, model theorists often work inside a monster model $\mathfrak{C}$ — a sufficiently large, saturated model of $T$ that serves as an ambient universe. All “small” models and parameter sets are assumed to live inside $\mathfrak{C}$. This convention, introduced by Shelah, simplifies notation considerably: types are computed inside $\mathfrak{C}$, and elementary substructures of $\mathfrak{C}$ serve as the models of $T$ under study. The monster model plays a role in model theory analogous to the role of a universal domain in algebraic geometry.

Quantifier Elimination

A theory $T$ admits quantifier elimination (QE) if every $\mathcal{L}$-formula $\varphi(\bar{x})$ is equivalent modulo $T$ to a quantifier-free formula $\psi(\bar{x})$: for all models $\mathcal{A} \models T$ and all tuples $\bar{a}$, $\mathcal{A} \models \varphi(\bar{a})$ iff $\mathcal{A} \models \psi(\bar{a})$. Quantifier elimination dramatically simplifies the analysis of definable sets: every definable set is a Boolean combination of atomic formulas, making the theory’s “geometry” directly visible.

The standard criterion for QE is the quantifier elimination test: $T$ has QE if and only if for any two models $\mathcal{A}, \mathcal{B} \models T$ and any common substructure $\mathcal{C} \subseteq \mathcal{A}, \mathcal{B}$, every existential sentence with parameters from $C$ true in $\mathcal{A}$ is also true in $\mathcal{B}$. In practice, one often uses a back-and-forth argument or shows that quantifier-free types determine complete types.

The most celebrated examples of QE are foundational to the subject. The theory DLO (dense linear orders without endpoints) has QE: every formula about a dense linear order is equivalent to a Boolean combination of inequalities $x < y$. This was established by Cantor’s back-and-forth argument, which also shows DLO is $\aleph_0$-categorical and complete. The theory ACF$_p$ of algebraically closed fields of fixed characteristic $p$ (where $p = 0$ or $p$ is prime) has QE in the language of rings. This profound result means that every first-order definable subset of $\mathbb{A}^n$ over an algebraically closed field is a constructible set — a finite Boolean combination of Zariski-closed sets. This is the model-theoretic content of Chevalley’s theorem in algebraic geometry, and it reveals a deep connection between logic and algebraic geometry.

Perhaps the most remarkable QE result is Tarski’s theorem on real-closed fields (1948): the theory RCF of real-closed fields admits quantifier elimination in the language $\{+, \cdot, 0, 1, <\}$. Since every formula over the reals is equivalent to a quantifier-free formula, the first-order theory of $(\mathbb{R}, +, \cdot, 0, 1, <)$ is decidable. Tarski’s original decision procedure had non-elementary complexity, but Collins’s cylindrical algebraic decomposition (1975) brought it down to doubly exponential, and modern algorithms approach practical usability. This result shows that, unlike arithmetic (which is undecidable by Godel’s theorem), the first-order theory of the ordered real field is tame.

A weaker property is model-completeness: $T$ is model-complete if every embedding between models of $T$ is elementary. By Robinson’s test, this is equivalent to every formula being equivalent to an existential formula modulo $T$. Model-completeness is often a stepping stone toward full QE (one enlarges the language with definable Skolem functions or constants). QE has far-reaching consequences for decidability — any theory with QE in a language with a decidable quantifier-free fragment is decidable — and connects model theory to computer algebra, real algebraic geometry, and the theory of o-minimal structures.

Stability Theory and Classification

Saharon Shelah’s classification program, initiated in the 1970s and developed across his monumental Classification Theory (1978, revised 1990), is the deepest and most far-reaching achievement of modern model theory. The program’s goal is to classify complete first-order theories according to the complexity of their class of models — to determine which theories admit a “structure theory” (a meaningful description of all models) and which are irreducibly wild.

The key dividing line is stability. A complete theory $T$ is stable if for every model $\mathcal{A} \models T$ and every parameter set $A \subseteq \mathcal{A}$, the number of complete types $|S_1(A)| \leq |A|^{|T|}$. Informally, stable theories are those where the type spaces do not explode in cardinality. The opposite — instability — manifests as the order property: a theory is unstable if and only if some formula $\varphi(x, y)$ can linearly order an infinite set of tuples. Stability comes in a hierarchy of strengths:

$\text{strongly minimal} \;\Rightarrow\; \omega\text{-stable} \;\Rightarrow\; \text{superstable} \;\Rightarrow\; \text{stable}$

A theory is $\omega$-stable if $|S_n(A)| \leq \aleph_0$ for every countable $A$; it is superstable if every type does not fork over a finite set; it is stable if the above counting condition holds. Each level of the hierarchy admits progressively stronger structure theorems.

The program’s first landmark was Morley’s categoricity theorem (1965): if a countable complete theory $T$ is categorical in some uncountable cardinal $\kappa$ (all models of cardinality $\kappa$ are isomorphic), then $T$ is categorical in every uncountable cardinal. This was the first deep result suggesting that the “tameness” of a theory’s models could be read off from cardinal-arithmetic properties. Morley’s proof introduced the notion of $\omega$-stability, which became the foundation for all later classification work. Shelah’s work vastly extended Morley’s theorem, showing that for stable theories, the number of non-isomorphic models in each uncountable cardinality is controlled and predictable.

A set $D$ definable in a model of a strongly minimal theory carries a pregeometry (matroid) structure via algebraic closure, giving rise to a dimension theory analogous to the dimension of vector spaces or transcendence degree of field extensions. Forking independence, Shelah’s model-theoretic generalization of linear independence and algebraic independence, provides a notion of “generic position” that works uniformly across all stable theories. For $p \in S(\mathcal{A})$ and $B \supseteq A$, a type $q \in S(B)$ extending $p$ is a non-forking extension if it does not “gain new information” about $B$ beyond what $p$ already encodes. Forking satisfies symmetry, transitivity, finite character, and extension — axioms that mirror the properties of independence in linear algebra and field theory.

Beyond stability, the current frontier of classification theory studies NIP (not the independence property), NTP$_2$ (not the tree property of the second kind), and other dividing lines that organize the universe of first-order theories into a hierarchy of structural complexity. NIP theories include all stable theories and all o-minimal theories (such as the real field), and they have found applications in combinatorics (via the Sauer-Shelah lemma on VC dimension) and machine learning. Geometric model theory, pioneered by Zilber, Hrushovski, and Pillay, applies the tools of stability theory and forking to problems in algebraic geometry and number theory — most famously in Hrushovski’s model-theoretic proof of the Mordell-Lang conjecture for function fields (1996). The classification program continues to be an active research area, revealing ever finer structure in the landscape of first-order theories.