A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
A model M is κ-saturated if every type over a set of size < κ is realized in M. κ-saturated models contain 'no missing witnesses' and are highly homogeneous. Every complete theory has arbitrarily large saturated models constructed via ultraproducts. Saturated models are crucial for studying limiting behavior and appear in proofs of categoricity and stability.
You already know what a type is: a maximal consistent set of formulas in one or more free variables, describing how a hypothetical element (or tuple) behaves relative to a fixed set of parameters. You know that some types are realized (some element in the model satisfies all the formulas) and some are omitted (no element satisfies them all). The omitting types theorem tells you you can build models that deliberately leave types unrealized. Saturation is the opposite demand: a saturated model leaves *nothing* unrealized — every consistent type over a small enough parameter set must be realized by some actual element.
Formally, a model M is κ-saturated if for every set A ⊆ M of size strictly less than κ, and every type p(x) over A that is consistent with the theory of M relative to A, there is an element m ∈ M realizing p. The threshold κ controls how many parameters you are allowed to use when specifying a type. An ω-saturated model realizes all finitely-parameterized types; a (2^ω)-saturated model realizes types over any countable parameter set. The larger κ is, the harder it is to build a κ-saturated model, but the richer its internal structure.
The intuition is that a saturated model is *maximally realized* — it contains every element that could consistently exist. Think of the rational numbers as a saturated model of dense linear orders without endpoints: any consistent description of a new point (e.g., "between 1/3 and 1/2, and also between 0.4 and 0.5") is already realized by an existing rational. No matter how you try to describe a "missing" point using finitely many rational parameters, the rationals already contain one. This is ω-saturation for the theory of DLO.
Saturated models are highly homogeneous: any two realizations of the same type can be mapped to each other by an automorphism of the model. This is the key structural property. If you have a saturated model, it "looks the same from every angle" — two elements that satisfy the same formulas over any finite parameter set are indistinguishable and interchangeable. This homogeneity makes saturated models ideal for proving that certain properties are independent of the choice of element and for constructing elementary maps between structures.
The construction of saturated models typically uses ultraproducts (Łoś's theorem ensures they realize many types) or transfinite chains of elementary extensions, each new extension realizing more types. Every complete theory with an infinite model has saturated models of every sufficiently large cardinality. Saturated models serve as "canonical" representatives of their theories in proofs of categoricity (Morley's theorem), stability, and quantifier elimination — wherever you need a model rich enough to realize every consistent configuration that the theory allows.