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 be a nonempty countable structure in a countable first-order language. The countable infinitary logic 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 for every finite tuple from and every countable ordinal .
At stage zero, let be the conjunction of all atomic formulas true of and the negations of all atomic formulas false of . 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
At a nonzero limit ordinal , put . 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 .
For tuples of the same length within , define by . 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 . A pair can cease to be equivalent at most once. The supremum of the first separation stages of all pairs that separate below is a countable ordinal. Choose a countable at least that supremum. No pair can first separate at , so
This justifies stabilization without assuming that all tuples stabilize at one predetermined finite stage.
Now form the following Scott sentence, where the case has no displayed variables or quantifiers:
It is a sentence of countable infinitary logic, because the family of all finite tuples is countable. The stabilization above and the truth of show .
Suppose a countable structure satisfies . Start with the empty matching tuples, and maintain . The corresponding conjunct of upgrades this to . The existential conjuncts extend the match by any specified element of . The universal-disjunction conjunct extends it by any specified element of . 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 satisfies , since isomorphisms preserve formulas of countable infinitary logic by induction on their construction. Therefore
If countable have the same sentences, satisfies this Scott sentence of and is isomorphic to . This proves Scott isomorphism theorem.