= Solution
Here fixed means \b[fixed setwise]: $\sigma[D]=D$ for every <structure automorphism> $\sigma$, not that each point must be fixed individually. A parameter-free <definable set> has this invariance by <automorphism invariance of parameter-free definability>.
For the converse, first establish the needed <saturation implies homogeneity> step. In a countable <omega-saturated model>, a finite <partial elementary map> can be extended to include any prescribed additional element in its domain. Transfer the element's <complete type> over the old finite domain along the map. Each finite part of this transported type has a witness because the old map is elementary; the <omega-saturated model> realizes the full transported type. The inequalities in the type maintain injectivity. Apply the same construction to the inverse map to enlarge the range. Alternating these steps through an enumeration of the countable domain is the <back-and-forth method>, giving a <structure automorphism>. In particular, any two elements with the same <complete type> over the empty set are related by a <structure automorphism>.
Assume now that $D$ is finite and invariant, and fix $a\in D$. All realizations in $A$ of $p_a=\operatorname{tp}(a/\varnothing)$ belong to $D$, by the preceding homogeneity and the invariance assumption. Suppose that no parameter-free <first-order formula> $\theta_a\in p_a$ has all its realizations in $D$. Then every finite subset of
$$
p_a(x)\cup\{x\ne d:d\in D\}
$$
is satisfiable in $A$: conjoin the finitely many <first-order formulas> from $p_a$, and use the assumed absence of a defining neighbourhood inside $D$ to find a witness outside $D$. This is a <partial type> over the finite parameter set $D$. The <omega-saturated model> would realize it by an element outside $D$ with the same empty-set type as $a$, a contradiction. Hence such a $\theta_a$ does exist.
There are only finitely many $a\in D$, so
$$
\boxed{D=\{x\in A:\mathcal A\models\bigvee_{a\in D}\theta_a(x)\}.}
$$
For $D=\varnothing$, use $x\ne x$. Thus <finite invariant sets in a countable saturated structure are definable>. Finiteness is used twice: the extra parameters form a finite set, and the final disjunction is a <first-order formula> rather than an infinite disjunction.
Back to article page
