Documentation

Mathlib.ModelTheory.Infinitary.QuantifierRank

Quantifier rank of infinitary formulas #

The quantifier rank of an infinitary formula: 0 on atoms, max on implication, successor under ∀, and the supremum over the branching carrier at an infinitary node.

The universe of the rank #

Because the infinitary cases take a supremum over the carrier ι, the natural target is Ordinal.{uι} — the carrier's own ordinal universe. At ι := ℕ this is exactly Ordinal.{0}, which is where Scott analysis wants it; no lifting appears in the L_{ω₁ω} case.

Transport between carriers is therefore stated up to Ordinal.lift: qrank_reindex says reindex preserves rank once both sides are lifted into a common universe. Padding is invisible to rank, since the padded branches are ⊤/⊥, both of rank 0 — which is why the statement holds for empty carriers too, where every branch is padding.

Main definitions #

Main results #

source
noncomputable def FirstOrder.Language.BoundedFormulaInf.qrank {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} :
L.BoundedFormulaInf ι α n → Ordinal.{uι}

The quantifier rank of an infinitary formula, valued in the branching carrier's own ordinal universe.

Equations
Instances For
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_falsum {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} :
    falsum.qrank = 0
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_equal {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {t₁ t₂ : L.Term (α ⊕ Fin n)} :
    (equal t₁ t₂).qrank = 0
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_rel {L : Language} {ι : Type uι} {α : Type u'} {n l : ℕ} {R : L.Relations l} {ts : Fin l → L.Term (α ⊕ Fin n)} :
    (rel R ts).qrank = 0
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_imp {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormulaInf ι α n} :
    (φ.imp ψ).qrank = max φ.qrank ψ.qrank
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_all {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf ι α (n + 1)} :
    φ.all.qrank = Order.succ φ.qrank
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_iSup {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φs : ι → L.BoundedFormulaInf ι α n} :
    (iSup φs).qrank = ⨆ (i : ι), (φs i).qrank
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_iInf {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φs : ι → L.BoundedFormulaInf ι α n} :
    (iInf φs).qrank = ⨆ (i : ι), (φs i).qrank
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_not {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} :
    φ.not.qrank = φ.qrank
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_bot {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} :
    ⊥.qrank = 0
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_top {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} :
    ⊤.qrank = 0
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_ex {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf ι α (n + 1)} :
    φ.ex.qrank = Order.succ φ.qrank
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_alls {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} :
    qrank φ.alls = φ.qrank + ↑n
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_exs {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} :
    qrank φ.exs = φ.qrank + ↑n
    source
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_reindex {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} (c : IndexCoding ι κ) {n : ℕ} (φ : L.BoundedFormulaInf ι α n) :
    Ordinal.lift.{uι, uκ} (reindex c φ).qrank = Ordinal.lift.{uκ, uι} φ.qrank

    Rank transport: carrier transport preserves quantifier rank, up to Ordinal.lift into the common universe.

    Padding is invisible: the branches a coding cannot decode are ⊤/⊥, both of rank 0, so they never raise the supremum. In particular this holds when ι is empty, where every branch of the transported formula is padding.

    source
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_reindex_ofEquiv {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (e : ι ≃ κ) (φ : L.BoundedFormulaInf ι α n) :
    Ordinal.lift.{uι, uκ} (reindex (IndexCoding.ofEquiv e) φ).qrank = Ordinal.lift.{uκ, uι} φ.qrank

    Rank transport along an equivalence coding, where no padding occurs.

    source
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_toInf {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) :
    Ordinal.lift.{uκ, uι} φ.toInf.qrank = Ordinal.lift.{uι, uκ} φ.toInf.qrank

    Carrier-independence of the finitary embedding's rank. A finitary formula has no infinitary nodes, so its rank is the same at every branching carrier — the ranks live in different ordinal universes, so the statement is up to Ordinal.lift, exactly as in qrank_reindex.

    Unlike qrank_reindex this needs no coding between the carriers: there is nothing to transport.