Internal stabilization of back-and-forth equivalence

For a fixed structure, simultaneous one-step stabilization at every tuple length implies stabilization at every later ordinal. The propagation argument is stated for tuples of two structures, so that it also serves stabilization against other structures. Every structure stabilizes, and a countable structure stabilizes below the first uncountable ordinal. The least such level is selfStabilizationOrdinal. This supplies an internal level at which characteristic formulas can be used to construct a Scott sentence.

Apart from that propagation lemma and the upgrade at limit levels of equivalence with a tuple of another structure, both tuples belong to the same structure. No countability of the language is needed: the countable set used in the bound consists of pairs of finite tuples of the structure, rather than formulas. The stabilization ordinal lives in the universe of the structure.

Main results

• bfEquiv_of_le_of_forall_add_one: between two structures, one-step stabilization at every tuple length propagates to all later levels.
• SelfStabilizesCompletely.bfEquiv_of_le: one-step stabilization propagates to all later levels.
• SelfStabilizesCompletely.bfEquiv_add_one_of_isSuccLimit: internal stabilization at α upgrades equivalence with a tuple of any structure at every limit β > α to β + 1.
• exists_selfStabilizesCompletely: every structure has a stabilizing level.
• exists_complete_self_stabilization: a countable structure has one below ω₁.
• selfStabilizationOrdinal_lt_omega_one: the least stabilizing level is below ω₁.

References

• Dana Scott, Logic with denumerably long formulas and finite strings of quantifiers, 1965.
• Cameron Freer's cameronfreer/infinitary-logic, checkpoint 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4, InfinitaryLogic/Scott/Sentence.lean and InfinitaryLogic/Scott/OrbitRankStabilization.lean, develops these internal stabilization statements. Here the unrestricted existence proof uses Mathlib's eventual constancy of ordinal-indexed antitone maps; the countable bound takes a supremum of failure witnesses.

def TauCeti.SelfStabilizesCompletely {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] (α : Ordinal.{o}) : Prop

A structure stabilizes internally at α if, simultaneously at every tuple length, back-and-forth equivalence at α is equivalent to equivalence at α + 1.

theorem TauCeti.selfStabilizesCompletely_def {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] (α : Ordinal.{o}) : SelfStabilizesCompletely M α ↔ ∀ (n : ℕ) (a b : Fin n → M), BFEquiv α n a b ↔ BFEquiv (α + 1) n a b

Internal stabilization is simultaneous one-step stabilization at all tuple lengths.

theorem TauCeti.bfEquiv_of_le_of_forall_add_one {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {α β : Ordinal.{o}} (h : ∀ (n : ℕ) (a : Fin n → M) (b : Fin n → N), BFEquiv α n a b → BFEquiv (α + 1) n a b) (hαβ : α ≤ β) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (hab : BFEquiv α n a b) : BFEquiv β n a b

If, between two fixed structures, back-and-forth equivalence at α upgrades to α + 1 for tuples of every length, then equivalence at α persists at every later level.

theorem TauCeti.SelfStabilizesCompletely.bfEquiv_of_le {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {α β : Ordinal.{o}} (h : SelfStabilizesCompletely M α) (hαβ : α ≤ β) {n : ℕ} {a b : Fin n → M} (hab : BFEquiv α n a b) : BFEquiv β n a b

Once all tuple lengths stabilize, equivalence at that level persists at every later level.

theorem TauCeti.SelfStabilizesCompletely.bfEquiv_iff {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {α β : Ordinal.{o}} (h : SelfStabilizesCompletely M α) (hαβ : α ≤ β) {n : ℕ} {a b : Fin n → M} : BFEquiv β n a b ↔ BFEquiv α n a b

At every level above a stabilizing level, the internal equivalence relations agree.

theorem TauCeti.SelfStabilizesCompletely.mono {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {α β : Ordinal.{o}} (h : SelfStabilizesCompletely M α) (hαβ : α ≤ β) : SelfStabilizesCompletely M β

Every level above a stabilizing level is itself stabilizing.

theorem TauCeti.SelfStabilizesCompletely.bfEquiv_of_bfEquiv_of_le {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {α : Ordinal.{o}} (h : SelfStabilizesCompletely M α) {n : ℕ} {u w : Fin n → M} {v : Fin n → N} {δ : Ordinal.{o}} (hαδ : α ≤ δ) (huv : BFEquiv α n u v) (hwv : BFEquiv δ n w v) : BFEquiv δ n u v

In a structure stabilizing internally at α, a tuple α-equivalent to an outside tuple v is equivalent to v at every level δ ≥ α at which some tuple of the structure is.

theorem TauCeti.SelfStabilizesCompletely.bfEquiv_add_one_of_isSuccLimit {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {α : Ordinal.{o}} (h : SelfStabilizesCompletely M α) {β : Ordinal.{o}} (hβ : Order.IsSuccLimit β) (hαβ : α < β) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (hab : BFEquiv β n a b) : BFEquiv (β + 1) n a b

Internal stabilization gives external stabilization at limits. If M stabilizes internally at α, then at every limit level β > α, back-and-forth equivalence at β between a tuple of M and a tuple of any structure N upgrades to β + 1.

theorem TauCeti.exists_selfStabilizesCompletely {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] : ∃ (α : Ordinal.{w}), SelfStabilizesCompletely M α

Every structure stabilizes at some ordinal in its own universe, without countability assumptions on either the structure or its relational language.

theorem TauCeti.exists_complete_self_stabilization {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] [Countable M] : ∃ α < Ordinal.omega 1, SelfStabilizesCompletely M α

A countable structure stabilizes below ω₁. Only its tuples are counted; the language may be uncountable.

noncomputable def TauCeti.selfStabilizationOrdinal {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] : Ordinal.{w}

The least ordinal, in the universe of the structure, at which all its finite tuples simultaneously stabilize internally.

theorem TauCeti.selfStabilizationOrdinal_def {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] : selfStabilizationOrdinal M = sInf {α : Ordinal.{w} | SelfStabilizesCompletely M α}

The least internal stabilization ordinal is the infimum of the stabilizing levels.

@[simp]

theorem TauCeti.selfStabilizesCompletely_selfStabilizationOrdinal {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] : SelfStabilizesCompletely M (selfStabilizationOrdinal M)

The infimum defining the least internal stabilization ordinal is attained.

theorem TauCeti.selfStabilizationOrdinal_le {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] {α : Ordinal.{w}} (h : SelfStabilizesCompletely M α) : selfStabilizationOrdinal M ≤ α

The least internal stabilization ordinal is no larger than any stabilizing level.

theorem TauCeti.selfStabilizationOrdinal_le_iff {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] {α : Ordinal.{w}} : selfStabilizationOrdinal M ≤ α ↔ SelfStabilizesCompletely M α

A level stabilizes internally exactly when it is above the least stabilizing level.

theorem TauCeti.selfStabilizationOrdinal_lt_omega_one {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] [Countable M] : selfStabilizationOrdinal M < Ordinal.omega 1

The least internal stabilization ordinal of a countable structure is countable.