Solution (source code)

= Solution

\b[Every countable structure in a countable <first-order language> has a <Scott sentence> whose countable models are precisely its <isomorphic> copies.] In particular two countable structures with the same <countable infinitary logic> sentences are <isomorphic>. Countability of both structures is essential to the back-and-forth conclusion; the sentence need not exclude uncountable models.

Let $M$ be a nonempty countable structure in a countable <first-order language>. The <countable infinitary logic> $L_{\omega_1,\omega}$ permits countable <logical conjunctions> and <logical disjunctions>, but only finite strings of quantifiers and finitely many <free variables> in each formula. We construct a <Scott formula> $\phi_{\bar a}^{\alpha}(\bar x)$ for every finite <tuple> $\bar a$ from $M$ and every countable <ordinal> $\alpha$.

At stage zero, let $\phi_{\bar a}^{0}$ be the conjunction of all <atomic formulas> true of $\bar a$ and the negations of all <atomic formulas> false of $\bar a$. Include atomic formulas involving arbitrary terms and constants, not just relation symbols applied directly to variables. There are only countably many such formulas. This complete atomic description ensures that matching <tuples> determine a <partial isomorphism of structures>.

At successors put
$$
\begin{aligned}
\phi_{\bar a}^{\alpha+1}(\bar x)=\;&\phi_{\bar a}^{\alpha}(\bar x)\\
&\land\bigwedge_{b\in M}\exists y\;\phi_{\bar a,b}^{\alpha}(\bar x,y)\\
&\land\forall y\;\bigvee_{b\in M}\phi_{\bar a,b}^{\alpha}(\bar x,y).
\end{aligned}
$$
At a nonzero limit <ordinal> $\lambda<\omega_1$, put $\phi_{\bar a}^{\lambda}=\bigwedge_{\beta<\lambda}\phi_{\bar a}^{\beta}$. All these are formulas of <countable infinitary logic>: each indexing set is countable, and the <free variables> are only the fixed finite <tuple>. Rename bound variables when necessary. <Transfinite induction> also shows $M\models\phi_{\bar a}^{\alpha}(\bar a)$.

For <tuples> of the same length within $M$, define $\bar a\equiv_\alpha\bar b$ by $M\models\phi_{\bar a}^{\alpha}(\bar b)$. Induction identifies this with the usual symmetric <back-and-forth method> equivalence: the <tuples> have the same atomic description at stage zero, and at a successor every one-element extension on either side has a matching extension at the previous stage. Thus these are decreasing <equivalence relations>, simultaneously for every finite <tuple> length.

There are only countably many pairs of finite <tuples> in $M$. A pair can cease to be equivalent at most once. The supremum of the first separation stages of all pairs that separate below $\omega_1$ is a countable <ordinal>. Choose a countable $\alpha$ at least that supremum. No pair can first separate at $\alpha+1$, so
$$
\equiv_\alpha\;=\;\equiv_{\alpha+1}\quad\text{on every }M^n.
$$
This justifies stabilization without assuming that all <tuples> stabilize at one predetermined finite stage.

Now form the following <Scott sentence>, where the case $n=0$ has no displayed variables or quantifiers:
$$
\sigma_M=\phi_{\varnothing}^{\alpha}\ \land\
\bigwedge_{n<\omega}\ \bigwedge_{\bar a\in M^n}
\forall\bar x\;\bigl(\phi_{\bar a}^{\alpha}(\bar x)\to\phi_{\bar a}^{\alpha+1}(\bar x)\bigr).
$$
It is a sentence of <countable infinitary logic>, because the family of all finite <tuples> is countable. The stabilization above and the truth of $\phi_{\varnothing}^{\alpha}$ show $M\models\sigma_M$.

Suppose a countable structure $N$ satisfies $\sigma_M$. Start with the empty matching <tuples>, and maintain $N\models\phi_{\bar a}^{\alpha}(\bar b)$. The corresponding conjunct of $\sigma_M$ upgrades this to $N\models\phi_{\bar a}^{\alpha+1}(\bar b)$. The existential conjuncts extend the match by any specified element of $M$. The universal-disjunction conjunct extends it by any specified element of $N$. The <atomic formula> information makes a new element on one side match a new element on the other, and makes repeated elements agree with their earlier matches.

Enumerate both structures and alternate these two extension steps, including the least element not yet covered at each step. The union is a <bijection> preserving and reflecting every <atomic formula>, hence an <isomorphism>; for function symbols, eventually include both a <tuple> and the value of its function term to see explicitly that the function is preserved. For finite structures the same construction stops when both are covered. Conversely every <isomorphic> copy of $M$ satisfies $\sigma_M$, since <isomorphisms> preserve formulas of <countable infinitary logic> by induction on their construction. Therefore
$$
\boxed{\text{for countable }N,\qquad N\models\sigma_M\iff N\cong M.}
$$
If countable $M,N$ have the same $L_{\omega_1,\omega}$ sentences, $N$ satisfies this <Scott sentence> of $M$ and is <isomorphic> to $M$. This proves <Scott isomorphism theorem>.