Model theory

Model theory studies mathematical structures through the first-order sentences and formulas they satisfy.

Finite model theory studies logical definability and equivalence on finite first-order structures. Unlike unrestricted model theory, first-order compactness is unavailable when models are required to be finite. Locality, bounded-variable games and descriptive characterizations of complexity classes are central tools.

Two formulas with the same free variables are asymptotically equivalent when the probability of their universal equivalence tends to one over the chosen finite-structure distribution. If a quantifier-eliminating extension theory has all its axioms of asymptotic probability one, compactness makes every formula asymptotically equivalent to a quantifier-free one: each particular equivalence follows from finitely many axioms, whose conjunction still has limiting probability one.

Extend first-order logic by iterating definable relation operators from the empty relation. If iteration reaches a fixed point, use that relation; if it enters a nontrivial cycle, the partial fixed point is the empty relation. For a fixed arity on a finite universe, a relation requires polynomially many bits and there are exponentially many states, so iteration is evaluable in PSPACE. On finite ordered structures this logic captures PSPACE.

For a relational structure, the Gaifman graph has the same universe. Two distinct elements are adjacent if they occur together in some tuple of some interpreted relation. A tuple's radius-$r$ neighbourhood is the induced structure on the union of its radius-$r$ graph balls, with the tuple marked by constants.

For a finite relational signature and quantifier rank $q$, matching the numbers of all marked radius-$3^q$ one-point neighbourhood types suffices for two finite structures to satisfy the same first-order sentences of rank at most $q$. Equivalently, a bijection can match the isomorphism types of these marked neighbourhoods point by point. On bounded-degree structures, a threshold version permits large neighbourhood-type counts to differ once both exceed a fixed bound. Long cycles of equal total size give useful exact-count applications.

A recursive presentation identifies the domain of a countable structure with a computable set, with its basic operations given by total computable functions and its basic relations decidable. In a fixed finite signature this makes evaluation of atomic formulas effective. A countable structure may have a recursive presentation of a structure only for some choices of presentation, or none at all.

A computable isomorphism is an isomorphism between presented structures whose underlying map is a total computable function. For presentations on $\mathbb{N}$, its inverse is computable too: enumerate inputs until the required output occurs. Two abstractly isomorphic structures with a recursive presentation of a structure need not admit a computable isomorphism between the chosen presentations.

A finitary algebraic theory specifies sorts, finite-arity operations and equations between terms. Its internal models can be interpreted in any category with finite products. Finitely presented set-based models generate arbitrary models under filtered colimits and determine its classifying topos.

A finitely presented model is described by finitely many generators and finitely many equations. Model homomorphisms from it commute with filtered colimits. A small skeleton of these models is equivalent to the opposite of the finite-equation part of the algebraic syntactic category.

In each round the Spoiler selects an element from either structure and the Duplicator responds in the other. The paired selected elements must preserve all atomic information and equality, giving a partial isomorphism of structures. In the infinite game the Duplicator wins by avoiding failure at every finite stage. In a timed game the Spoiler first announces the number of rounds, allowing a different response strategy for each horizon.

With $k$ moves remaining, preserve corresponding gap sizes exactly when smaller than $2^k-1$, and otherwise require both gaps to have at least that many points. One move splits a gap; $2^k-1=2(2^{k-1}-1)+1$ permits matching both smaller gaps. This strategy proves that $(\mathbb{N},<)$ and $(\mathbb{N}+\mathbb{Z},<)$ agree at every finite quantifier rank despite the second order containing points with infinitely many predecessors.

For a finite relational first-order language, with finitely many constants allowed, the Duplicator wins the $n$-round game exactly when the structures are rank-n equivalent. Game-winning implies rank equivalence in arbitrary languages; the converse needs a finiteness condition and can fail even for an infinite unary vocabulary. Over a finite relational vocabulary, winning every announced finite horizon is equivalent to elementary equivalence.

For countably many unary predicates $P_i$, let $M$ contain infinitely many copies of each finite membership pattern and let $N$ add an element satisfying all predicates. Every finite vocabulary reduct has infinitely many elements in every Boolean cell in both structures, so $M\equiv N$. The Spoiler nevertheless wins the one-round full-language game by selecting the new element, whose complete atomic pattern has no counterpart in $M$.

The theory of formally real fields consists of the field axioms and all sentences asserting that $-1$ is not a sum of $m$ squares, one for each positive integer $m$. The real closure theorem and model completeness make the Theory of real closed fields its model companion.

This first-order theory has as models the nonzero torsion-free divisible Abelian groups. Rational division equips them with the structure of vector spaces over the rational numbers. A rational divisible hull gives an algebraically prime extension of each nonzero torsion-free base, while the zero base uses a one-dimensional rational space.

Remove the nonzero-model axiom from DAG. The inclusion $\{0\}\subseteq \mathbb{Q}$ is then an inclusion of models but is not a simple closure, because $x\ne 0$ has a witness only in the larger model. The theory does not have quantifier elimination: all closed group terms are zero, so no quantifier-free sentence distinguishes the two models.

For a first-order theory $T$ and $A\models T_{\forall }$, an algebraically prime extension is a structure embedding $i:A\to P\models T$ such that every embedding $j:A\to N\models T$ factors as $j=h\circ i$ for some structure embedding $h:P\to N$. The embeddings need not be elementary or unique. A theory has algebraically prime models when every such $A$ has an extension of this kind.

Given nonempty first-order structures ${\mathcal{M}}_i$ and a proper filter on a set $F$, a reduced product identifies product functions $f,g$ when $\{i:f(i)=g(i)\}\in F$. Operations are interpreted coordinatewise, and relations hold when their coordinate truth sets belong to $F$. For an ultrafilter this is an ultraproduct. Primitive positive formulas transfer through an arbitrary proper filter, whereas logical disjunction and logical negation can fail to transfer.

Two first-order structures are elementarily equivalent when they satisfy the same first-order sentences. They need not be isomorphic or embed into one another. Every elementary embedding implies elementary equivalence of its source and target.

A monster model is a fixed sufficiently saturated and strongly homogeneous model of a complete theory, of a cardinality much larger than every parameter set under discussion.

If $\mathcal{D}=\varphi (\mathcal{U},b)$, its automorphism orbit consists of the sets $\varphi (\mathcal{U},f(b))$. If this orbit is infinite, saturation constructs $|\mathcal{U}|$ pairwise distinct conjugates, so $|O(\mathcal{D})|=|\mathcal{U}|$.

A consistent first-order theory is complete when it decides every sentence in its language.

A theory is $\kappa$-categorical when all of its models of cardinality $\kappa$ are isomorphic.

An aleph-zero-categorical theory has, up to isomorphism, exactly one countably infinite model.

For a complete theory with infinite models in a countable language, the following are equivalent: the theory is aleph-zero-categorical; every type space $S_n(T)$ is finite; and for every $n$ there are only finitely many formulas in $n$ variables modulo the theory.

Every reduct of an aleph-zero-categorical theory to a sublanguage is aleph-zero-categorical. There can only be fewer formulas in each arity, so the finite-formula characterization in the Ryll-Nardzewski theorem is preserved.

This theorem is the uncountable categoricity theorem for a categorical theory. If a countable first-order theory is categorical in one uncountable cardinal, then it is categorical in every uncountable cardinal.

Let a language partition the universe into two infinite unary predicates and include a bijection between them. Its complete theory is categorical in every infinite cardinal. The reduct forgetting the bijection is not categorical in any uncountable cardinal, because the two infinite parts can have different cardinalities.

Compactness gives a countable model elementarily equivalent to $(\mathbb{Z},+,0)$ that contains a nonzero element divisible by every positive standard integer. It is not isomorphic to $\mathbb{Z}$, so $\mathrm{Th}(\mathbb{Z},+,0)$ is not aleph-zero-categorical.

The complete theory of infinite-dimensional vector spaces over a fixed finite field is aleph-zero-categorical: every countably infinite model has countably infinite dimension and is therefore isomorphic to every other such model.

The diagram of $M$ is the set of atomic and negated atomic sentences true in the expansion by constants naming every element of $M$. Its elementary diagram contains every sentence true in that expansion. Models of these diagrams correspond respectively to embeddings and elementary embeddings of $M$.

The elementary diagram of $M$ is the set of all first-order sentences true in the expansion of $M$ by a constant symbol for each element. A model of the elementary diagram contains an elementary copy of $M$.

The method of diagrams adds the diagram or elementary diagram of a structure to a theory and applies compactness. A resulting model supplies an embedding or elementary embedding of the named structure.

A first-order structure $A$ embeds into a model of $T$ exactly when $A\models T_{\forall }$. For the nontrivial direction apply the compactness theorem to $T\cup \mathrm{Diag}(A)$. If a finite diagram conjunction were inconsistent with $T$, its universal negation after replacing the new constants by variables would belong to $T_{\forall }$ and contradict its truth in $A$.

If a type $p(x)$ over a structure $M$ is finitely satisfiable in $M$, then the elementary diagram of $M$ together with $p(c)$ is finitely satisfiable. Compactness gives an elementary extension of $M$ realizing $p$.

A first-order theory is inductive when unions of chains of its models under embeddings remain models. A theory is inductive exactly when it has an axiomatization by sentences of the form $\forall \bar{x}\exists \bar{y}\phi (\bar{x},\bar{y})$ with quantifier-free $\phi$.

A theory is model-complete when every embedding between its models is elementary. Every model-complete theory is inductive and hence admits a forall-exists axiomatization.

A model companion of $T$ is a model-complete theory $T^{\ast }$ in the same language with $T_{\forall }^{\ast }=T_{\forall }$. Equivalently each model of either theory embeds into a model of the other. Alternating these embeddings and using the elementary chain theorem proves uniqueness up to logical equivalence. A model companion need not be a syntactic extension of its original theory.

This is the complete first-order theory of real closed fields.

The theory of real closed fields is complete and model-complete. In the language of ordered rings it eliminates quantifiers; in the pure language of rings its definable order prevents quantifier elimination.

In the language of ordered rings, the Theory of real closed fields has quantifier elimination. In its pure ring reduct the order is definable by nonzero squares, so model completeness survives, although quantifier elimination does not. Keeping these two language conventions separate is essential when constructing a model companion.

A non-Archimedean real closed field contains a positive element larger than every standard integer. Compactness constructs one by adjoining a constant $c$ and the formulas $c>n$ for all natural numbers $n$.

Model completeness of real closed fields transfers positivity of a rational function from $\mathbb{R}$ to real closed extensions of $\mathbb{R}$. If the function were not a sum of squares, the Artin-Schreier ordering criterion would produce a real closure in which it is negative, giving a contradiction.

An Ehrenfeucht-Mostowski model is generated, often as a Skolem hull, by a sequence of order indiscernibles whose finite order types determine their types.

A sequence $(a_i{)}_{i\in I}$ indexed by a total order is order-indiscernible when any two increasing finite subsequences of the same length satisfy the same first-order formulas.

Let $M$ be an infinite first-order structure and $I$ a total order. After choosing a Skolem expansion of $M$, an elementary extension contains distinct elements $(a_i{)}_{i\in I}$ forming an order-indiscernible sequence in that expanded language. Their Skolem hull is an elementary substructure in the expanded language, and its reduct is a first-order model of $\mathrm{Th}(M)$. Every order automorphism of $I$ extends uniquely to a structure automorphism of the hull preserving the chosen Skolem expansion, by transporting terms in the generators.

Uniqueness need not hold among all structure automorphisms of the reduct. For an infinite structure in the pure logical equality language, take two distinct nullary Skolem function values $c_0,c_1$ in the hull. For an infinite order-indiscernible sequence, neither can equal a generator: the expanded formula $x=c_j$ would otherwise hold at every generator, contradicting their distinctness. Swapping $c_0,c_1$ fixes every generator and preserves the pure logical equality reduct, while failing to preserve the Skolem expansion. Thus the identity order automorphism already has two extensions in that reduct.

Expand an infinite first-order structure by Skolem functions, choose distinct elements $b_n$, and fix a nonprincipal ultrafilter $\mathcal{U}$ on $\mathbb{N}$. For each finite subset $F$ of the required index order, form the ultrapower over ${\mathbb{N}}^F$ using the ordered Fubini product of ultrafilters. Pullback along coordinate projections gives coherent elementary maps by the Łoś theorem. In their directed limit of elementary embeddings, the classes of the coordinate functions $\mathbf{n}\mapsto b_{n_i}$ are distinct and form an order-indiscernible sequence; every first-order formula on increasing coordinates has the same nested ultrafilter test. Their Skolem hull gives an Ehrenfeucht-Mostowski model. An index-order automorphism sends a term in the generators to the same term in the transported generators; indiscernibility makes this well defined. Uniqueness is in the specified Skolem expansion, not necessarily in its reduct. If generators must respect a definable infinite order, first produce an increasing sequence by an ultrapower of finite increasing chains.

Every first-order theory with an infinite model has models whose automorphism groups have arbitrarily large cardinality. Choose a total order with many order automorphisms and apply the Ehrenfeucht-Mostowski theorem.

A prime model of a complete theory elementarily embeds into every model of that theory.

A model is atomic when the complete type over the empty set of every finite tuple is isolated. For a complete theory in a countable language, a model is prime exactly when it is countable and atomic.

Take a countable structure with countably many independent unary predicates, every finite predicate pattern realized infinitely often, and a constant naming every element. Its complete theory has an atomic model: tuples of named elements have types isolated by equations to their names. But every infinite binary predicate pattern, together with inequalities to every named element, is consistent. There are uncountably many such one-types, so no countable omega-saturated model exists. Thus existence of a countable atomic model does not imply existence of a countable saturated one.

A countable atomic model of a complete theory elementarily embeds into every model. Enumerate it and recursively extend a finite partial elementary map; an isolating formula for the next joint type guarantees a realization in the target.

If $M,N$ are infinite atomic models of a complete theory and a finite partial elementary map sends $\bar{a}$ to $\bar{b}$, then for every $c\in M$ there is $d\in N$ extending it by $c\mapsto d$. An isolating formula for $\mathrm{tp}(\bar{a},c)$ supplies $d$. Back-and-forth therefore makes any two countable atomic models isomorphic.

A theory has quantifier elimination when every formula is equivalent modulo the theory to a quantifier-free formula.

For a binary relation with no symmetry or loop restrictions, an extension axiom demands a fresh element realizing any prescribed choices of incoming edges, outgoing edges and its own loop relative to a finite list of distinct parameters. All such axioms together eliminate quantifiers: the quantifier-free type of a parameter tuple determines which witness patterns can occur. These axioms differ from the undirected loop-free theory of the random graph.

A theory $T$ eliminates quantifiers if, whenever two models of $T$ contain isomorphic copies of the same substructure $A$, they satisfy the same formulas over $A$. Equivalently, $T\cup D(A)$ is complete for every substructure of a model of $T$.

For a first-order theory $T$, suppose every existential quantifier-free formula over a common substructure has a witness in either of two $T$-models exactly when it has one in the other. Then $T$ has quantifier elimination. One may test a single quantified variable, since elimination of these formulas inductively eliminates all quantifiers. A language with a constant avoids empty-generated-substructure and quantifier-free-sentence conventions.

If $T$ has algebraically prime models and every inclusion between models of $T$ is a simple closure, then $T$ has quantifier elimination. For a common base $A$, embed its algebraically prime extension into both models. Simple closure transfers a witness into that extension; the second embedding transfers it to the other model.

A partial embedding is an injective map between subsets of structures that preserves and reflects atomic formulas. It therefore preserves every quantifier-free formula.

The theory of algebraically closed fields of a fixed characteristic eliminates quantifiers in the language of rings. Over a parameter field $F$, the complete type of a tuple is determined by the prime ideal of polynomial relations it satisfies.

Complete $n$-types over a subfield $F$ of an algebraically closed field correspond to prime ideals of $F[X_1,\dots ,X_n]$, or equivalently to generic points of irreducible affine varieties over $F$. The Stone topology corresponds to the constructible topology: polynomial equalities and inequalities define basic clopen sets.

The theory of the random graph says that the edge relation is irreflexive and symmetric and that, for every two finite disjoint vertex sets, a new vertex is adjacent to every vertex of the first and none of the second.

Every small partial embedding of a monster random graph extends by back-and-forth to an automorphism, using saturation and the extension axioms. It is therefore elementary, and the theory of the random graph eliminates quantifiers.

For every small set $A$ in a monster random graph,Any vertex outside $A$ has infinitely many conjugates over $A$ with the same adjacency pattern.

The three-types of the random graph are determined by equality and adjacency among three variables. There is one all-equal type, six types with exactly two variables equal, and eight types with all variables distinct, for a total of fifteen.

The back-and-forth method constructs an isomorphism by alternately extending finite partial isomorphisms to include elements from each structure.

An effective back-and-forth construction alternately extends a finite partial isomorphism of structures to include the least unused domain and range elements, searching computably for a compatible extension. If extension always exists and its finite compatibility conditions are decidable, the union is a computable isomorphism. Decidable presentations of a dense linear order without endpoints provide a basic example.

A dense linear order without endpoints is a linear order in which a third point lies strictly between every two distinct points and every point has points both below and above it.

Add constants $c_0<c_1<\cdots$ to the theory of dense linear orders without endpoints. The three countable models have respectively a least upper bound for the named sequence, no upper bound, or upper bounds with no least one. The unbounded model is an atomic model; the bounded model with no least upper bound is an omega-saturated model. The remaining model omits the type $c_i<x<d$ over its least-upper-bound parameter $d$.

A complete dense linear order without endpoints with the countable chain condition for a linear order, but with no countable order-dense subset.

The assertion that there is no Suslin line, equivalently that every complete dense linear order without endpoints satisfying the interval countable chain condition is separable. A Suslin tree gives a counterexample.

The theory of dense linear orders without endpoints eliminates quantifiers. A finite partial order isomorphism extends by placing each new point in the corresponding interval or ray.

An ultraproduct identifies two sequences when they agree on a set belonging to an ultrafilter and interprets symbols coordinatewise.

An ultraproduct over a nonprincipal ultrafilter on $\omega$ realizes each countable finitely satisfiable type. For the first $n$ formulas, their coordinate simultaneous-witness set $E_n$ belongs to the ultrafilter by the Łoś theorem. Replace it by $E_n\cap [n,\infty )$ and choose at coordinate $i$ a witness to as many initial formulas as that coordinate permits. This finite number tends to infinity modulo the ultrafilter, so the resulting product class realizes every formula. More generally countably incomplete ultrafilters admit the same descending-set diagonalization. This statement does not assert saturation at every larger cardinal.

An ultrapower is an ultraproduct whose factors are all one structure $M$. Its elements are equivalence classes $[f]$ of functions $f:I\to M$, where $f\sim g$ exactly when $\{i\in I:f(i)=g(i)\}$ belongs to the chosen ultrafilter $\mathcal{U}$.

An ultralimit is the direct limit of a chain of structures formed by taking successive ultrapowers along their diagonal elementary embeddings. At limit stages use the elementary chain theorem. This is a different concept from a topological ultrafilter limit. Alternating relative ultrapower embeddings constructs isomorphic ultralimits of any two elementarily equivalent structures, without requiring the stronger single-ultrapower isomorphism theorem.

The Frayne embedding lemma embeds $B$ into an ultrapower $A_1$ of $A$. Its relative version embeds $A_1$ into an ultrapower $B_1$ of $B$, fixing the diagonal copy of $B$. Continue alternately over the previously fixed elementary substructure. After coherent identifications one has $B⪯A_1⪯B_1⪯A_2⪯B_2⪯\cdots$, while each $A_{n+1}$ is an ultrapower of $A_n$ along its diagonal map, and similarly for $B$. The two cofinal subsequences have the same elementary union. This proves the ultralimit assertion without the stronger single-ultrapower isomorphism theorem.

If $A\equiv B$, the elementary diagram of $B$ is finitely satisfiable by interpreting its finitely many named elements in $A$. Choose those finite realizations as coordinates, extend the filter of diagram cones to an ultrafilter, and use the Łoś theorem to embed $B$ elementarily into an ultrapower of $A$. If $A\prec B$, work over the named elements of $A$ and keep their coordinates constant. The resulting embedding extends the diagonal map of $A$. This relative assertion allows an alternating chain of ultrapowers to keep every previously embedded substructure fixed.

If $U$ is a kappa-complete nonprincipal ultrafilter on $\kappa$ and $|M|\ge \kappa$, then $|M^{\kappa }/U|>\kappa$. Otherwise enumerate representatives $f_{\alpha }$ for its classes and choose $g(i)\notin \{f_{\alpha }(i):\alpha <i\}$. Every tail of $\kappa$ belongs to $U$, so $g$ differs modulo $U$ from every representative. The small set is absent from a complete nonprincipal ultrafilter lemma supplies the tail property.

This theorem characterizes truth in an ultraproduct. Łoś's theorem says that a first-order formula holds in an ultraproduct exactly when it holds in a set of factors belonging to the ultrafilter.

For a family of first-order structures, take free filters on the index set as worlds, ordered by inclusion, and product sequences as parameters. Force an atom when its coordinate truth set belongs to the filter. Conjunction is local, implication and negation quantify over filter extensions, and a disjunction is forced when every extension has a further extension forcing one disjunct. Existence is witnessed by a product sequence and universality holds for all sequences at all extensions. With the axiom of choice, induction on formulas identifies forcing with membership of the classical coordinate truth set. Equivalently, every ultrafilter extension satisfies the formula in its ultraproduct. Thus the semantics validates classical logic. A local disjunction rule would fail this identification: a set and its complement can both be absent from a free filter, while their union is the whole index set.

For a prime number $p$, a nonprincipal ultrafilter on $\mathbb{N}$ givesThe Łoś theorem makes $K$ a field of characteristic $p$. For every natural number $m$, almost all factors have at least $m$ elements, so $K$ is infinite.

An elementary extension is an extension preserving all first-order truth with parameters, hence giving elementary equivalence. An extension $N\supseteq M$ is elementary when every formula with parameters from $M$ has the same truth value in both structures.

A model $N$ is $\kappa$-saturated when every complete type over a subset of size less than $\kappa$ is realized in $N$.

A model is omega-saturated when it realizes every complete finite-tuple type over any finite parameter set. Realizing all one-variable types over finite parameter sets suffices by successively adjoining coordinates. This is weaker than saturation over every countable parameter set.

For every infinite regular cardinal $\kappa$, every first-order structure has a $\kappa$-saturated elementary extension. At one stage use the compactness theorem with the elementary diagram to realize all complete types over subsets of the stage having size less than $\kappa$. There is a set of such types; finite subsets of the enlarged theory are satisfiable because their finitely many witnesses are independent. Iterate for $\kappa$ stages, taking elementary unions at limits. Regularity puts any parameter set of size less than $\kappa$ inside one stage, and its type is realized at the next one. Passing to a larger regular cardinal covers singular requested degrees of saturation as well.

In a countable language, an ultraproduct over a nonprincipal ultrafilter on $\omega$ realizes every countable finitely satisfiable type, including types over countably many parameters. Enumerate the type ${\phi }_1,{\phi }_2,\dots$, and let $A_n$ be the ultrafilter-large set of coordinates where the first $n$ first-order formulas have a simultaneous witness. Put $B_n=\{i:i\ge n\}\cap {\bigcap }_{j\le n}{A}_j$. At coordinate $i$, choose a witness for the largest $n\le i$ with $i\in B_n$, or an arbitrary element when there is none. For each fixed $n$, the resulting function satisfies the first $n$ first-order formulas on $B_n$. The Łoś theorem then realizes the entire type. Countability of the language and parameter set makes the enumeration possible.

A $\kappa$-saturated model has the one-point extension property for partial elementary maps of size below $\kappa$: transport the type of the new element through the map and realize it by saturation. This is $\kappa$-homogeneity; back-and-forth gives the corresponding automorphisms when cardinalities permit.

If an aleph-zero-homogeneous model realizes every finite type over the empty set, it is aleph-zero-saturated. Realize the joint empty-set type of the parameters and a desired element, then use homogeneity to move the realized parameter tuple to the given one.

A model $N$ of cardinality $\kappa$ is universal when every model of the same complete theory having cardinality less than $\kappa$ admits an elementary embedding into $N$.

A model $N$ of cardinality $\kappa$ is homogeneous when every partial elementary map between subsets of size less than $\kappa$ extends to an automorphism of $N$.

A universal homogeneous model realizes every type over a small parameter set. Embed a small model containing a realization into the universal model, then use homogeneity to move the embedded parameters back to the original ones.

Let $N$ be uncountable and saturated, and let a formula define an equivalence relation. If every small elementary submodel of $N$ meets every class, then there are only finitely many classes. Otherwise a small elementary submodel $M$ yields the finitely satisfiable type $\{\neg E(x,m):m\in M\}$, contradicting saturation.

The union of an elementary chain of structures has a unique induced structure, and every member of the chain is an elementary substructure of the union.

A directed system of first-order structures and coherent elementary embeddings has a direct limit into which every member embeds elementarily. Represent an element by a pair consisting of a stage and an element at that stage; identify two representatives when their images agree at a common later stage. Interpret functions and relations at a common stage. Mathematical induction on first-order formulas proves elementarity: for an existential first-order formula true at the limit, its witness and parameters occur at a common stage, and elementarity pulls truth back to the stage containing the original parameters. This generalizes the elementary chain theorem beyond linearly ordered diagrams.

The complete type of a tuple over parameters records every formula over those parameters that the tuple satisfies.

A complete type is algebraic when it contains a formula having finitely many realizations in a model of the theory. A one-element example is the type containing $x=c$ for a named constant. Such a type cannot gain infinitely many realizations in an elementarily equivalent structure. An isolated type need not be algebraic: the unique empty-set one-type in a dense linear order without endpoints is isolated by $x=x$ and has infinitely many realizations.

With its standard topology, this type space is a Stone space. The type space $S_n^M(A)$ is the set of complete $n$-types over a parameter set $A$ that are consistent with the complete theory of $M$ together with its diagram over $A$.

For a type space $S_n^M(A)$, the basic open set $[\phi ]$ consists of complete types containing the formula $\phi$. These sets are clopen, satisfy $[\phi ]\cap [\psi ]=[\phi \wedge \psi ]$, and distinguish distinct types. The compactness theorem makes this topology compact; it is Hausdorff and has a basis of clopen sets.

A complete type $p\in S_n(A)$ is isolated when some formula $\phi \in p$ belongs to no other complete type in $S_n(A)$. Equivalently, the basic open set determined by $\phi$ is the singleton $\{p\}$.

If a complete countable theory has a prime model, isolated types are dense in every finite-arity type space. Every nonempty basic open set is realized in the prime model, whose finite tuples have isolated types.