Internal Scott rank

The orbit rank of a finite tuple is the least back-and-forth level at which its class inside its own structure agrees with its class at every ordinal level. The internal Scott rank is the supremum of the successors of these tuple ranks, over all tuple lengths. Both ranks live in the universe of the structure.

The least simultaneous stabilization level is the supremum of the tuple ranks. Consequently the internal Scott rank lies between that level and its successor, and is below ω₁ for every countable structure. No countability assumption on the relational language is needed for these rank comparisons.

For a countable structure, the back-and-forth class of a tuple at any orbit-stable level, in particular at its orbit rank, is exactly its automorphism orbit.

The all-levels condition in orbitStable is essential: a single tuple's class can agree at two consecutive levels and still split later. Simultaneous stabilization at all tuple lengths, supplied by SelfStabilizesCompletely, does propagate.

The rank convention follows Cameron Freer's cameronfreer/infinitary-logic, checkpoint 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4, InfinitaryLogic/Scott/OrbitRank.lean and InfinitaryLogic/Scott/OrbitRankStabilization.lean. Here tuples of all lengths are indexed by a sigma type, and existence comes from the existing internal stabilization API.

def TauCeti.orbitStable {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : Set Ordinal.{w}

The levels at which the internal back-and-forth class of a already agrees with its class at every ordinal level.

@[simp]

theorem TauCeti.mem_orbitStable_iff {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) (α : Ordinal.{w}) : α ∈ orbitStable a ↔ ∀ (b : Fin n → M), BFEquiv α n a b → ∀ (β : Ordinal.{w}), BFEquiv β n a b

Membership in orbitStable is the all-levels upgrade property for a tuple.

theorem TauCeti.orbitStable_mono {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) {α β : Ordinal.{w}} (h : α ∈ orbitStable a) (hαβ : α ≤ β) : β ∈ orbitStable a

Orbit stability persists at every larger level.

theorem TauCeti.SelfStabilizesCompletely.mem_orbitStable {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} {α : Ordinal.{w}} (h : SelfStabilizesCompletely M α) (a : Fin n → M) : α ∈ orbitStable a

A simultaneous stabilization level is orbit-stable for every tuple.

theorem TauCeti.orbitStable_nonempty {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : (orbitStable a).Nonempty

Every tuple has an orbit-stable level, without any countability assumption.

noncomputable def TauCeti.orbitRank {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : Ordinal.{w}

The least level at which a tuple's internal back-and-forth class agrees with its class at every ordinal level.

theorem TauCeti.orbitRank_def {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : orbitRank a = sInf (orbitStable a)

The orbit rank is the infimum of the orbit-stable levels.

theorem TauCeti.orbitRank_mem_orbitStable {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : orbitRank a ∈ orbitStable a

The infimum defining the orbit rank is attained.

theorem TauCeti.orbitRank_le {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) {α : Ordinal.{w}} (h : α ∈ orbitStable a) : orbitRank a ≤ α

The orbit rank is no larger than any orbit-stable level.

theorem TauCeti.orbitRank_le_iff {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) (α : Ordinal.{w}) : orbitRank a ≤ α ↔ α ∈ orbitStable a

A level is orbit-stable exactly when it is at least the orbit rank.

theorem TauCeti.mem_orbitStable_iff_of_countable {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} [Countable M] (a : Fin n → M) (α : Ordinal.{w}) : α ∈ orbitStable a ↔ ∀ (b : Fin n → M), BFEquiv α n a b → ∃ (σ : L.Equiv M M), ⇑σ ∘ a = b

In a countable structure, a level is orbit-stable for a exactly when every tuple back-and-forth equivalent to a at that level lies in the automorphism orbit of a.

theorem TauCeti.bfEquiv_iff_exists_equiv_comp_eq_of_mem_orbitStable {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} [Countable M] {a b : Fin n → M} {α : Ordinal.{w}} (hα : α ∈ orbitStable a) : BFEquiv α n a b ↔ ∃ (σ : L.Equiv M M), ⇑σ ∘ a = b

In a countable structure, the back-and-forth class of a at an orbit-stable level is the automorphism orbit of a.

theorem TauCeti.bfEquiv_orbitRank_iff_exists_equiv_comp_eq {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} [Countable M] (a b : Fin n → M) : BFEquiv (orbitRank a) n a b ↔ ∃ (σ : L.Equiv M M), ⇑σ ∘ a = b

In a countable structure, the back-and-forth class of a at its orbit rank is the automorphism orbit of a.

theorem TauCeti.orbitRank_le_selfStabilizationOrdinal {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : orbitRank a ≤ selfStabilizationOrdinal M

Every tuple's orbit rank is bounded by the least simultaneous stabilization level.

theorem TauCeti.selfStabilizationOrdinal_eq_iSup_orbitRank {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] : selfStabilizationOrdinal M = ⨆ (p : (n : ℕ) × (Fin n → M)), orbitRank p.snd

The least simultaneous stabilization level is the supremum of the orbit ranks of all finite tuples. This holds for arbitrary structures.

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

The internal Scott rank is the supremum, over all finite tuples, of the successor of the tuple's orbit rank. In particular, even the empty structure has rank at least one.

theorem TauCeti.internalScottRank_def {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] : internalScottRank M = ⨆ (p : (n : ℕ) × (Fin n → M)), orbitRank p.snd + 1

The defining supremum for the internal Scott rank.

@[simp]

theorem TauCeti.internalScottRank_le_iff {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] (α : Ordinal.{w}) : internalScottRank M ≤ α ↔ ∀ (n : ℕ) (a : Fin n → M), orbitRank a < α

The internal Scott rank is at most α exactly when every finite tuple has orbit rank strictly below α.

theorem TauCeti.orbitRank_lt_internalScottRank {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : orbitRank a < internalScottRank M

Every tuple's orbit rank is strictly below the internal Scott rank.

theorem TauCeti.internalScottRank_eq_add_one_of_mem_orbitStable_of_orbitRank_eq {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {m : ℕ} {a₀ : Fin m → M} {α : Ordinal.{w}} (hα : ∀ (n : ℕ) (a : Fin n → M), α ∈ orbitStable a) (h₀ : orbitRank a₀ = α) : internalScottRank M = α + 1

If every tuple is orbit-stable at α and some tuple has orbit rank α, then the internal Scott rank is exactly the successor of α.

theorem TauCeti.one_le_internalScottRank {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] : 1 ≤ internalScottRank M

The internal Scott rank is at least one, including for an empty structure.

theorem TauCeti.selfStabilizationOrdinal_le_internalScottRank {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] : selfStabilizationOrdinal M ≤ internalScottRank M

The least simultaneous stabilization level is no larger than the internal Scott rank.

theorem TauCeti.internalScottRank_le_succ_selfStabilizationOrdinal {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] : internalScottRank M ≤ selfStabilizationOrdinal M + 1

The internal Scott rank is at most the successor of the least simultaneous stabilization level.

theorem TauCeti.internalScottRank_lt_omega_one {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] : internalScottRank M < Ordinal.omega 1

Every countable structure has internal Scott rank below the first uncountable ordinal. The relational language need not be countable.