Solution (source code)

= Solution

Here an <ultralimit> in the model-theoretic sense is a <model-theoretic ultralimit>: start with a <first-order structure>, take successive <ultrapowers> along their diagonal <elementary embeddings>, and take the <directed limit of elementary embeddings> of that chain. The <elementary chain theorem>, proved by induction on formulas after identifying the embeddings with inclusions, makes every stage elementary in the limit. This definition concerns structures, rather than the topological <ultrafilter limit>.

We first prove the needed <Frayne embedding lemma>. If $C\equiv D$, every finite subset of the <elementary diagram of a structure> $D$ can be realized in $C$: existentially quantify its finitely many named elements, and use <elementary equivalence>. Index by finite diagram fragments, choose such realizations, and extend the filter of cones requiring each diagram formula to an <ultrafilter>. For each $d\in D$, let $f_d$ give its chosen coordinate realizations, filling unspecified coordinates arbitrarily. The <Łoś theorem> shows that $d\mapsto[f_d]$ is an <elementary embedding> of $D$ into an <ultrapower> of $C$. The formulas $c_d\neq c_e$ ensure injectivity.

There is a relative version: if $C\preceq D$, keep all named elements from $C$ constant in every coordinate. Each finite diagram fragment is realizable in $C$ over those parameters by elementarity, so the resulting embedding extends the diagonal embedding of $C$ into its <ultrapower>.

Now use <alternating ultrapowers give isomorphic ultralimits>. First embed $B$ into an <ultrapower> $A_1$ of $A$. Apply the relative lemma to $B\preceq A_1$, embedding $A_1$ into an <ultrapower> $B_1$ of $B$ over its diagonal copy. Next embed $B_1$ into an <ultrapower> $A_2$ of $A_1$ over $A_1$, and continue. After coherent identifications this gives
$$
B\preceq A_1\preceq B_1\preceq A_2\preceq B_2\preceq\cdots.
$$
Each $A_{n+1}$ is an <ultrapower> of $A_n$ along its diagonal embedding, and each $B_{n+1}$ is an <ultrapower> of $B_n$ likewise. The two subsequences are cofinal in the same chain of <elementary substructures>, so their limits are the same union. Hence $\boxed{A\equiv B\Longrightarrow A_\infty\cong B_\infty}$. No isomorphism theorem for single <ultrapowers> has been assumed.