Orbit ranks of finite tuples and the internal Scott rank

The internal finite-tuple invariant of a single structure M: for a tuple a : Fin n → M, its orbit rank orbitRank a is the least ordinal α such that every tuple b of M that is back-and-forth equivalent to a at level α is equivalent to a at every level. For countable M that is exactly "the level-α class of a is its automorphism orbit" (bfEquiv_orbitRank_iff_exists_automorphism). The internal Scott rank internalScottRank M = ⨆ (orbitRank a + 1) is the SR(M) convention.

Convention, and a source discrepancy. Marker (Lectures on Infinitary Model Theory, 2016, Definition 2.2.4) prints the one-step condition "a ∼_α b ⇒ a ∼_{α+1} b". That condition does not define orbits: a class can pause for one level and split later (the graph K₂ ⊔ K₃: all vertices are equivalent at levels 0 and 1, a K₂-vertex and a K₃-vertex are not automorphic and separate at level 2; see scripts/check_orbit_rank_regressions.lean). The production definition here is the all-levels form, as in the Scott-rank survey (arXiv:2011.03923, Definition 2.6), which is what the orbit reading requires.

This is deliberately distinct from elementRank/scottRank (Scott/Rank.lean), which compare a singleton of M with tuples of arbitrary countable structures. No comparison between the two conventions is supplied here.

Contents:

• orbitStable a: the levels at which the orbit of a has stabilized (all-levels form); upward closed; nonempty for every structure (orbitStable_nonempty, via the set-sized stabilization ordinal of M with itself), so orbitRank is never an infimum over an empty set.
• orbitRank, its membership and least-element lemmas; for countable M, equivalence at the orbit rank is equivalent to an automorphism carrying the tuple.
• internalScottRank: the supremum API (internalScottRank_le, cofinal lower bound, internalScottRank_eq_iff) and, on top of it, the semantic exact-rank criterion: internalScottRank_le_of_orbits_determined (every tuple's orbit is determined at some level below α) and le_internalScottRank_of_not_automorphic (below every β < α some β-equivalent tuples are not automorphic), assembled in internalScottRank_eq_of_orbits.
• Transport of BFEquiv along isomorphisms (BFEquiv.map_equiv) and isomorphism invariance of both ranks.
• exists_automorphism_of_bfEquiv_all: for countable M, two tuples equivalent at every level are carried to each other by an automorphism (pointed Karp). The proof builds a pointed potential isomorphism and reads the tuple off the graph specification of the countable back-and-forth construction through the equality atoms.
• Infinite pure sets: every orbit rank is 0 and the internal Scott rank is 1.

Ordinals live in Ordinal.{w} for M : Type w, the universe the stabilization argument uses. No computability or admissibility enters.

Transport along isomorphisms

theorem FirstOrder.Language.SameAtomicType.map_equiv {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {M' : Type u_1} {N' : Type u_2} [L.Structure M'] [L.Structure N'] (e : L.Equiv M M') (e' : L.Equiv N N') {n : ℕ} {a : Fin n → M} {b : Fin n → N} : SameAtomicType (⇑e ∘ a) (⇑e' ∘ b) ↔ SameAtomicType a b

Atomic types are transported along isomorphisms.

theorem FirstOrder.Language.BFEquiv.map_equiv {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {M' : Type w} {N' : Type w'} [L.Structure M'] [L.Structure N'] (e : L.Equiv M M') (e' : L.Equiv N N') (α : Ordinal.{u_1}) {n : ℕ} {a : Fin n → M} {b : Fin n → N} : BFEquiv α n (⇑e ∘ a) (⇑e' ∘ b) ↔ BFEquiv α n a b

Back-and-forth equivalence is transported along isomorphisms of both sides.

Orbit rank

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

The levels at which the orbit of a inside M has stabilized: every b in M equivalent to a at level α is equivalent to a at every level.

Equations

• FirstOrder.Language.orbitStable a = {α : Ordinal.{?u.1} | ∀ (b : Fin n → M), FirstOrder.Language.BFEquiv α n a b → ∀ (γ : Ordinal.{?u.1}), FirstOrder.Language.BFEquiv γ n a b}

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

The stabilization set is never empty: the set-sized stabilization ordinal of M with itself belongs to it. No countability of M is needed.

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

Stabilization persists upward.

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

Orbit rank of a tuple: the least level α such that every tuple of M equivalent to a at level α is equivalent to a at every level. For countable M over a relational language, that class is the automorphism orbit of a (bfEquiv_orbitRank_iff_exists_automorphism); in general it is the all-levels class.

Equations

• FirstOrder.Language.orbitRank a = sInf (FirstOrder.Language.orbitStable a)

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

theorem FirstOrder.Language.bfEquiv_all_of_bfEquiv_orbitRank {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {a b : Fin n → M} (h : BFEquiv (orbitRank a) n a b) (γ : Ordinal.{w}) : BFEquiv γ n a b

The defining property at the orbit rank: equivalence there is equivalence at every level.

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

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

theorem FirstOrder.Language.orbitRank_elim0 {L : Language} {M : Type w} [L.Structure M] : orbitRank Fin.elim0 = 0

The empty tuple has orbit rank 0, in any carrier including the empty one.

theorem FirstOrder.Language.orbitRank_of_length_zero {L : Language} {M : Type w} [L.Structure M] {m : ℕ} (hm : m = 0) (t : Fin m → M) : orbitRank t = 0

A tuple of length 0 has orbit rank 0, for a length given by a count that is not syntactically 0.

theorem FirstOrder.Language.exists_not_all_of_lt_orbitRank {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {a : Fin n → M} {β : Ordinal.{w}} (h : β < orbitRank a) : ∃ (b : Fin n → M), BFEquiv β n a b ∧ ¬∀ (γ : Ordinal.{w}), BFEquiv γ n a b

Below the orbit rank, stabilization fails: some b is equivalent at that level but not at every level.

theorem FirstOrder.Language.bfEquiv_all_of_automorphism {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {a b : Fin n → M} (e : L.Equiv M M) (he : ⇑e ∘ a = b) (γ : Ordinal.{w}) : BFEquiv γ n a b

Automorphic tuples are equivalent at every level.

theorem FirstOrder.Language.orbitRank_map_equiv {L : Language} {M : Type w} [L.Structure M] {M' : Type w} [L.Structure M'] (e : L.Equiv M M') {n : ℕ} (a : Fin n → M) : orbitRank (⇑e ∘ a) = orbitRank a

Isomorphism invariance of the orbit rank.

Internal Scott rank

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

Internal Scott rank SR(M) = ⨆ (orbitRank a + 1) over all finite tuples, with the all-levels orbit rank of this module (the Scott-rank survey's Definition 2.6 convention; see the module docstring for the discrepancy with Marker's printed Definition 2.2.4).

Equations

• FirstOrder.Language.internalScottRank M = ⨆ (x : (n : ℕ) × (Fin n → M)), FirstOrder.Language.orbitRank x.snd + 1

theorem FirstOrder.Language.orbitRank_add_one_le_internalScottRank {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : orbitRank a + 1 ≤ internalScottRank M

Lower bound: every tuple's orbit rank plus one is at most the internal Scott rank.

theorem FirstOrder.Language.internalScottRank_le {L : Language} {M : Type w} [L.Structure M] {β : Ordinal.{w}} (h : ∀ (n : ℕ) (a : Fin n → M), orbitRank a + 1 ≤ β) : internalScottRank M ≤ β

Upper bound: a bound on every orbitRank a + 1 bounds the internal Scott rank.

theorem FirstOrder.Language.exists_orbitRank_add_one_gt_of_lt_internalScottRank {L : Language} {M : Type w} [L.Structure M] {γ : Ordinal.{w}} (h : γ < internalScottRank M) : ∃ (n : ℕ) (a : Fin n → M), γ < orbitRank a + 1

Cofinal lower bound: every ordinal below the internal Scott rank is exceeded by some orbitRank a + 1.

theorem FirstOrder.Language.internalScottRank_eq_iff {L : Language} {M : Type w} [L.Structure M] {β : Ordinal.{w}} : internalScottRank M = β ↔ (∀ (n : ℕ) (a : Fin n → M), orbitRank a + 1 ≤ β) ∧ ∀ γ < β, ∃ (n : ℕ) (a : Fin n → M), γ < orbitRank a + 1

Exact-rank criterion: internalScottRank M = β iff β bounds every orbitRank a + 1 and every ordinal below β is exceeded by some orbitRank a + 1.

theorem FirstOrder.Language.internalScottRank_map_equiv {L : Language} {M : Type w} [L.Structure M] {M' : Type w} [L.Structure M'] (e : L.Equiv M M') : internalScottRank M' = internalScottRank M

Isomorphism invariance of the internal Scott rank.

Pointed automorphisms

theorem FirstOrder.Language.exists_automorphism_of_bfEquiv_all {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {n : ℕ} {a b : Fin n → M} (h : ∀ (α : Ordinal.{w}), BFEquiv α n a b) : ∃ (e : L.Equiv M M), ⇑e ∘ a = b

Pointed Karp. In a countable structure, two tuples back-and-forth equivalent at every level are carried to each other by an automorphism. The automorphism comes from the countable back-and-forth construction applied to the pointed family; that it carries a to b is read off the graph specification through the equality atoms of the extended tuples.

The orbit characterization and the semantic exact-rank criterion

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

Equivalence at the orbit rank is automorphism. For countable M, b is equivalent to a at level orbitRank a iff an automorphism carries a to b.

theorem FirstOrder.Language.bfEquiv_all_iff_exists_automorphism {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {n : ℕ} {a b : Fin n → M} : (∀ (γ : Ordinal.{w}), BFEquiv γ n a b) ↔ ∃ (e : L.Equiv M M), ⇑e ∘ a = b

Equivalence at every level is automorphism, for countable M.

theorem FirstOrder.Language.mem_orbitStable_of_orbit_determined {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {a : Fin n → M} {β : Ordinal.{w}} (h : ∀ (b : Fin n → M), BFEquiv β n a b → ∃ (e : L.Equiv M M), ⇑e ∘ a = b) : β ∈ orbitStable a

A level at which the class of a is its automorphism orbit is a stabilization level.

theorem FirstOrder.Language.internalScottRank_le_of_orbits_determined {L : Language} {M : Type w} [L.Structure M] {α : Ordinal.{w}} (h : ∀ (n : ℕ) (a : Fin n → M), ∃ β < α, ∀ (b : Fin n → M), BFEquiv β n a b → ∃ (e : L.Equiv M M), ⇑e ∘ a = b) : internalScottRank M ≤ α

Semantic upper bound. If every tuple has some level below α at which its class is its automorphism orbit, the internal Scott rank is at most α.

theorem FirstOrder.Language.le_internalScottRank_of_not_automorphic {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {α : Ordinal.{w}} (h : ∀ β < α, ∃ (n : ℕ) (a : Fin n → M) (b : Fin n → M), BFEquiv β n a b ∧ ¬∃ (e : L.Equiv M M), ⇑e ∘ a = b) : α ≤ internalScottRank M

Semantic lower bound. If below every β < α some tuples are β-equivalent but not automorphic, the internal Scott rank is at least α. Countability of M enters through the pointed automorphism theorem.

theorem FirstOrder.Language.internalScottRank_eq_of_orbits {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {α : Ordinal.{w}} (hup : ∀ (n : ℕ) (a : Fin n → M), ∃ β < α, ∀ (b : Fin n → M), BFEquiv β n a b → ∃ (e : L.Equiv M M), ⇑e ∘ a = b) (hlow : ∀ β < α, ∃ (n : ℕ) (a : Fin n → M) (b : Fin n → M), BFEquiv β n a b ∧ ¬∃ (e : L.Equiv M M), ⇑e ∘ a = b) : internalScottRank M = α

Semantic exact-rank criterion: the internal Scott rank is α when every tuple's orbit is determined below α and below every β < α some β-equivalent tuples are not automorphic.

Infinite pure sets

@[instance_reducible]

def FirstOrder.Language.instStructureEmpty_infinitaryLogic {X : Type w} : Language.empty.Structure X

The unique empty-language structure on X, local to this section.

Equations

• FirstOrder.Language.instStructureEmpty_infinitaryLogic = FirstOrder.Language.emptyStructure

theorem FirstOrder.Language.sameAtomicType_empty_iff {X : Type w} {n : ℕ} (a b : Fin n → X) : SameAtomicType a b ↔ ∀ (i j : Fin n), a i = a j ↔ b i = b j

In the empty language, atomic agreement is agreement of the equality pattern.

theorem FirstOrder.Language.bfEquiv_all_of_pattern {X : Type w} [Infinite X] {n : ℕ} (a b : Fin n → X) (h : ∀ (i j : Fin n), a i = a j ↔ b i = b j) (α : Ordinal.{w}) : BFEquiv α n a b

In an infinite pure set, tuples with the same equality pattern are equivalent at every level: extend by a matching old coordinate, or by a fresh element.

theorem FirstOrder.Language.orbitRank_pureSet {X : Type w} [Infinite X] {n : ℕ} (a : Fin n → X) : orbitRank a = 0

Every tuple of an infinite pure set has orbit rank 0.

theorem FirstOrder.Language.internalScottRank_pureSet {X : Type w} [Infinite X] : internalScottRank X = 1

An infinite pure set has internal Scott rank 1.