Theorem 7.1.3 in Hodges' Shorter Model Theory establishes a link between existentially closed structures, the amalgamation property, and quantifier elimination.
We're given a class K of structures that is closed under isos, and we assume that the class of substructures of things in K has the amalgamation property. We then have to show that any existential formula is equivalent to some quantifier-free formula in all structures in K.
The proof goes like this: Fix an existential formula $\phi(\bar{x})$ whose quantifiers you want to eliminate. He calls a pair $(A,\bar{a})$ /good/ if$A$ is in $K$ and $\bar{a}$ witnesses the truth of $\phi$ in $A$.
Let $\theta_{(A,\bar{a})}$ the conjunction of all the literals $\psi(\bar{x})$ such that $A \models \psi(\bar{a})$, and $\chi(\bar{x})$ be the disjunction of all the $\theta_{(A,\bar{a})}$, for $(A,\bar{a})$ a good pair.
At some point Hodges claims this: if $B$ is existentially closed in K and $B \models \chi(\bar{b})$, then there's a good pair $(A,\bar{a})$ and an isomorphism $e\colon \langle \bar{a} \rangle_A \to B$ mapping $\bar{a}$ to $\bar{b}$.
This hypothesis tells us that there's a good pair $(A,\bar{a})$ such that if $A \models \psi(\bar{a})$, then $B\models \psi(\bar{b})$ (for all literals $\psi$). But why is that enough to build the isomorphism?
I think we really want this to be an isomorphism, so that we can use the assumption that K is closed under isos later on. But it is not clear to me that we can build the iso $e$. How can we prove that?
Best Answer
Turning my comments into an answer:
When Hodges writes "an isomorphism $e\colon \langle\overline{a}\rangle_A\to B$", this is a typo. It should say either "an embedding $e\colon \langle\overline{a}\rangle_A\to B$" or "an isomorphism $e\colon \langle\overline{a}\rangle_A\to \langle\overline{b}\rangle_B$".
Indeed, since $\overline{a}$ generates $\langle \overline{a}\rangle_A$, if $\overline{b}$ fails to generate $B$, there can be no isomorphism $\langle\overline{a}\rangle_A\to B$ mapping $\overline{a}$ to $\overline{b}$.
To finish the proof, the key point is that $\overline{a}$ is a tuple from $A$ and $\overline{b}$ is a tuple from $B$ of the same length, and $\overline{a}$ and $\overline{b}$ satisfy the same literals, then there is an isomorphism $e\colon \langle\overline{a}\rangle_A\to \langle\overline{b}\rangle_B$ mapping $\overline{a}$ to $\overline{b}$ (and so $e$ can also be viewed as an embedding $\langle\overline{a}\rangle_A\to B$).
We define the isomorphism by $e(t^A(\overline{a})) = t^B(\overline{b})$ where $t(\overline{x})$ is an arbitrary term. This is well-defined, since $a'\in \langle \overline{a}\rangle_A$ if and only if there is some term $t(\overline{x})$ such that $a' = t^A(\overline{a})$, and if $t^A(\overline{a}) = s^A(\overline{a})$, then $t^B(\overline{b}) = s^B(\overline{b})$, since $\overline{a}$ and $\overline{b}$ satisfy the same literals. Similar reasoning shows that $t$ is a bijection, with inverse $e^{-1}(t^B(\overline{b})) = t^A(\overline{a})$.
For any $n$-ary function symbol $f$, we have $e(f^A(t_1^A(\overline{a}),\dots,t_n^A(\overline{a}))) = f^B(t_1^B(\overline{b}),\dots,t_n^B(\overline{b})) = f^B(e(t_1^A(\overline{a})),\dots,e(t_n^A(\overline{a})))$, so $e$ preserves $f$. And for any $n$-ary relation symbol $R$, we have $A\models R(t_1^A(\overline{a}),\dots,t_n^A(\overline{a}))$ if and only if $B\models R(t_1^B(\overline{b}),\dots,t_n^B(\overline{b}))$, since $\overline{a}$ and $\overline{b}$ satisfy the same literals. So $e$ is an isomorphism.