Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2007 / B / 7 / iii

Every automorphism preserves all logical formulas by induction on their construction, so an automorphism taking $\vec{a}$ to $\vec{b}$ necessarily gives equal partial types.

For the converse, first note that a finite first-order structure is atomic by (ii). Thus in both cases every realized finite-tuple partial type has an isolating logical formula. Suppose two finite tuples $\vec{u},\vec{v}$ have the same complete type, and choose a new element $x$ to extend the first tuple. Let $\theta (\vec{z},w)$ isolate the realized partial type of $(\vec{u},x)$. Sincelogical equality of partial types gives $\mathcal{A}\models \exists w\theta (\vec{v},w)$. Choose a witness $y$. Isolation ensures $(\vec{u},x)$ and $(\vec{v},y)$ have the same complete type. In particular, if $x$ is distinct from the entries already used, their inequality logical formulas ensure $y$ is distinct from its corresponding entries. The resulting finite map is injective and partial elementary.

Start from $\vec{a}\mapsto \vec{b}$, which is well-defined even for repeated coordinates because their logical equality patterns agree. Enumerate the carrier and extend alternately to include the next missing element in the domain and the next missing element in the range. For a range step apply the same extension argument to the inverse finite map. The union is an elementary bijection from $A$ onto itself: every finite tuple and every logical formula involving it is handled at some stage. It is therefore an automorphism taking $\vec{a}$ to $\vec{b}$. In the finite case the construction terminates once all elements have been included.

HenceCountability makes the back-and-forth numeralwise enumeration in arithmetic exhaust the entire first-order structure; it cannot simply be dropped.