Rank Bounds: sr, AttainedScottRank, and rank-height relations

This file defines sr (the supremum of element ranks without the +1 adjustment) and AttainedScottRank, and proves bounds relating sr, scottRank, and scottHeight.

Main Definitions

• sr: Supremum of element ranks (without +1), as opposed to scottRank (with +1).
• AttainedScottRank: Whether the supremum in sr is attained by some element.

Main Results

• sr_le_scottRank: sr ≤ scottRank always.
• sr_le_scottHeight_of: sr ≤ scottHeight (conditional on CRH).
• scottRank_le_scottHeight_succ_of: scottRank ≤ scottHeight + 1 (conditional on CRH).

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

The supremum of element ranks without the +1 adjustment.

This is denoted sr(M) in some references (e.g., Marker). Compare with scottRank which is ⨆ m, elementRank m + 1 (denoted SR(M) or α(M)).

Equations

• FirstOrder.Language.sr M = ⨆ (m : M), FirstOrder.Language.elementRank m

theorem FirstOrder.Language.sr_le_scottRank {L : Language} (M : Type w) [L.Structure M] [Countable M] : sr M ≤ scottRank M

sr ≤ scottRank always holds, since scottRank = ⨆ m, elementRank m + 1 ≥ ⨆ m, elementRank m.

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

The element-rank supremum sr is bounded by scottHeight.

Since scottHeight M is a complete stabilization ordinal (conditional on CountableRefinementHypothesis), every elementRank m ≤ scottHeight M, so the supremum sr M = ⨆ m, elementRank m ≤ scottHeight M.

theorem FirstOrder.Language.scottRank_le_scottHeight_succ_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) (M : Type w) [L.Structure M] [Countable M] : scottRank M ≤ scottHeight M + 1

scottRank M ≤ scottHeight M + 1.

Since scottRank M = ⨆ m, elementRank m + 1 and each elementRank m ≤ scottHeight M (via elementRank_le_completeStab at the complete stabilization ordinal scottHeight M), we get scottRank M ≤ scottHeight M + 1. Conditional on CountableRefinementHypothesis.

def FirstOrder.Language.AttainedScottRank {L : Language} (M : Type w) [L.Structure M] [Countable M] : Prop

A structure has attained Scott rank if some element achieves the supremum sr.

This is an important distinction in the theory of Scott rank: when the rank is attained, the structure has a "witness" element of maximal complexity.

Equations

• FirstOrder.Language.AttainedScottRank M = ∃ (m : M), FirstOrder.Language.elementRank m = FirstOrder.Language.sr M