Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Model Theory

Model theory is the study of the relationship between formal languages and their interpretations — between first-order theories and the structures that satisfy them. Where proof theory studies syntax (what is derivable) and set theory supplies a foundation, model theory studies semantics in its own right: which structures realize a theory, how structures relate to one another, and what the theory's class of models reveals about the theory. Its informal slogan is

This page builds on the syntax and Tarskian semantics of first-order logic and on its three pillars — completeness, compactness, and Löwenheim–Skolem — which are the everyday tools of the subject.


What is a model?

A model of a theory is a structure in which every sentence of is true — a concrete "world" that makes the axioms hold. Unpacking the two words:

  • A structure for a signature consists of a nonempty domain (universe) together with an interpretation of each symbol of : each constant symbol names an element of , each -ary function symbol denotes a function , and each -ary relation symbol denotes a relation . (This is the same notion defined in first-order-logic.md.)
  • is a model of , written , when for every sentence .

Examples: a group is a model of the group axioms; is the standard model of arithmetic; a set-with-an--relation satisfying the ZFC axioms is a model of ZFC. In the degenerate propositional case, a "model" of a formula is just a truth assignment satisfying it (see sentential-logic.md).

Two cautions about the word, both elaborated in remarks:

  • A model is itself a set-theoretic object. A structure is a set (the domain) carrying further sets (the interpreted relations and functions), so the very notion of "model" is defined inside a background set theory — the metatheory. This is why a "model of ZFC" is not circular: it is a set, living in the metatheory, that happens to satisfy the ZFC axioms taken as the object theory.
  • "Model" here is a logician's term of art, not the everyday/scientific sense of "a simplified representation." In logic a model is a full interpretation that makes a theory true, not an approximation of something.

With that fixed, model theory asks: given a theory, what do all its models look like, and how do they relate?

Structures, theories, and elementary equivalence

Recall from first-order logic that an -structure interprets the symbols of a signature in a domain , and says satisfies the sentence . Model theory starts by organizing structures by the sentences they satisfy.

  • The theory of a structure is , the set of all sentences true in .
  • Two structures are elementarily equivalent, , if — no first-order sentence distinguishes them.
  • A theory is complete if it decides every sentence ( or for all ); equivalently, all its models are elementarily equivalent. is always complete.

Isomorphism implies elementary equivalence, but not conversely — a central theme. By Löwenheim–Skolem there are countable and uncountable models of that are elementarily equivalent yet not isomorphic; likewise has nonstandard elementary-equivalent models with extra "blocks." First-order logic simply cannot see the difference.

Embeddings and elementary substructures

To compare structures one needs maps that respect the language.

  • An embedding is an injection preserving all atomic formulas (constants, functions, relations). is a substructure when the inclusion is an embedding.
  • is an elementary substructure if, for every formula and tuple from , Elementary substructure is far stronger than substructure: it requires agreement on all first-order properties, with the same parameters.

The practical test is the Tarski–Vaught criterion: is elementary iff every formula with a witness in already has a witness in . Combined with a closure argument this yields the downward Löwenheim–Skolem theorem in its sharp form: every infinite structure has an elementary substructure of size .

The compactness theorem at work

Compactness — a theory has a model iff every finite subset does — is the engine of classical model theory. A few signature consequences:

  • Nonstandard models of arithmetic. Add to a new constant with axioms . Every finite subset is satisfiable (interpret large), so by compactness the whole set has a model: a structure elementarily equivalent to containing an "infinite" element. The same move yields the hyperreals and nonstandard analysis.
  • Failure to express finiteness / well-foundedness. No first-order theory has exactly the finite models, and "is finite," "is well-ordered," "is connected," and "is torsion" are all not first-order expressible — compactness forbids it.
  • Transfer and overspill. Properties holding in arbitrarily large finite structures persist into an infinite model.

Quantifier elimination and definability

A theory has quantifier elimination (QE) if every formula is -equivalent to a quantifier-free one. QE is a powerful structural property: it makes the definable sets (those of the form ) transparent and is the usual route to proving completeness, decidability, and model completeness. Landmark examples:

  • Dense linear orders without endpoints (DLO) — the theory of — has QE and is complete; is its unique countable model (see -categoricity below).
  • Algebraically closed fields (ACF) have QE (essentially the geometric content of Chevalley's theorem: projections of constructible sets are constructible). (fixed characteristic) is complete.
  • Real closed fields (RCF) have QE in the ordered-field language — this is Tarski's theorem on the decidability of elementary real algebra and geometry. Via this result first-order Euclidean geometry is itself complete and decidable, and elementary plane geometry coincides model-theoretically with the theory of .
  • Presburger arithmetic has QE (with congruence predicates) and is decidable — unlike full arithmetic, which is not.

A structure is minimal/o-minimal when its definable subsets of the line are as simple as possible (finite/cofinite, or finite unions of points and intervals). o-minimality — exemplified by RCF and by the reals with exponentiation (Wilkie's theorem) — has become a major program with deep applications to real geometry and, via the Pila–Wilkie theorem, to number theory.

Categoricity and counting models

How many models of a given cardinality does a complete theory have? This counting problem organizes much of modern model theory.

  • A theory is -categorical if it has exactly one model of cardinality up to isomorphism. By Löwenheim–Skolem no first-order theory with an infinite model is categorical in all infinite cardinalities — categoricity is always relative to a .
  • Łoś–Vaught test: a theory with no finite models that is -categorical for some infinite is complete. (This is how DLO and are shown complete.)
  • -categorical (-categorical) theories are characterized by the Ryll-Nardzewski theorem: a complete theory is -categorical iff for each it has only finitely many formulas in variables up to equivalence — a deep link between automorphisms of the countable model and definability.
  • Morley's categoricity theorem (1965): a countable theory categorical in some uncountable cardinal is categorical in every uncountable cardinal. This astonishing dichotomy launched stability theory and earned Morley's student Shelah's vast classification program, which sorts theories by combinatorial dividing lines (stable, superstable, simple, NIP, …) measuring how wild their model classes can be.

Types and saturation

The local analogue of a theory is a type: a maximal consistent set of formulas describing a (possibly missing) tuple over a parameter set . The space of types — a compact totally disconnected space (the Stone space) — packages all the first-order behavior available at a point.

  • A type is realized in if some tuple satisfies all of it, and omitted otherwise.
  • The Omitting Types Theorem says a non-isolated (non-principal) type can be omitted by some countable model — the semantic counterpart to building models avoiding prescribed behavior.
  • A model is saturated if it realizes all types over small parameter sets — a "maximally rich" model — and prime if it elementarily embeds into every model of the theory ("minimal"). Saturated and prime models are the workhorses for analyzing a theory's whole model class.

Applications

Model-theoretic methods reach well beyond logic:

  • Algebra and number theory. The Ax–Grothendieck theorem (injective polynomial maps are surjective) falls out of compactness and transfer between and . Ax–Kochen resolves Artin's conjecture for all but finitely many primes via ultraproducts of -adic fields.
  • Diophantine geometry. Hrushovski's model-theoretic proof of the Mordell–Lang conjecture in positive characteristic, and o-minimal methods behind the André–Oort results (Pila–Zannier).
  • Nonstandard analysis. Robinson's rigorous infinitesimals via saturated nonstandard models of .
  • Geometry. The independence of the parallel postulate — proved by exhibiting a model of hyperbolic geometry inside the reals — is the historical prototype of the model method for independence, predating the ZFC results. Beyond it: Tarski's decidability of elementary geometry via RCF, o-minimality as a theory of tame geometry, and the Zilber trichotomy recovering projective geometry inside strongly minimal structures.
  • Combinatorics. Ultraproducts and stability-theoretic regularity lemmas (e.g. the model-theoretic Szemerédi regularity for stable/NIP graphs).

Summary

ConceptMeaning
Structure / modelinterpretation of a signature satisfying a theory
Elementary equivalence same first-order theory; weaker than isomorphism
Elementary substructure agrees on all formulas with parameters (Tarski–Vaught)
Compactnessfinite satisfiability ⇒ satisfiability; builds nonstandard models
Quantifier eliminationevery formula reduces to quantifier-free (ACF, RCF, DLO, Presburger)
-categoricityunique model of size ; Łoś–Vaught ⇒ completeness; Morley's theorem
Type / saturationmaximal consistent formula-set; saturated = realizes all types
o-minimality / stabilitytameness conditions classifying theories' model classes

Model theory turns the semantics of first-order logic into a structural subject in its own right: compactness and Löwenheim–Skolem manufacture exotic models on demand, while categoricity, types, and stability theory measure exactly how rigid or wild a theory's class of models can be — with payoffs reaching deep into algebra, geometry, and number theory.