Let be a countable omega-saturated model and finite. Then is a parameter-free definable set exactly when every structure automorphism preserves it setwise. One direction is automorphism invariance of parameter-free definability. For the converse, saturation implies homogeneity and the back-and-forth method show that equal empty-set types are in the same automorphism orbit. For , if no formula in has its realization set contained in , the partial type is finitely satisfiable. Its parameters form a finite set, so saturation realizes it outside , contradicting invariance. Choose a defining neighbourhood for each and take their finite disjunction. The empty set is defined by . Setwise invariance permits automorphisms to permute points within .
Finite tuple Created 2026-10-06 Updated 2026-10-07
A finite tuple is an ordered list of finitely many entries; coordinates can repeat, and their positions matter. A tuple of length from a set is an element of the Cartesian product . The empty tuple has length zero. Finite tuples support Scott formulas in a back-and-forth method construction, where matching tuples determine a partial isomorphism of structures.
Finite-tuple homogeneity 2026-10-31
A first-order structure has finite-tuple homogeneity when any two finite tuples of the same parameter-free complete type are related by an automorphism. For countably infinite first-order structures this agrees with extension of finite partial elementary maps to automorphisms. Countable atomic models have this property by a back-and-forth method using isolating logical formulas. Uncountable atomic models can fail it.
Homogeneous model Created 2026-09-28 Updated 2026-11-05
A model is strongly -homogeneous when every partial elementary map between its subsets of size less than extends to an automorphism. Here the unqualified expression homogeneous model uses this automorphism extension convention. For finite parameter tuples it says, in particular, that equal complete types can be carried to one another by an automorphism.
A weaker local convention asks only for one-point extensions of small partial elementary maps. A -saturated model always has that local property. If its cardinality is , the back-and-forth method yields the strong version too. For example, order-preserving maps between finite subsets of the rational dense linear order without endpoints extend to automorphisms by back-and-forth.
Partial elementary map 2026-10-14
An injective map between subsets of structures is partial elementary when it preserves every first-order formula on tuples from its domain. This is stronger than a partial embedding, which only preserves quantifier-free formulas. In countable models, successive one-point extensions in both directions produce an elementary isomorphism by the back-and-forth method.
Use the back-and-forth method. Enumerate the two domains without repetitions as and . We construct a sequence of finite maps, each a partial isomorphism of structures,
starting with the empty function. Each is a bijection between finite subsets of the domains and preserves both adjacency and nonadjacency on its domain.
At a forth step, choose the first outside the current domain. List the finitely many domain vertices as . In , prescribe that the new image be adjacent to exactly when is adjacent to in . Since the image vertices are distinct, an extension axiom in supplies such a outside the entire current range. Extend by . This preserves injectivity, adjacency and nonadjacency, including the absence of loops.
At a back step, choose the first outside the current range. Apply the same argument to the inverse partial isomorphism of structures in , finding a fresh preimage with the required adjacency pattern to the current domain. Extend by this new pair. Alternate forth and back steps indefinitely.
Define
Because each finite function extends the preceding one, this is a well-defined injective function. The forth steps eventually include every in its domain, and the back steps eventually include every in its range, so is a bijection. Given any , both lie in the domain of some finite , where the edge equivalence already holds. It therefore also holds for :
Thus the two first-order structures are isomorphic. Alternating the steps is essential for surjectivity: repeatedly extending only the domain would merely construct an embedding into .
Enumerate both countable models. Build an increasing sequence of finite order-preserving partial bijections. At an even stage, take the first unmatched element of the first model. Its position relative to the finitely many already matched points determines an open interval or exterior ray in the second model. Density and absence of endpoints supply an unused point there, so the map extends.
At an odd stage perform the symmetric operation starting from the second model, extending the inverse map. Every required interval has infinitely many points, so avoiding the finitely many used values is possible. The union is a total bijection, by the alternating enumeration requirements, and it preserves and reflects order because every finite stage does. Hence it is an isomorphism of structures.
This is the back-and-forth method, proving countable categoricity of the dense-order theory.
The edge choices are understood to be independent, and is a fixed positive integer. We prove the hypergraph extension property and then show directly that it determines a unique countable hypergraph isomorphism type.
For a finite , prescribe a family . We want a new vertex such that
For any , the probability of precisely this pattern in the countable random uniform hypergraph is
Two different candidate vertices use disjoint hyperedge decisions: all the other vertices in each tested edge lie in . The successes are therefore independent random variables with the same positive probability . The probability that the first candidates all fail is . The same argument after discarding any finite initial set of candidates shows that infinitely many witnesses exist almost surely.
There are only countably many finite subsets of , and finitely many prescriptions for each. A countable union of null events is null. Consequently the random uniform hypergraph satisfies every such extension prescription simultaneously almost surely.
Now let and be two countably infinite -uniform hypergraphs with the hypergraph extension property. Enumerate their vertex sets and construct increasing finite partial hypergraph isomorphisms by the back-and-forth method. At a forward step, take the least unused vertex of . Its incident hyperedges with each -subset of the current domain specify a pattern on the matched vertices of . The hypergraph extension property supplies an unused vertex of with exactly this pattern. Adding preserves and reflects every hyperedge in the enlarged domain. At the next step, take the least unused vertex of and perform the identical construction with and interchanged.
The union of the finite maps is defined on every vertex and has every vertex in its range. It is a bijection, and each finite -set appears at some finite stage, so all hyperedges and nonedges are preserved. Thus it is a hypergraph isomorphism. Existence of at least one structure with the property follows from the probability-one construction already proved; fix one representative and call it . Therefore
The hypergraph isomorphism type does not depend on . In the case it is the Rado graph. For , the argument says that the infinitely many selected and unselected singleton vertices determine the same one-uniform structure for every .
The maximum is . We construct that many aleph-one-like linear orders, whose proper initial segments are countable, and prove that they are nonisomorphic. As usual the rational-type requirement concerns nonempty proper initial segments; the empty segment occurs in every order.
Let be the club set of nonzero limit ordinals below . For , form the order sum
Here means a new least point followed by a copy of the rational numbers; distinct blocks are disjoint, and all points of an earlier block precede every point of a later one. Every block is countable, dense and has no greatest point. Since , the full total order has neither a least nor a greatest point. It has size .
The sum is dense: within a block use density, and for points in different blocks choose a larger point in the earlier block. If is a proper initial segment and lies in block , then is contained in the union of the blocks through . There are only countably many such blocks, each countable. Thus is countable, rather than an uncountable interval in an aleph-one-dense order.
Every nonempty is dense and has no least point. If it has no greatest point either, the back-and-forth method gives : enumerate both orders, alternately include the least unused element from either enumeration in a finite partial order isomorphism, and choose its partner in the appropriate open interval. Density and absence of endpoints always supply a new partner. The union is a bijective order isomorphism. If has a greatest point, remove it, apply the same argument, and reattach it. Hence every nonempty proper initial segment is isomorphic to or .
The stationary information is recorded at the limit cuts. Write
This is a continuous increasing kappa-filtration by countable initial segments. At a limit , the complement has a least point exactly when .
Suppose is an order isomorphism. Since each filtration stage is countable, its image under and the corresponding image under are bounded in block index: the supremum of their countable collection of countable ordinals remains below . Choose so that
The set
is a club set. To see unboundedness, start above any given ordinal and recursively choose larger than every for . The supremum of the countable sequence remains below and belongs to . Closure follows because below a limit of members of , each fixed lies below one of those members.
For , continuity of the filtrations gives both inclusions needed for
The isomorphism therefore preserves whether the complementary final segment has a least point. Consequently
This club agreement of countable filtrations proves the invariant: if is stationary, the orders cannot be isomorphic.
We also construct enough pairwise different stationary encodings. For each , fix an injection , and set
For fixed , these sets partition the stationary tail . At least one is stationary: otherwise choose a club avoiding each one and intersect the countably many clubs to obtain a club avoiding the entire tail. The countable-intersection fact follows directly: above any starting point choose an increasing sequence, visiting each club infinitely often; its countable supremum belongs to every club by closure. For each let be the least such . One value occurs for uncountably many , since a countable union of countable sets is countable. For that fixed the cells are pairwise disjoint, by injectivity of . Enumerating those cells gives
a family of pairwise disjoint stationary subsets of . This is the explicit Ulam matrix on omega-one proof of disjoint stationary subsets of omega-one.
For put . If , their symmetric difference contains an entire and is stationary. The stationary encoding in an aleph-one-like dense order therefore produces pairwise nonisomorphic orders .
Finally, on a fixed carrier of size , every total order is a subset of its Cartesian square. That square has size , so there are at most possible relations. Thus
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.
Under the finite relational vocabulary hypothesis of the Ehrenfeucht-Fraïssé theorem, II wins the timed game exactly when the structures are elementarily equivalent. If II wins, then for every choice of by I, its strategy restricts to a winning strategy in . Hence the models agree on every sentence of quantifier rank at most . Every first-order sentence has finite quantifier rank, so they agree on all sentences.
Conversely, elementary equivalence gives for every . Choose a winning strategy for each , and use that strategy once I announces . Unlike the infinite game, the timed game permits the strategy to depend on the announced horizon.
The PDF does not explicitly impose finite vocabulary. If an arbitrary language and the full partial isomorphism of structures winning condition are intended, the reverse assertion is false. Here is a failure of finite-round game equivalence in infinite languages. Let be unary relational. Let
and obtain by adjoining one point satisfying every .
For any finite sublanguage, every Boolean cell of predicates has infinitely many elements in both structures. Every finite partial isomorphism of structures of these reducts can therefore be extended in either direction. Induction on formulas, or a back-and-forth method, shows their reducts are elementarily equivalent. Since every sentence uses finitely many symbols, in the whole language.
Nevertheless I wins by choosing : every point of fails some , so no response preserves all atomic formulas. Thus the printed unrestricted equivalence requires the finite-vocabulary convention, or a game which additionally restricts each play to a finite vocabulary fragment.
The theory of the random graph has the extension property: for finite disjoint vertex sets , there is a new vertex adjacent to every point of and to no point of .
Let be countable models and let be a finite partial embedding. Enumerate and . At an even stage, take the first outside the domain. Its adjacency pattern to the finite domain prescribes finite disjoint subsets of the range; the extension property in supplies a new image with exactly that pattern. At an odd stage, apply the same argument to the inverse map and the first unused . This back-and-forth method produces an increasing sequence of finite partial embeddings whose union is an isomorphism. Hence every finite partial embedding extends to an isomorphism .
Use the partial-isomorphism criterion for quantifier elimination: it is enough that every finite partial embedding between sufficiently saturated models have the one-point extension property.
Let be a finite partial order isomorphism between models of the theory of dense linear order without endpoints, and take . The finite set partitions into the points of , the intervals between consecutive elements, and the two outer rays. The order relations between and identify one of those intervals or rays. The image determines the corresponding interval or ray in . Density supplies a point there when it is bounded, and the absence of endpoints supplies one in either outer ray. Choose such a point ; then remains a partial order isomorphism.
The same argument works in the reverse direction. A back-and-forth method therefore extends finite partial order isomorphisms, making them partial elementary. The criterion proves quantifier elimination for dense linear orders without endpoints.
An atomic model is a model in which the type over the empty set of every finite tuple is isolated. Let be partial elementary and take . Choose a formula isolating . Since , elementarity gives . Any witness realizes the isolated joint type, so is partial elementary. This is the one-point extension between atomic models.
Alternately applying this extension property in the two directions to enumerations of countable atomic models constructs a back-and-forth isomorphism.
Let be a small partial embedding. To add a vertex , prescribe for its image adjacency to exactly when is adjacent to , together with inequalities excluding the existing image. Every finite part of this prescription is realized by the extension axioms of the theory of the random graph, and saturation realizes the whole type. The same argument applies in the reverse direction. A transfinite back-and-forth method therefore extends to an automorphism of . Automorphisms preserve every first-order formula, so is elementary.
Use the finite-partial-isomorphism criterion for quantifier elimination. Let and let be an isomorphism between finite suborders. For , its position relative to is one of the finitely many open intervals determined by , or one of the two exterior rays. The corresponding interval or ray determined by is nonempty because the orders are dense and have no endpoints. Choose there. Then remains a partial order isomorphism.
The same argument extends in the other direction. The back-and-forth method criterion therefore applies, proving quantifier elimination for dense linear orders without endpoints. Hence DLO eliminates quantifiers.
Every finite partial isomorphism between models of extends by one point. If the new point belongs to a class already represented in the domain, choose an unused point in the corresponding target class. Otherwise choose an unused point in the other target class. Both classes are infinite, so the choice is always possible. The back-and-forth method shows that tuples with the same quantifier-free type have the same complete type. Therefore has quantifier elimination.
In a countable first-order model, the finitely many named constants split the order into the open intervals
together with the named points. Each interval is a countable dense linear order without endpoints in its induced order. It is nonempty and infinite by density and the absence of endpoints.
Use Cantor's classification of countable dense linear orders without endpoints: each such interval is isomorphic to the rational order. It follows by a back-and-forth method extending finite increasing partial bijections alternately along enumerations of the two orders. Given two first-order models of , choose isomorphisms between their corresponding intervals and send each named point to its counterpart. Their union is an increasing bijection preserving all constants, hence an isomorphism in .
There are countable first-order models, for example any finite increasing list in the rational order. Therefore
For , the same argument is just the classification theorem for the whole order.
Use the complete theory of dense linear orders without endpoints in the first-order language . It eliminates quantifiers: existential conditions on one new point reduce to finitely many logical equality constraints and interval bounds, and density and absence of endpoints decide whether a suitable point exists. Its countably infinite first-order models are all isomorphic to the rational order by the usual back-and-forth method, extending finite order-preserving maps alternately along enumerations of the two first-order models. Thus it is -categorical.
To distinguish first-order models of size , let
with ordered sums. Both are dense without endpoints and have cardinality . The first has cofinality : countably many points lie in a bounded set of block indices and cannot be cofinal. The second has cofinality , supplied by its final rational block. Cofinality of a linear order is preserved by isomorphism, so they are not isomorphic. Therefore
For Ryll-Nardzewski, its -types are precisely the finitely many equality-and-order patterns on coordinates. Each is isolated by the conjunction specifying that pattern, agreeing with the theorem's prediction.
An atomic model is a model in which every finite tuple realizes an isolated complete type over the empty set. For a complete theory in a countable language, every countable atomic model is prime. The underlying argument is a back-and-forth method in the one-sided form needed for an embedding: enumerate the atomic model, and extend a finite partial elementary map one element at a time using an isolating formula for the enlarged tuple. The target model has the required witness because the already matched tuple has the same complete type.
Thus property (iii) implies property (iv). It need not imply pointwise definability or term-generation. The countable dense linear order without endpoints with a single named point, for example , is atomic: quantifier elimination for dense linear orders without endpoints isolates a tuple by its finite order-and-equality pattern relative to zero. But order structure automorphisms fixing zero move every nonzero rational. Such elements are not parameter-free definable, and no closed term names them. This supplies the failed implications (iii)(ii) and (iii)(i).