Ultraproduct (${\prod }_i{M}_i/\mathcal{U}$)

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.