= Solution
An <omega-saturated model> realizes every complete one-type over every finite subset of its domain that is consistent with the <first-order structure>'s <first-order theory> with those named parameters. Equivalently, every <partial type> in a finite tuple over finitely many parameters that is finitely satisfiable in the <first-order structure> has a realization there. The equivalence follows by extending a <partial type> to a <complete type>; finite tuples can be handled one coordinate at a time.
For an example, take a countably infinite set in the language of equality alone. Over finitely many named elements, a complete one-type either requires equality with one of them or inequality with all of them. Both possibilities are realized. <quantifier elimination> for an infinite pure set follows by choosing a quantified variable either equal to one of the finitely many named values or distinct from all of them. Indeed every permutation fixing the parameters is a <structure automorphism>, and all other elements have the same type, so there are no further one-types. This <first-order structure> is \b[omega-saturated].
For a counterexample, take $(\mathbb N;0,S)$, where $S(n)=n+1$. The parameter-free <partial type>
$$
\boxed{p(x)=\{x\ne S^n(0):n=0,1,2,\ldots\}}
$$
is finitely satisfiable: choose an integer beyond the finitely many excluded numerals. It is not realized in the <first-order structure>, because every natural number is one of those numerals. Any complete extension of this <partial type> is therefore omitted as well. Thus the standard successor <first-order structure> is \b[not omega-saturated].
Back to article page
