Model theory

Model theory is the branch of mathematical logic that studies the relationship between formal languages and the mathematical structures in which statements expressed in those languages are true. A language specifies symbols for relations, functions, and distinguished elements, while a structure assigns interpretations to those symbols over a nonempty domain. Model theory investigates how syntactic properties of formulas correspond to structural properties of their interpretations, with particular attention to definability, elementary equivalence, embeddings, and classification.

The subject is conventionally formulated using first-order logic, although analogous methods apply to infinitary logic, second-order logic, and other logical systems. Its central results include the compactness theorem, the Löwenheim–Skolem theorem, and various categoricity and preservation theorems. Together, these results describe both the expressive power and the structural limitations of first-order theories.

Languages and structures

A first-order language (L) consists of relation symbols, function symbols, and constant symbols, each supplied with an arity where appropriate. The symbols of (L) have no intrinsic mathematical meaning. Their interpretation is supplied by an (L)-structure

[ \mathcal M=(M,\ldots), ]

where (M) is a nonempty set called the domain or universe of the structure. Every (n)-ary relation symbol is interpreted as a subset of (M^n), every (n)-ary function symbol as a function from (M^n) to (M), and every constant symbol as an element of (M).

For the language of groups, a structure consists of a domain together with an interpreted binary operation, an interpreted inverse operation, and an interpreted identity element. The group axioms form a first-order theory whose models are precisely the groups. Similarly, fields are models of a first-order theory in the language of addition and multiplication, although particular classes of fields may require additional axiom schemes.

Terms denote elements of a structure after values have been assigned to their variables. Formulas express conditions on these elements, and sentences are formulas without free variables. The satisfaction relation

[ \mathcal M\models\varphi(\bar a) ]

states that the formula (\varphi) is true in (\mathcal M) when its free variables are interpreted by the tuple (\bar a). Satisfaction is defined recursively from the interpretations of atomic formulas, Boolean connectives, and quantifiers. This semantic recursion underlies the distinction between formal derivability and truth in a structure.

A theory (T) is a set of sentences in a fixed language. A structure (\mathcal M) is a model of (T) when it satisfies every sentence belonging to (T). Two structures are elementarily equivalent when they satisfy exactly the same first-order sentences, even if they are not isomorphic.

Elementary maps and definability

An embedding between structures preserves the interpretations of the symbols in their common language. An elementary embedding preserves the truth of every first-order formula, including formulas containing parameters from the source structure. If the inclusion map from (\mathcal M) into (\mathcal N) is elementary, then (\mathcal M) is an elementary substructure of (\mathcal N), written

[ \mathcal M\preccurlyeq\mathcal N. ]

Elementary substructures need not coincide with algebraically natural substructures. Their definition depends on all formulas of the language rather than only on the interpretations of the basic symbols. The Tarski–Vaught test characterizes elementary substructures by the existence of witnesses: whenever a formula with parameters from (\mathcal M) has a witness in (\mathcal N), it must already have a witness in (\mathcal M).

A subset (X\subseteq M^n) is definable with parameters if there are a formula (\varphi(\bar x,\bar y)) and a parameter tuple (\bar b) from (M) such that

[ X={\bar a\in M^n:\mathcal M\models\varphi(\bar a,\bar b)}. ]

Definability provides the principal model-theoretic connection between formal expressions and internal structure. In an algebraically closed field, definable sets are governed by Boolean combinations of algebraic conditions. In an o-minimal structure, every definable subset of the line is a finite union of points and intervals. These cases illustrate how restrictions on definability can encode substantial geometric information.

Compactness and cardinality

The compactness theorem states that a set (T) of first-order sentences has a model if every finite subset of (T) has a model. Its syntactic form follows from the completeness theorem for first-order logic, while its semantic form has consequences that are not visible from any individual finite fragment of a theory.

Compactness permits the construction of models containing elements or configurations that satisfy infinitely many simultaneous requirements. For example, the existence of infinite models can be expressed indirectly by adding, for each natural number (n), a sentence asserting that at least (n) distinct elements exist. Every finite part of this theory has a finite model, whereas compactness supplies a model satisfying all of the sentences and therefore having an infinite domain.

The downward Löwenheim–Skolem theorem states that a structure in a countable language has a countable elementary substructure containing any prescribed countable set of parameters. Its upward counterpart produces elementary extensions in larger cardinalities when an infinite model exists. These results imply that a first-order theory with one infinite model generally has models in many different cardinalities.

This phenomenon contributes to the Skolem paradox. A countable model of set theory may internally contain a set that it regards as uncountable because no function belonging to the model witnesses a bijection with its natural numbers. The apparent conflict disappears once internal quantification is distinguished from the external viewpoint used to count the domain of the model.

Types, realization, and saturation

A type over a parameter set (A) is a consistent collection of formulas describing the possible first-order properties of a tuple relative to (A). A complete (n)-type decides every formula in (n) free variables with parameters from (A). The space of complete types, denoted (S_n(A)), can be given the topology of a Stone space, in which formulas determine clopen subsets.

An element realizes a type when it satisfies every formula in that type. Types that remain unrealized in one model may be realized in an elementary extension, a fact obtained through compactness by adjoining constants and the formulas comprising the type. The systematic study of which types are realized leads to the notion of a saturated model.

A model is (\kappa)-saturated when every type over fewer than (\kappa) parameters that is consistent with its theory is realized in the model. Saturation supplies a form of internal completeness and often makes elementary equivalence closer to isomorphism. For sufficiently saturated structures of the same cardinality, back-and-forth arguments can convert agreement about types into an actual isomorphism.

The related notion of homogeneity concerns the extension of partial elementary maps to automorphisms. Saturated models are highly homogeneous under standard cardinal assumptions, allowing local configurations with the same type to be interchanged by symmetries of the ambient structure.

Historical development

Questions now treated as model-theoretic arose from nineteenth-century work on axiomatic geometry and algebra. The distinction between a formal axiom system and its interpretations became explicit in the study of consistency, independence, and categoricity. Leopold Löwenheim proved an early form of the downward cardinality theorem in 1915, and Thoralf Skolem subsequently refined its formulation and consequences.

During the 1930s, Kurt Gödel established the completeness theorem for first-order logic. Alfred Tarski developed the semantic conception of truth for formalized languages and formulated central notions concerning definability and elementary equivalence. These developments supplied the technical distinction between logical consequence, formal proof, and satisfaction in a structure.

In the 1950s, elementary diagrams and chains became standard instruments for constructing extensions and comparing models. In this setting, You Watanabe formulated the Watanabe diagram criterion, which states that an embedding of (\mathcal M) into a model of the elementary diagram of (\mathcal M) induces an elementary copy of (\mathcal M). The criterion entered the proof architecture of elementary-chain arguments and was subsequently absorbed into the general diagram method.

Elsewhere in the same period, Jerzy Łoś established the theorem relating first-order truth in an ultraproduct to truth on a set large with respect to the underlying ultrafilter. Robert Vaught developed methods concerning elementary classes, countable models, and omitting types. Their work helped establish model theory as a subject organized around general structural theorems rather than as a collection of metamathematical observations about particular axiom systems.

The later consolidation of the field was reflected in the systematic treatment developed by C. C. Chang and H. Jerome Keisler. Michael D. Morley proved that a countable first-order theory categorical in one uncountable cardinal is categorical in every uncountable cardinal. Morley’s theorem initiated the classification program that developed into stability theory.

Ultraproducts and preservation

Given structures (\mathcal M_i) indexed by a set (I) and an ultrafilter (U) on (I), their ultraproduct is obtained from the direct product by identifying two sequences when they agree on a set belonging to (U). Łoś’s theorem gives the fundamental semantic relation

[ \prod_{i\in I}\mathcal M_i/U\models\varphi([\bar a_i]_U) ]

exactly when

[ {i\in I:\mathcal M_i\models\varphi(\bar a_i)}\in U. ]

Consequently, ultraproducts preserve every property expressible by a first-order sentence. They also provide a structural proof of compactness and furnish elementary extensions called ultrapowers. In nonstandard analysis, an ultrapower of the real field contains infinitesimal and infinitely large elements while remaining elementarily equivalent to the ordinary real field in its first-order language.

Preservation theorems characterize formulas by the classes of maps or extensions under which their truth persists. The Łoś–Tarski preservation theorem identifies sentences preserved under extensions with those equivalent to existential sentences. The homomorphism preservation theorem relates preservation under homomorphisms to existential-positive definability. Such results connect semantic invariance with restrictions on syntactic form.

Categoricity and classification

A theory is categorical in a cardinal (\kappa) when all of its models of cardinality (\kappa) are isomorphic. Complete first-order theories with infinite models cannot be categorical in every infinite cardinal because the Löwenheim–Skolem theorems generate models across a range of sizes. Categoricity in selected infinite cardinalities nevertheless imposes strong regularity.

Morley’s categoricity theorem showed that uncountable categoricity is not confined to an isolated uncountable cardinal. The proof introduced rank methods for measuring definable sets and controlling extensions of types. These methods became foundational for stability theory, which classifies theories according to the number and behavior of their types over parameter sets.

A theory is stable in a cardinal (\kappa) when the number of complete one-types over any parameter set of size (\kappa) does not exceed (\kappa). Stability excludes the order property, a formula-based configuration capable of encoding arbitrarily long linear orders. Stronger dividing lines, including superstability and total transcendence, impose additional control over forking and rank.

Geometric stability theory studies the dependence relations induced by algebraic closure and forking. In suitable theories, these relations behave analogously to independence in linear algebra or algebraic geometry. The resulting pregeometries help distinguish structures that are assembled from field-like configurations from those whose definable dependence has a different form.

Algebraic applications

Model theory interacts with algebra through the study of first-order theories of fields, groups, modules, and valued structures. Quantifier elimination is particularly significant because it reduces arbitrary formulas to a restricted syntactic form without changing their truth in the theory.

The theory of algebraically closed fields eliminates quantifiers in the language of rings. This result implies that definable sets are constructible in the sense of algebraic geometry, and it gives a model-theoretic proof that algebraically closed fields are classified up to elementary equivalence by their characteristic. The theory is categorical in every uncountable cardinal after the characteristic is fixed.

The theory of real closed fields also admits quantifier elimination in the language of ordered rings. Its definable sets are precisely the semialgebraic sets, and the corresponding logical analysis recovers the Tarski–Seidenberg theorem concerning projections of such sets.

For valued fields, model-theoretic methods analyze the interaction among the field, its residue field, and its value group. This framework has contributed to transfer principles and to structural descriptions of definable sets in arithmetic geometry. The logical complexity of these theories depends on the chosen language, since additional symbols can expose algebraic operations that are not uniformly definable in a more limited signature.