External stabilization and the Scott height

A structure M stabilizes completely at α when, for every countable structure N in Type, finite or empty ones included, and for tuples of every length, back-and-forth equivalence at α between a tuple of M and a tuple of N upgrades to equivalence at α + 1. Unlike the internal stabilization SelfStabilizesCompletely, the partner tuple lies in another structure. The Scott height scottHeight M is the least such level, an ordinal in the universe of M.

The height is what makes back-and-forth equivalence of countable structures decide isomorphism at a single level: for countable M and N, M ≅ N exactly when their empty tuples are equivalent at scottHeight M. It is an isomorphism invariant, and it is countable for countable M, because it lies within ω of the internal stabilization level: if M stabilizes internally at α, it stabilizes externally at every limit level above α, in particular at α + ω. Hence scottHeight M ≤ internalScottRank M + ω.

The comparison partners range over countable structures in Type only. Every countable structure in any universe is isomorphic to one of these, so the isomorphism criterion holds for countable partners in every universe.

Main definitions

• TauCeti.StabilizesCompletely M α: external one-step stabilization of M at α.
• TauCeti.scottHeight M: the least externally stabilizing level.

Main results

• TauCeti.StabilizesCompletely.bfEquiv_of_le: external stabilization propagates to all later levels.
• TauCeti.SelfStabilizesCompletely.stabilizesCompletely_of_isSuccLimit: internal stabilization at α gives external stabilization at every limit above α.
• TauCeti.scottHeight_le_internalScottRank_add_omega0 and TauCeti.scottHeight_lt_omega_one.
• FirstOrder.Language.Equiv.scottHeight_eq: the Scott height is an isomorphism invariant.
• TauCeti.nonempty_equiv_of_bfEquiv_of_scottHeight_le and TauCeti.nonempty_equiv_iff_bfEquiv_scottHeight: for countable structures, equivalence at the Scott height decides isomorphism.

References

• Dana Scott, Logic with denumerably long formulas and finite strings of quantifiers, 1965.
• Cameron Freer's cameronfreer/infinitary-logic, checkpoint 518a366cba97b1ae8c4dc64a297a396939bc3e0b, InfinitaryLogic/Scott/Height/Defs.lean and InfinitaryLogic/Scott/InternalRankBounds.lean, defines a Scott height by external stabilization against countable partners in the universe of the structure and proves lift_scottHeight_le_internalScottRank_add_omega0. Here the partners live in Type, the height lives in the universe of the structure, and the bound by the internal rank plus ω comes from a direct back-and-forth argument.

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

M stabilizes completely at α: for every countable structure N in Type and tuples of every length, back-and-forth equivalence at α between a tuple of M and a tuple of N implies equivalence at α + 1.

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

External stabilization is one-step stabilization against every countable structure in Type, at every tuple length.

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

External stabilization at α makes equivalence at α with a countable structure in Type persist at every later level.

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

Every level above an externally stabilizing level is itself externally stabilizing.

theorem TauCeti.SelfStabilizesCompletely.stabilizesCompletely_of_isSuccLimit {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {α : Ordinal.{o}} (h : SelfStabilizesCompletely M α) {β : Ordinal.{o}} (hβ : Order.IsSuccLimit β) (hαβ : α < β) : StabilizesCompletely M β

Internal stabilization at α gives external stabilization at every limit above α.

theorem TauCeti.SelfStabilizesCompletely.stabilizesCompletely_add_omega0 {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {α : Ordinal.{o}} (h : SelfStabilizesCompletely M α) : StabilizesCompletely M (α + Ordinal.omega0)

Internal stabilization at α gives external stabilization at α + ω.

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

Every structure stabilizes externally at some ordinal in its own universe.

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

The Scott height of M: the least ordinal, in the universe of M, at which M stabilizes externally against every countable structure in Type.

theorem TauCeti.scottHeight_def {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] : scottHeight M = sInf {α : Ordinal.{w} | StabilizesCompletely M α}

The Scott height is the infimum of the externally stabilizing levels.

@[simp]

theorem TauCeti.stabilizesCompletely_scottHeight {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] : StabilizesCompletely M (scottHeight M)

The infimum defining the Scott height is attained.

theorem TauCeti.scottHeight_le {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] {α : Ordinal.{w}} (h : StabilizesCompletely M α) : scottHeight M ≤ α

The Scott height is no larger than any externally stabilizing level.

theorem TauCeti.scottHeight_le_iff {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] {α : Ordinal.{w}} : scottHeight M ≤ α ↔ StabilizesCompletely M α

A level stabilizes externally exactly when it is at least the Scott height.

theorem TauCeti.scottHeight_le_selfStabilizationOrdinal_add_omega0 {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] : scottHeight M ≤ selfStabilizationOrdinal M + Ordinal.omega0

The Scott height is within ω of the least internal stabilization level.

theorem TauCeti.scottHeight_le_internalScottRank_add_omega0 {L : FirstOrder.Language} [L.IsRelational] (M : Type w) [L.Structure M] : scottHeight M ≤ internalScottRank M + Ordinal.omega0

The Scott height is within ω of the internal Scott rank.

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

The Scott height of a countable structure is a countable ordinal. The relational language need not be countable.

theorem TauCeti.nonempty_equiv_of_bfEquiv_of_scottHeight_le {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {N : Type w'} [L.Structure N] [Countable N] {β : Ordinal.{w}} (hβ : scottHeight M ≤ β) (h : BFEquiv β 0 Fin.elim0 Fin.elim0) : Nonempty (L.Equiv M N)

Equivalence at the Scott height decides isomorphism. If M and N are countable, in any universes, and their empty tuples are back-and-forth equivalent at a level at least the Scott height of M, then M and N are isomorphic.

theorem TauCeti.nonempty_equiv_iff_bfEquiv_scottHeight {L : FirstOrder.Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {N : Type w'} [L.Structure N] [Countable N] : Nonempty (L.Equiv M N) ↔ BFEquiv (scottHeight M) 0 Fin.elim0 Fin.elim0

Isomorphism is equivalence at the Scott height. Two countable structures, in any universes, are isomorphic exactly when their empty tuples are back-and-forth equivalent at the Scott height of the first.

theorem FirstOrder.Language.Equiv.stabilizesCompletely_iff {L : Language} [L.IsRelational] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (e : L.Equiv M N) {α : Ordinal.{o}} : TauCeti.StabilizesCompletely M α ↔ TauCeti.StabilizesCompletely N α

External stabilization at a level is invariant under isomorphism.

theorem FirstOrder.Language.Equiv.scottHeight_eq {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] (e : L.Equiv M N) : TauCeti.scottHeight M = TauCeti.scottHeight N

The Scott height is an isomorphism invariant.