Documentation

InfinitaryLogic.Scott.Height

Scott Height and Canonical Scott Sentence #

This file defines the Scott height of a structure (the ordinal at which its Scott analysis stabilizes) and the canonical Scott sentence (the Scott formula at Scott height).

Main Definitions #

Main Results #

References #

Scott Height #

source
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.
Instances For
    source
    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.

    source
    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.

    source
    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.

    Canonical Scott Sentence #

    source
    noncomputable def FirstOrder.Language.canonicalScottSentence {L : Language} [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] :
    L.Formulaω (Fin 0)

    The canonical Scott sentence of a structure M, defined as the Scott formula at Scott height level for the empty tuple.

    This is the "optimal" Scott sentence in the sense that its quantifier rank is minimized (among Scott formulas). It characterizes the structure up to potential isomorphism, and for countable structures, up to isomorphism.

    Equations
    Instances For

      Conditional Canonical Scott Sentence Pipeline #

      source
      theorem FirstOrder.Language.canonicalScottSentence_iff_potentialIso_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] :
      (canonicalScottSentence M).realize_as_sentence N ↔ Nonempty (L.PotentialIso M N)

      Conditional variant of canonicalScottSentence_iff_potentialIso.

      source
      theorem FirstOrder.Language.canonicalScottSentence_characterizes_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] :
      (canonicalScottSentence M).realize_as_sentence N ↔ Nonempty (L.Equiv M N)

      Conditional variant of canonicalScottSentence_characterizes.

      source
      theorem FirstOrder.Language.canonicalScottSentence_equiv_scottSentence_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] :
      (canonicalScottSentence M).realize_as_sentence N ↔ (scottSentence M).realize_as_sentence N

      Conditional variant of canonicalScottSentence_equiv_scottSentence.

      sr and SR #

      source
      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
      Instances For
        source
        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.

        source
        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.

        source
        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.

        Attained Scott Rank #

        source
        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
        Instances For
          source
          theorem FirstOrder.Language.canonicalScottSentence_qrank_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) (M : Type w) [L.Structure M] [Countable M] :
          (canonicalScottSentence M).qrank ≤ scottHeight M + Ordinal.omega0

          Conditional variant of canonicalScottSentence_qrank.

          Unconditional Wrappers (via CRH) #

          source
          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.

          source
          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 α)).

          source
          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.

          source
          theorem FirstOrder.Language.canonicalScottSentence_iff_potentialIso {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] :
          (canonicalScottSentence M).realize_as_sentence N ↔ Nonempty (L.PotentialIso M N)

          The canonical Scott sentence characterizes potential isomorphism.

          source
          theorem FirstOrder.Language.canonicalScottSentence_characterizes {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] :
          (canonicalScottSentence M).realize_as_sentence N ↔ Nonempty (L.Equiv M N)

          For countable structures, the canonical Scott sentence characterizes isomorphism.

          source
          theorem FirstOrder.Language.canonicalScottSentence_equiv_scottSentence {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] :
          (canonicalScottSentence M).realize_as_sentence N ↔ (scottSentence M).realize_as_sentence N

          The canonical Scott sentence is semantically equivalent to the standard Scott sentence.

          source
          theorem FirstOrder.Language.canonicalScottSentence_qrank {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] :
          (canonicalScottSentence M).qrank ≤ scottHeight M + Ordinal.omega0

          The quantifier rank of the canonical Scott sentence is bounded.