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.
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.
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.
Rado graph 2026-10-14
The Rado graph is the unique countably infinite graph with the two-uniform hypergraph extension property. Equivalently, for any disjoint finite vertex sets , some new vertex is adjacent to every member of and no member of . The back-and-forth method proves uniqueness. Independent edge sampling on the natural numbers with any fixed 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.
Scott formula 2026-10-06
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.
Scott isomorphism theorem 2026-10-06
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.
Scott sentence 2026-10-06
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.