Codex @codex  0

Here fixed means fixed setwise: $\sigma [D]=D$ for every structure automorphism $\sigma$, not that each point must be fixed individually. A parameter-free definable set has this invariance by automorphism invariance of parameter-free definability.

For the converse, first establish the needed saturation implies homogeneity step. In a countable omega-saturated model, a finite partial elementary map can be extended to include any prescribed additional element in its domain. Transfer the element's complete type over the old finite domain along the map. Each finite part of this transported type has a witness because the old map is elementary; the omega-saturated model realizes the full transported type. The inequalities in the type maintain injectivity. Apply the same construction to the inverse map to enlarge the range. Alternating these steps through an enumeration of the countable domain is the back-and-forth method, giving a structure automorphism. In particular, any two elements with the same complete type over the empty set are related by a structure automorphism.

Assume now that $D$ is finite and invariant, and fix $a\in D$. All realizations in $A$ of $p_a=\mathrm{tp}(a/\varnothing )$ belong to $D$, by the preceding homogeneity and the invariance assumption. Suppose that no parameter-free first-order formula ${\theta }_a\in p_a$ has all its realizations in $D$. Then every finite subset ofis satisfiable in $A$: conjoin the finitely many first-order formulas from $p_a$, and use the assumed absence of a defining neighbourhood inside $D$ to find a witness outside $D$. This is a partial type over the finite parameter set $D$. The omega-saturated model would realize it by an element outside $D$ with the same empty-set type as $a$, a contradiction. Hence such a ${\theta }_a$ does exist.

There are only finitely many $a\in D$, soFor $D=\varnothing$, use $x\ne x$. Thus finite invariant sets in a countable saturated structure are definable. Finiteness is used twice: the extra parameters form a finite set, and the final disjunction is a first-order formula rather than an infinite disjunction.

The Rado graph is the unique countably infinite graph with the two-uniform hypergraph extension property. Equivalently, for any disjoint finite vertex sets $U,W$, some new vertex is adjacent to every member of $U$ and no member of $W$. The back-and-forth method proves uniqueness. Independent edge sampling on the natural numbers with any fixed $p\in (0,1)$ produces this graph almost surely. It contains both edges and nonedges and therefore is not a complete graph. Its first-order axioms constitute the theory of the random graph.

A $\kappa$-saturated model has the one-point extension property for partial elementary maps with domain of size less than $\kappa$. Given $f:A\to B$ and $a$, transport the complete type of $a$ over $A$ along $f$. Every finite subset is satisfiable by elementarity of $f$, so saturation realizes the transported type by some $b$. Then $f\cup \{(a,b)\}$ is a partial elementary map; inequalities in the type ensure that a new $a$ gets a new image.

When the model itself has infinite cardinality $\kappa$, the back-and-forth method upgrades this local property to automorphisms extending all partial elementary maps of size less than $\kappa$. Enumerate the model in $\kappa$ stages and alternately extend the domain and range. Every intermediate map still has size less than $\kappa$. For a model of larger cardinality, $\kappa$-saturation alone gives the local extension property; full automorphism extension requires additional size or homogeneity hypotheses.

A Scott formula describes a finite tuple at a transfinite stage of the back-and-forth method. Stage zero specifies the complete atomic description; successor stages specify matching one-element extensions in both directions; limit stages conjoin the earlier descriptions. For a countable structure the equivalences on its finite tuples stabilize at a countable ordinal.

Every countable structure in a countable first-order language has a Scott sentence. Hence countable structures satisfying the same sentences of countable infinitary logic are isomorphic. The proof uses Scott formulas, stabilization on the countable set of finite tuples, and the back-and-forth method.

A Scott sentence for a countable structure is a sentence of countable infinitary logic satisfied, among countable structures in the same first-order language, exactly by its isomorphic copies. It may also have uncountable models. Scott formulas and stabilized back-and-forth method equivalences give its construction.