= Solution
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)$. Since
$$
\mathcal A\models\exists w\,\theta(\vec u,w),
$$
<logical 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.
Hence
$$
\boxed{\operatorname{tp}(\vec a)=\operatorname{tp}(\vec b)
\iff\exists\pi\in\operatorname{Aut}(\mathcal A),\ \pi(\vec a)=\vec b.}
$$
Countability makes the back-and-forth <numeralwise enumeration in arithmetic> exhaust the entire <first-order structure>; it cannot simply be dropped.
Back to article page
