Scott Height: Definition and Core Properties

The Scott height of a structure M is the least ordinal at which the Scott formula analysis stabilizes for all tuples simultaneously.

Main Definitions

• scottHeight: The least ordinal where the Scott formulas stabilize for all tuples.

Main Results

• scottHeight_lt_omega1: Scott height is a countable ordinal.
• scottHeight_stabilizesCompletely: At Scott height, all tuple sizes have stabilized.
• scottHeight_eq_of_equiv: Scott height is invariant under L-isomorphism.

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

The Scott height of a structure M: the least ordinal at which the Scott formula analysis stabilizes for all tuples simultaneously.

This is defined as the least ordinal α such that for all n and all tuples a : Fin n → M, if a structure N satisfies scottFormula a α, then it also satisfies scottFormula a (α + 1), and vice versa.

Equivalently, this is the least α where BFEquiv α n a b implies BFEquiv (α + 1) n a b for all tuples.

Scott height is related to but may differ from Scott rank. We always have scottHeight ≤ scottRank.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.scottHeight_lt_omega1_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) (M : Type w) [L.Structure M] [Countable M] : scottHeight M < Ordinal.omega 1

Conditional variant of scottHeight_lt_omega1.

theorem FirstOrder.Language.scottHeight_stabilizesCompletely_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) (M : Type w) [L.Structure M] [Countable M] : StabilizesCompletely M (scottHeight M)

Conditional variant of scottHeight_stabilizesCompletely.

theorem FirstOrder.Language.scottHeight_le_implies_stabilizesCompletely_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) (M : Type w) [L.Structure M] [Countable M] {α : Ordinal.{0}} (hα : scottHeight M ≤ α) : StabilizesCompletely M α

At any ordinal ≥ scottHeight, the structure stabilizes completely. Conditional on CountableRefinementHypothesis.

theorem FirstOrder.Language.scottHeight_lt_omega1 {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] : scottHeight M < Ordinal.omega 1

Scott height is less than ω₁ for countable structures.

theorem FirstOrder.Language.scottHeight_stabilizesCompletely {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] : StabilizesCompletely M (scottHeight M)

At Scott height, all tuple sizes have stabilized (BFEquiv α ↔ BFEquiv (succ α)).

theorem FirstOrder.Language.scottHeight_eq_of_equiv {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] (e : L.Equiv M N) : scottHeight M = scottHeight N

Scott height is invariant under L-isomorphism.