Documentation

InfinitaryLogic.Scott.Rank

Scott Rank #

This file defines the Scott rank of a structure and proves that it is below ω₁ for countable structures.

Main Definitions #

Main Results #

Implementation Notes #

We define Scott rank as sup {elementRank a + 1 : a ∈ M}, where elementRank a is the least ordinal α such that any tuple extending with a is determined by its α-type. This is equivalent to the stabilization ordinal approach but more compositional.

source
noncomputable def FirstOrder.Language.elementRank {L : Language} {M : Type w} [L.Structure M] (m : M) :
Ordinal.{0}

The rank of an element m in a structure M: the least ordinal α such that for any tuple a containing m, the α-type of a determines whether any extension has a back-and-forth equivalent extension.

We use Ordinal.{0} for consistency with stabilizationOrdinal and BFEquiv in formulas.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def FirstOrder.Language.scottRank {L : Language} (M : Type w) [L.Structure M] [Countable M] :
    Ordinal.{0}

    The Scott rank of a structure M is the supremum of element ranks + 1. We use Ordinal.{0} for consistency with elementRank and stabilizationOrdinal.

    Equations
    Instances For
      source
      theorem FirstOrder.Language.elementRank_le_completeStab {L : Language} {M : Type w} [L.Structure M] [Countable M] {α : Ordinal.{0}} (hstab : StabilizesCompletely M α) (m : M) :
      elementRank m ≤ α

      The elementRank of any element is bounded by any complete stabilization ordinal.

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

      Conditional variant of elementRank_lt_omega1.

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

      Conditional variant of scottRank_lt_omega1.

      Unconditional Wrappers (via CRH) #

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

      Element rank is below ω₁ for countable structures.

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

      Scott rank of a countable structure is a countable ordinal.