Model theory is a branch of mathematical logic that studies the relationship between formal languages (collections of symbols and rules) and the mathematical structures that satisfy them. Where other areas of logic ask “what can we prove?”, model theory asks “what are the possible worlds in which a given set of statements is true?” It emerged in the 1940s through the independent work of Alfred Tarski in the United States, Abraham Robinson in Britain, and Anatolii Mal’tsev in Russia, who realized that theorems about logic itself could be used to prove new results in mathematics.
Languages, Structures, and Models
Model theory rests on three core concepts. A language is a set of symbols: constants (like “0”), function symbols (like “+”), and relation symbols (like “<“). These symbols combine with logical connectives (“and,” “or,” “not,” “for all,” “there exists”) to form statements. A structure is a concrete mathematical world: a nonempty set of objects (called the universe) together with an interpretation that assigns meaning to each symbol. The constant “0” gets mapped to a specific element, “+” gets mapped to an actual operation, and “<” gets mapped to an actual relation on those objects.
When a structure makes every statement in a given set of sentences true, that structure is called a model of those sentences. A set of sentences is called a theory. So model theory, at its core, studies which structures are models of which theories, and what this tells us about both.
A simple example: the theory of groups consists of sentences saying there’s an identity element, every element has an inverse, and the operation is associative. The integers under addition are one model of this theory. The symmetries of a square under composition are another. These two structures look completely different, but they both make the same sentences true. Model theory gives you tools to understand what all models of a theory share and how they can differ.
How It Differs From Proof Theory
Logic has two sides. Proof theory studies derivations: sequences of formal steps that lead from axioms to conclusions. Model theory studies truth in structures. Proof theory asks whether a statement can be derived; model theory asks which mathematical worlds make it true. The key concepts on each side mirror each other: proof versus truth, derivations versus structures, definability in a theory versus definability in a model.
These two perspectives connect through a foundational result. Gödel’s Completeness Theorem (for first-order logic) says that any consistent set of statements has a model. “Consistent” means you can’t derive a contradiction from it; “has a model” means there’s a structure making all the statements true. This bridge between syntax and semantics is what allows model theory to work: if you can’t prove a contradiction, then a mathematical world satisfying your statements actually exists.
The Compactness Theorem
The Compactness Theorem is one of the most powerful tools in model theory. It states that a set of sentences has a model if and only if every finite subset of it has a model. In the other direction: if a set of sentences has no model, then some finite piece of it already has no model.
This sounds abstract, but it lets you build surprising mathematical objects. Here’s a classic application. Start with a connected graph and write down every first-order sentence it satisfies. Then add new sentences asserting that two special points have no path of length 1 between them, no path of length 2, no path of length 3, and so on. Any finite subset of this expanded collection is still satisfiable (the original graph, being connected, can handle finitely many “no path of length n” constraints by placing the two points far apart). By compactness, the entire infinite collection has a model. That model is a graph satisfying all the same first-order properties as the original connected graph, yet it is disconnected.
This leads to a striking conclusion: the property of being a connected graph cannot be captured by any set of first-order sentences. Neither can reachability. Compactness reveals the inherent limits of first-order logic by showing that certain properties always “leak” beyond what finite statements can pin down.
The Löwenheim-Skolem Theorem
The Löwenheim-Skolem Theorem addresses size. The downward version says: if a first-order theory has a model at all, it has a countable model (one whose universe can be put in correspondence with the natural numbers). The upward version says: if a theory has an infinite model, it has models of every larger infinite size.
This has a famously paradoxical flavor. Set theory is a first-order theory that talks about uncountable sets. Yet by Löwenheim-Skolem, set theory itself has a countable model. Inside that model, there are sets the model “thinks” are uncountable, even though from the outside, the entire model is countable. This isn’t a true contradiction. It reflects the fact that “uncountable” is a relative notion: it depends on which functions are available inside the model to establish correspondences. But it shows that first-order theories can never fully control the size of their models, which is a recurring theme in model theory.
Quantifier Elimination
Some theories have a remarkable property: every statement involving “for all” or “there exists” can be rewritten as an equivalent statement without any quantifiers at all. This is called quantifier elimination, and it effectively means that every question about the theory can be reduced to a straightforward algebraic check.
The most famous example is the Tarski-Seidenberg Theorem, which shows that the theory of the real numbers (with addition, multiplication, and ordering) admits quantifier elimination. Every first-order question about real polynomials, no matter how many layers of “for all” and “there exists” it involves, can be converted into a quantifier-free formula. This makes the theory decidable: there is an algorithm that can determine the truth or falsity of any first-order statement about the reals. It also provides a general technique for problems involving polynomial inequalities, with applications ranging from optimization to control theory.
Stability and Classification
One of the deepest programs in model theory is Saharon Shelah’s classification theory, which began in the 1970s. The motivating question is: given a theory, how many different models does it have in each infinite size? Some theories are “tame,” meaning they have relatively few models and those models can be classified in a structured way. Others are “wild,” with the maximum possible number of models at every size, resisting any systematic description.
The key dividing line is stability. A stable theory is one where the space of types (roughly, the possible behaviors an element can have over a given set) doesn’t blow up in size. Stable theories have rich structural properties that make classification possible. An early landmark was Morley’s Theorem, which says that if a countable first-order theory has exactly one model (up to isomorphism) in some uncountable size, then it has exactly one model in every uncountable size. Shelah’s work massively extended this, developing a hierarchy of properties (superstability, omega-stability, simplicity) that organize first-order theories by their structural complexity. More recent work has extended these ideas to new settings, including metric structures, where analogous classification results hold.
O-Minimality and Tame Geometry
O-minimality is a branch of model theory that connects to real geometry. A structure over the real numbers is called o-minimal if every subset of the real line that you can define using the structure’s tools is just a finite union of intervals and points. This is a strong tameness condition: it rules out pathological sets like fractals or space-filling curves from being definable.
The o-minimal condition has powerful consequences. Any function you can define in an o-minimal structure is continuous and differentiable except at finitely many points. A key result, proved by Alex Wilkie, is that the real numbers with the exponential function form an o-minimal structure. This means the geometry of sets defined using polynomials and exponentials is fundamentally well-behaved, even though exponential functions can grow in wild ways.
O-minimality has found applications well beyond logic. Work by Jonathan Pila and others has used o-minimal structures to attack problems in number theory, particularly questions about rational points on curves and higher-dimensional varieties. This is one of the most active areas where model theory feeds directly into mainstream mathematics.
Applications Beyond Logic
Model theory’s power lies in its ability to transfer information between different mathematical worlds. If two structures satisfy the same first-order sentences, any result proved using only first-order tools applies to both. This lets you prove theorems about complicated objects by working with simpler ones that happen to share the same theory.
A striking example is the Ax-Kochen Theorem, a purely algebraic statement about the zeros of certain polynomials over the p-adic numbers (a number system used in number theory). The theorem was originally proved using model-theoretic techniques, not algebra. The key idea was to show that certain p-adic structures share enough first-order properties with simpler structures where the result was already known.
Model theory also interacts with algebraic geometry, combinatorics, and even computer science. Quantifier elimination provides decision procedures for broad classes of problems. The structural tools of stability theory reveal hidden regularities in mathematical objects. And the theorems about the limits of first-order logic (like the non-definability of connectedness or reachability) inform the design of query languages for databases and verification systems. What began as a study of the relationship between sentences and structures has become a versatile toolkit with reach across mathematics.