Solution (source code)

= Solution

Assume every $S_n(T)$ is finite. Each of its points is isolated: choose, for every other type, a formula separating it from the given one, and conjoin the finitely many choices. Thus every finite tuple in every model has an isolated <complete type>. Moreover every <complete type> is realized in every model: its isolating formula is consistent with the <complete theory>, so the theory entails that the formula has a realization.

For clarity, here is the one-point extension argument needed for both remaining assertions. If tuples $\mathbf a$ and $\mathbf b$ in two models have the same <complete type> and $c$ is any new element in the first, let $\theta(\mathbf x,y)$ isolate $\operatorname{tp}(\mathbf a,c)$. The formula $\exists y\,\theta(\mathbf x,y)$ belongs to the type of $\mathbf a$, hence also to that of $\mathbf b$. Choose $d$ with $\theta(\mathbf b,d)$. This extends the tuple map to a <partial elementary map>. If $c$ is different from all earlier entries, the isolating type includes these disequalities, so $d$ is new as well.

Apply this argument alternately to the two enumerations of any two countable models. The resulting back-and-forth map is an isomorphism. Thus (ii) implies (i).

Choose any countable model $A$. The same back-and-forth argument, now within $A$, shows that any two tuples of the same <complete type> are related by an <automorphism of a first-order structure>. Conversely an automorphism preserves the type. Hence the orbits of $\operatorname{Aut}(A)$ on $A^n$ are exactly its complete $n$-types. There are finitely many of them for every $n$, so the automorphism group is an <oligomorphic permutation group>. Therefore \b[(ii) also implies (iii)].