= Solution
The <Łoś theorem> states that, for every <first-order formula> $\varphi(\mathbf x)$ and product representatives $\mathbf a^1,\ldots,\mathbf a^r$,
$$
\boxed{\prod_i\mathcal A_i/\mathcal U\models\varphi([\mathbf a^1],\ldots,[\mathbf a^r])\iff\{i:\mathcal A_i\models\varphi(a_i^1,\ldots,a_i^r)\}\in\mathcal U.}
$$
It extends the defining relation-symbol rule to arbitrary <first-order formulas>, including quantified ones.
Identify the countable index set with $\mathbb N$. A <nonprincipal ultrafilter> on it contains every cofinite set. Let $p(x)$ be a type over a finite parameter set in the ultraproduct $\mathcal M$, finitely satisfiable in $\mathcal M$. Because the language and parameter set are countable, enumerate it as $\varphi_0(x),\varphi_1(x),\ldots$, with chosen product representatives for the parameters. By finite satisfiability and Łoś,
$$
X_n=\left\{i:\mathcal A_i\models\exists x\bigwedge_{j\leq n}\varphi_j(x)\right\}\in\mathcal U.
$$
Make these large sets decrease while forcing their intersection to be empty:
$$
Y_n=\{i:i\geq n\}\cap\bigcap_{k\leq n}X_k\in\mathcal U.
$$
For each index $i$, let $r(i)$ be the largest $n\leq i$ with $i\in Y_n$, if one exists. Choose $b_i\in A_i$ satisfying the first $r(i)+1$ <first-order formulas>; this is possible because $i\in X_{r(i)}$. If no such $n$ exists, choose any $b_i$.
For each fixed $n$, every $i\in Y_n$ has $r(i)\geq n$, so $b_i$ satisfies $\varphi_n$. Its coordinate truth set contains $Y_n$ and belongs to $\mathcal U$. Another use of Łoś gives $\mathcal M\models\varphi_n([\mathbf b])$ for every $n$. Thus $[\mathbf b]$ realizes the type. This proves the <countable saturation of an ultraproduct over omega>, and in particular \b[the ultraproduct is omega-saturated]. The construction chooses a finite number of requirements at each coordinate; it does not presume the whole infinite type has a witness in any factor.
Back to article page
