Documentation

InfinitaryLogic.Lomega1omega.QuantifierRank

Lω₁ω Quantifier Rank #

This file defines the quantifier rank of Lω₁ω formulas and the "agree up to rank α" relation between structures.

Main Definitions #

Main Results #

References #

Quantifier Rank #

source
@[reducible, inline]
noncomputable abbrev FirstOrder.Language.BoundedFormulaω.qrank {L : Language} {α : Type u_1} {n : ℕ} :
L.BoundedFormulaω α n → Ordinal.{0}

The quantifier rank of an Lω₁ω formula: the carrier-generic BoundedFormulaInf.qrank, specialized at the branching carrier ℕ.

Because the rank is valued in the carrier's own ordinal universe, the ℕ specialization lands in Ordinal.{0} exactly — no lifting, which is what Scott analysis needs.

This is an abbrev, so it is the upstream rank rather than a parallel copy of it (gated by rfl below). The ω-facing lemmas beneath keep their historical statements: qrank_all and qrank_ex are still stated with + 1 rather than Order.succ, so downstream sees no proposition-level change. Only code that relied on the old definition unfolding by rfl is affected.

Note: For Lω₁ω, the quantifier rank is always a countable ordinal (< ω₁).

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev FirstOrder.Language.Formulaω.qrank {L : Language} {α : Type u_1} (φ : L.Formulaω α) :
    Ordinal.{0}

    Quantifier rank of a formula (no bound variables).

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev FirstOrder.Language.Sentenceω.qrank {L : Language} (φ : L.Sentenceω) :
      Ordinal.{0}

      Quantifier rank of a sentence.

      Equations
      Instances For

        Gate: the ω rank IS the upstream rank #

        Must close by rfl — that is what certifies this is the carrier-generic rank specialized at ℕ rather than a parallel recursive copy that happens to agree.

        Quantifier Rank Lemmas #

        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.qrank_falsum {L : Language} {α : Type u_1} {n : ℕ} :
        falsum.qrank = 0
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.qrank_bot {L : Language} {α : Type u_1} {n : ℕ} :
        ⊥.qrank = 0
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.qrank_equal {L : Language} {α : Type u_1} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) :
        (equal t₁ t₂).qrank = 0
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.qrank_rel {L : Language} {α : Type u_1} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) :
        (rel R ts).qrank = 0
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.qrank_imp {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) :
        (φ.imp ψ).qrank = max φ.qrank ψ.qrank
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.qrank_all {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) :
        φ.all.qrank = φ.qrank + 1

        Universal quantification adds 1. Kept in + 1 form: upstream states it with Order.succ, and the two agree for ordinals.

        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.qrank_iSup {L : Language} {α : Type u_1} {n : ℕ} (φs : ℕ → L.BoundedFormulaω α n) :
        (iSup φs).qrank = ⨆ (k : ℕ), (φs k).qrank
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.qrank_iInf {L : Language} {α : Type u_1} {n : ℕ} (φs : ℕ → L.BoundedFormulaω α n) :
        (iInf φs).qrank = ⨆ (k : ℕ), (φs k).qrank
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.qrank_top {L : Language} {α : Type u_1} {n : ℕ} :
        ⊤.qrank = 0

        The top formula has rank 0.

        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.qrank_not {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormulaω α n) :
        φ.not.qrank = φ.qrank

        Negation preserves quantifier rank.

        source
        theorem FirstOrder.Language.BoundedFormulaω.qrank_and {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) :
        (φ.and ψ).qrank = max φ.qrank ψ.qrank

        Conjunction takes max of ranks.

        source
        theorem FirstOrder.Language.BoundedFormulaω.qrank_or {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) :
        (φ.or ψ).qrank = max φ.qrank ψ.qrank

        Disjunction takes max of ranks.

        source
        theorem FirstOrder.Language.BoundedFormulaω.qrank_ex {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) :
        φ.ex.qrank = φ.qrank + 1

        Existential quantification adds 1 to rank. Kept in + 1 form, as for qrank_all.

        source
        theorem FirstOrder.Language.BoundedFormulaω.qrank_einf {L : Language} {α : Type u_1} {n : ℕ} {ι : Type u_2} [Encodable ι] (φs : ι → L.BoundedFormulaω α n) :
        (einf φs).qrank = ⨆ (i : ι), (φs i).qrank

        The quantifier rank of einf is the sup of the family's ranks.

        Note: This requires careful universe handling since einf encodes ι into ℕ, which changes the universe of the supremum. We need Small.{0} ι (from Encodable) for Ordinal.le_iSup to work at Ordinal.{0}.

        source
        theorem FirstOrder.Language.BoundedFormulaω.qrank_esup {L : Language} {α : Type u_1} {n : ℕ} {ι : Type u_2} [Encodable ι] (φs : ι → L.BoundedFormulaω α n) :
        (esup φs).qrank = ⨆ (i : ι), (φs i).qrank

        The quantifier rank of esup is the sup of the family's ranks.

        source
        theorem FirstOrder.Language.BoundedFormulaω.qrank_castLE {L : Language} {α : Type u_1} {m n : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaω α m) :
        (castLE h φ).qrank = φ.qrank

        castLE preserves quantifier rank.

        source
        theorem FirstOrder.Language.BoundedFormulaω.qrank_relabel {L : Language} {α β : Type w} {p : ℕ} (g : α → β ⊕ Fin p) {k : ℕ} (φ : L.BoundedFormulaω α k) :
        (relabel g φ).qrank = φ.qrank

        relabel preserves quantifier rank.

        source
        theorem FirstOrder.Language.qrank_openBounds {L : Language} {n : ℕ} (φ : L.BoundedFormulaω Empty n) :
        φ.openBounds.qrank = φ.qrank

        openBounds preserves quantifier rank: the universal case is qrank_relabel.

        Equivalence up to Quantifier Rank #

        source
        def FirstOrder.Language.EquivQRω (L : Language) (α : Ordinal.{0}) (M N : Type w) [L.Structure M] [L.Structure N] :
        Prop

        Two structures are equivalent up to quantifier rank α if they satisfy the same Lω₁ω sentences of quantifier rank ≤ α.

        This is a semantic relation that captures agreement on formulas of bounded complexity.

        Equations
        Instances For
          source
          theorem FirstOrder.Language.EquivQRω.refl {L : Language} {M : Type w} [L.Structure M] (α : Ordinal.{0}) :
          L.EquivQRω α M M

          Equivalence up to quantifier rank is reflexive.

          source
          theorem FirstOrder.Language.EquivQRω.symm {L : Language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] {α : Ordinal.{0}} (h : L.EquivQRω α M N) :
          L.EquivQRω α N M

          Equivalence up to quantifier rank is symmetric.

          source
          theorem FirstOrder.Language.EquivQRω.trans {L : Language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] {P : Type w} [L.Structure P] {α : Ordinal.{0}} (h₁ : L.EquivQRω α M N) (h₂ : L.EquivQRω α N P) :
          L.EquivQRω α M P

          Equivalence up to quantifier rank is transitive.

          source
          theorem FirstOrder.Language.EquivQRω.monotone {L : Language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] {α β : Ordinal.{0}} (hαβ : α ≤ β) (h : L.EquivQRω β M N) :
          L.EquivQRω α M N

          Equivalence at higher rank implies equivalence at lower rank.

          source
          theorem FirstOrder.Language.EquivQRω.zero_iff_agree_atomic {L : Language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] :
          L.EquivQRω 0 M N ↔ ∀ (φ : L.Sentenceω), φ.qrank = 0 → (φ.Realize M ↔ φ.Realize N)

          Equivalence at rank 0 means agreement on all quantifier-free sentences.