Limits of back-and-forth chains

Let M 0, M 1, … be countably infinite structures in a relational language and let α be a monotone sequence of ordinals such that consecutive structures are back-and-forth equivalent at depth α i + ω. Then there is a single structure on ℕ that is back-and-forth equivalent to each M i at depth α i, with no loss in the ordinal.

This is the limit step in the Harnik–Makkai construction of minimal counterexamples to Vaught's conjecture: a branch through a tree of models whose levels approximate one another ever more closely has a limit model approximating every model on the branch.

Implementation notes

The limit is assembled from finite injective tuples a k in M k, of nondecreasing lengths n k. Consecutive tuples are linked: the first n k entries of a (k + 1) are back-and-forth equivalent to a k at depth α k + 1. Since M k and M (k + 1) are equivalent at α k + 1 + n k < α k + ω, a link is found by n k forth steps from the empty tuples (TauCeti.BFEquiv.exists_bfEquiv_append). Each pair (j, x), with x in M j, is scheduled at the stage after Nat.pair j m, where x is the m-th element of M j: composing the links from j on gives an equivalence at depth α j + 1 between a j and an initial segment of the new tuple, and one more forth step finds a partner of x, appended unless it already occurs. The positions of the tuples exhaust ℕ because every M j is infinite. The limit structure on ℕ reads each relation on a list of positions from any tuple long enough to contain them; the links preserve atomic types, so the reading does not depend on the tuple. An induction on the depth γ then shows that, whenever γ ≤ α i, the tuple a i is equivalent at depth γ to the first n i positions of the limit: forth uses the scheduled partner, and back uses a link from a i to a tuple containing the given position.

Main results

• TauCeti.exists_structure_bfEquiv_of_bfEquiv_chain — the limit of a chain of countably infinite structures, as a structure on ℕ.

The form for configurations on ℕ is TauCeti.RelationalConfiguration.exists_limit_of_bfEquiv_chain.

References

• Antonio Montalbán, Computable Structure Theory: Beyond the Arithmetic, Part 2, Chapter XII, §2 (the limit model in the proof of the Harnik–Makkai theorem, there stated for a different back-and-forth hierarchy).
• Victor Harnik and Michael Makkai, A tree argument in infinitary model theory, Proc. Amer. Math. Soc. 67 (1977).

The construction

The links

The limit structure

theorem TauCeti.exists_structure_bfEquiv_of_bfEquiv_chain {L : FirstOrder.Language} [L.IsRelational] {M : ℕ → Type w} [hM : (i : ℕ) → L.Structure (M i)] [∀ (i : ℕ), Countable (M i)] [∀ (i : ℕ), Infinite (M i)] {α : ℕ → Ordinal.{o}} (hα : Monotone α) (h : ∀ (i : ℕ), BFEquiv (α i + Ordinal.omega0) 0 Fin.elim0 Fin.elim0) : ∃ (S : L.Structure ℕ), ∀ (i : ℕ), BFEquiv (α i) 0 Fin.elim0 Fin.elim0

The limit of a back-and-forth chain. Let M i be countably infinite structures and α a monotone sequence of ordinals such that M i and M (i + 1) are back-and-forth equivalent at depth α i + ω. Then some structure on ℕ is back-and-forth equivalent to every M i at depth α i.