Model theory

Model theory studies mathematical first-order structures through the first-order formulas they satisfy. A theory specifies sentences, while a model of a first-order theory gives a domain and interpretations of the nonlogical symbols making those sentences true.

For example, dense total orders without endpoints have a common complete first-order theory, although a countable such order and the real line cannot be isomorphic. The Löwenheim-Skolem theorem and compactness theorem explain why first-order truth can leave cardinality and other global structure undetermined. Quantifier elimination, complete types, and elementary embeddings provide tools for describing exactly what a theory can distinguish.

A logic or fragment has the finite model property if every satisfiable sentence has a finite model. This does not require every model to be finite, or a uniform bound on all finite model sizes.

Finite model theory studies first-order structures restricted to finite domains, and asks which properties can be expressed in specified formal languages. The restriction changes the available tools: ordinary first-order compactness does not hold when only finite models are admitted.

For example, the sentences saying there are at least $n$ distinct elements, one for every positive integer $n$, have a finite model for each finite subset but no common finite model. This is a direct failure of finite compactness. Logical games, locality, and bounded-variable fragments then compare the expressive power of formulas on finite databases and graphs, linking definability with computational complexity theory.

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.

In a torsion-free divisible Abelian group, division by a nonzero integer is unique. The rational scalar operations are therefore a definitional expansion. Formulas reduce to Boolean combinations of rational linear equations: eliminate an existential variable in a conjunction by solving any equation with nonzero coefficient; if none fixes the variable, the finitely many nontrivial disequalities exclude only finitely many choices in an infinite group. Equations with zero coefficient reduce to parameter conditions.

Thus over a finite parameter set a complete one-variable type either specifies an element of its linear span, or excludes every element of that span. An uncountable rational vector space realizes the latter type because a finite-parameter span is countable. It is consequently an omega-saturated model in the additive language.

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.

The first-order theory of a bijection $f$ with named inverse $g$ and no finite cycles has first-order models consisting of disjoint integer orbits. Atomic logical formulas reduce to $x_j=f^k(x_i)$ for integer $k$. An existential logical variable is either fixed by such a logical equality or must avoid finitely many points. This proves quantifier elimination and completeness. There is one complete one-type; the complete two-types are the integer offsets and the nonprincipal different-orbit partial type. There are countably many finite-arity partial types but countable first-order models with different numbers of orbits are not isomorphic.

In the first-order language of logical equality, assert that there are at least $n$ elements for every positive integer $n$. Eliminating one existential logical variable either substitutes a logical equality or avoids finitely many points, so this first-order theory has quantifier elimination and is complete. It is categorical in every infinite cardinal. Its complete $n$-types are the logical equality partitions of $n$ coordinates and are counted by the Bell numbers.

The complete theory of the standard successor structure is axiomatized by injectivity of $s$, $0$ outside its range, a predecessor for every nonzero element, and the sentences $s^n(x)\ne x$ for each positive integer $n$. Its models have a single distinguished one-sided chain generated by zero and any collection of two-sided integer chains. The classification of models of the successor theory proves completeness and explains why the theory is categorical at every uncountable cardinal but not at the countable cardinal.

In a model of the axioms for the theory of successor, repeatedly taking successor and predecessor partitions the domain into components. Injectivity and the predecessor axiom leave only the zero-generated one-sided chain and two-sided chains; the no-cycle axioms exclude finite components. Choosing one origin in each remaining component gives the displayed structure.

These axioms have quantifier elimination. To eliminate one existential quantification, put its quantifier-free matrix in disjunctive normal form. In a conjunction, an equality between a successor iterate of the bound variable and a parameter term fixes at most one candidate, by injectivity. Existence of the finitely many necessary predecessors excludes only finitely many initial zero iterates; the other equalities and inequalities then translate to conditions on the parameters by cancellation of successor iterates. If there is no such fixing equality, only finitely many candidates are excluded, so some point on the infinite zero chain works. Equalities between two different iterates of the same variable are false by absence of cycles. Thus the existential formula reduces to a quantifier-free formula.

Every closed quantifier-free sentence is decided by the distinct zero iterates, proving completeness. A one-variable formula over the empty set is a Boolean combination of finitely many equalities $x=s^n(0)$, modulo this theory. All points in added integer chains therefore realize the same nonisolated complete type over the empty set. At an uncountable cardinal $\kappa$ a model has exactly $\kappa$ integer components, proving categoricity there. A countable model with infinitely many integer components is an omega-saturated model because finite parameters involve only finitely many components, leaving a fresh one for every new-component type.

A first-order theory is $\kappa$-categorical when it has a model of a first-order theory of cardinality $\kappa$ and any two such models of a first-order theory are isomorphic. Existence is required, so a missing model size does not make categoricity vacuously true.

For any infinite cardinal $\kappa$, insert a dense order without endpoints of size $\kappa$ into an irrational cut of the named rationals. Compare it with an order of the same size having a dense tail above every named rational. Both models satisfy the complete named rational diagram by quantifier elimination, but only the second realizes the type of being above every named rational. This is an isomorphism invariant over the constants, even though it is an infinite type rather than one defining sentence. Thus the diagram is categorical in no cardinal with a model.

If a theory without finite models is categorical in an infinite cardinal at least the language size, it is complete. Otherwise its two consistent extensions deciding a sentence oppositely have infinite models. The Löwenheim-Skolem theorems produce models of both of the specified cardinality, contradicting their forced isomorphism. Categoricity includes existence at that cardinality, so it is not vacuous.

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 finite conjunction from the signed atomic diagram of $A$ becomes, after existentially closing its new names, a sentence in its existential theory. Joint satisfiability with $T$ therefore makes the full diagram finitely satisfiable with $T$. Compactness gives the embedding, with inequalities ensuring injectivity and signed atomic formulas ensuring both preservation and reflection of relations as required for a structure embedding. The reverse implication is preservation of existential truth under embeddings.

If $B$ satisfies the universal theory of $A$, every existential sentence true in $B$ is true in $A$, since its falsehood in $A$ would supply a universal negation. Apply the existential-theory embedding criterion to $B$ and the complete theory of $A$ to obtain $A^{\ast }$. Conversely universal truth descends to substructures. The elementarily equivalent model need not be the original structure itself.

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.

Let two first-order models satisfy a complete theory and suppose every element of the first is the value of a closed term. Send each such value to the value of the same first-order term in the second first-order model. Completeness decides all logical equality first-order sentences, making this map well-defined and injective. It also decides every logical formula with closed terms substituted, making the map elementary. Thus the first first-order model is prime.

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.

An equivalence-relation first-order structure with exactly two infinite classes, one countable and one uncountable, is atomic but lacks finite-tuple homogeneity. Its first-order theory has quantifier elimination: a new point is either assigned a previously used class or an available unused class, and can avoid finitely many forbidden points in that infinite class. Finite equality-and-equivalence patterns therefore isolate all tuple partial types. All elements have the same complete one-type, but no automorphism exchanges the two differently sized classes.

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.

Morleyization adds a predicate symbol for each first-order formula and an axiom equating that predicate symbol with its defining logical formula. Every original first-order model has a unique expansion. Translating an expanded logical formula back to the original first-order language and then using its named predicate symbol gives quantifier elimination. Completeness of the original first-order theory implies completeness of the expanded first-order theory.

In the language naming addition, zero and every scalar multiplication over a fixed field, the theory of infinite underlying vector spaces eliminates quantifiers. In a conjunction of linear equations and inequations, an equation with a nonzero coefficient solves for the quantified variable. Otherwise the variable is excluded from only finitely many values, so infinitude supplies a witness. Disjunction and induction finish elimination. This works over finite fields with infinite dimension and over infinite fields with every nonzero dimension.

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.

For a nonprincipal ultrafilter on the primes, the ultraproduct of the prime fields ${\mathbb{F}}_p$ is a field of characteristic zero. Each fixed sentence $n\cdot 1\ne 0$, $n\ge 1$, fails at only finitely many prime divisors of $n$; its cofinite truth set belongs to the ultrafilter, so Łoś theorem transfers it to the product. Every sentence eventually true in the prime fields also transfers. However, the sentence asserting that minus one is a square splits along the two infinite prime classes modulo four. Ultrafilters concentrating on these two classes yield different characteristic-zero fields satisfying the same eventual-truth theory, showing that this common theory is incomplete.

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.

Let $M$ be a countable omega-saturated model and $D\subseteq M$ finite. Then $D$ is a parameter-free definable set exactly when every structure automorphism preserves it setwise. One direction is automorphism invariance of parameter-free definability. For the converse, saturation implies homogeneity and the back-and-forth method show that equal empty-set types are in the same automorphism orbit. For $a\in D$, if no formula in $\mathrm{tp}(a)$ has its realization set contained in $D$, the partial type $\mathrm{tp}(a)\cup \{x\ne d:d\in D\}$ is finitely satisfiable. Its parameters form a finite set, so saturation realizes it outside $D$, contradicting invariance. Choose a defining neighbourhood for each $a\in D$ and take their finite disjunction. The empty set is defined by $x\ne x$. Setwise invariance permits automorphisms to permute points within $D$.