= Solution
For nonempty <first-order structures> $(M_i)_{i\in I}$ in a common language and an <ultrafilter> $D$ on $I$, identify product <functions> by
$$
f\sim_D g\quad\Longleftrightarrow\quad\{i:f(i)=g(i)\}\in D.
$$
The <ultraproduct> $\prod_i M_i/D$ has these equivalence classes as elements. <Functions> are interpreted coordinatewise, and a relation holds of classes exactly when its coordinatewise truth <set> belongs to $D$. Closure under finite <intersections> makes these interpretations independent of representatives.
The <Łoś theorem> asserts
$$
\prod_i M_i/D\models\varphi([f_1],\ldots,[f_n])
\quad\Longleftrightarrow\quad
\{i:M_i\models\varphi(f_1(i),\ldots,f_n(i))\}\in D.
$$
Prove it by induction on <first-order formulas>. Atomic <first-order formulas> hold by the definitions and induction on terms. Conjunction uses <intersections>, and negation uses the fact that an <ultrafilter> contains exactly one of a <set> and its complement. For an existential <first-order formula>, a product witness gives a coordinate witness on a $D$-large <set>. Conversely, on the $D$-large <set> where a coordinate witness exists, choose one in each factor, and choose arbitrary values elsewhere. Its class is a product witness by the induction hypothesis. This is the only witness-selection step; the surrounding argument is made in a choice metatheory. The special case with all factors equal is an <ultrapower>, and constant <functions> give an <elementary embedding>.
Here is a direct <compactness theorem> proof. Suppose every finite <subset> of a theory $T$ has a model. Index factors by the finite <subsets> $i\subseteq T$, choosing $M_i\models i$. For finite $F\subseteq T$, the cone $C_F=\{i:F\subseteq i\}$ is nonempty, and $C_F\cap C_H=C_{F\cup H}$. Extend the generated proper filter to an <ultrafilter> $D$. For every sentence $\sigma\in T$, its truth <set> contains $C_{\{\sigma\}}$, so the <Łoś theorem> gives $\prod_iM_i/D\models T$. \b[Finite satisfiability therefore implies satisfiability], directly from the <ultraproduct> construction rather than from a syntactic completeness argument.
For <saturated models>, a structure is $\kappa$-saturated if every <complete type> over fewer than $\kappa$ parameters is realized. A useful concrete case is <countable saturation of a nonprincipal ultraproduct over omega>. In a <countable> language, enumerate any finitely satisfiable type over countably many parameters as $\varphi_1(x),\varphi_2(x),\ldots$, and represent its parameters by product <functions>. By the <Łoś theorem>, the <set> $A_n$ of coordinates where the first $n$ <first-order formulas> have a simultaneous witness belongs to the <nonprincipal ultrafilter> $D$. Put
$$
B_n=\{i:i\ge n\}\cap\bigcap_{j\le n}A_j.
$$
These are decreasing $D$-large <sets>. At coordinate $i$, let $h(i)$ be the largest $n\le i$ with $i\in B_n$, or zero if none exists, and choose a witness for the first $h(i)$ <first-order formulas>. For fixed $n$, every coordinate in $B_n$ has $h(i)\ge n$, so the resulting product <function> satisfies $\varphi_n$ on a $D$-large <set>. Its class realizes the whole type. Thus such an <ultraproduct> is $\aleph_1$-saturated.
There is also an existence construction at every prescribed degree $\kappa$. Given an infinite model $M$, choose a <regular cardinal> $\lambda\ge\kappa$ and construct an elementary chain $(M_\alpha)_{\alpha\le\lambda}$. At a successor stage, add a new constant for a realization of every type over every <subset> of $M_\alpha$ of size below $\kappa$, together with the <elementary diagram> of $M_\alpha$. Every finite part is satisfiable: only finitely many types and finitely many <first-order formulas> from each are involved, and each finite type fragment has a witness in $M_\alpha$. Compactness therefore supplies a simultaneous <elementary extension>. At limits take <unions>. To justify elementarity of a <union>, any existential <first-order formula> with parameters in an earlier stage has a witness in that stage whenever it has one at a later stage, by elementarity; this is the <Tarski-Vaught test>.
Any fewer-than-$\kappa$ parameters of $M_\lambda$ occur together in some $M_\alpha$, by regularity of $\lambda$. A type over them which is finitely satisfiable in $M_\lambda$ is finitely satisfiable in $M_\alpha$, again by elementarity, and was realized in $M_{\alpha+1}$. Hence \b[every infinite structure has a $\kappa$-saturated <elementary extension> for any prescribed cardinal $\kappa$.] No bound on the size of this extension is asserted; full saturation at the model's own <cardinality> has additional cardinal-arithmetic issues.
Back to article page
