= Countable saturation of a nonprincipal ultraproduct over omega
{title2=$\aleph_1\text{-saturation}$}
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 $\varphi_1,\varphi_2,\ldots$, 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\geq n\}\cap\bigcap_{j\leq n}A_j$. At coordinate $i$, choose a witness for the largest $n\leq 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.
Back to article page
