Documentation

TauCeti.ModelTheory.Infinitary.QuantifierRank

Quantifier rank of infinitary formulas #

The quantifier rank of an infinitary formula is 0 on atoms, the maximum on implication, the successor under a quantifier, and the supremum of the branches at an infinitary conjunction or disjunction.

The supremum ranges over the branching carrier ι, so the rank is valued in Ordinal.{uι}, the carrier's own ordinal universe; at ι := ℕ this is Ordinal.{0}. Ranks at different carriers live in different universes, and are compared after Ordinal.lift into a common one: carrier transport preserves rank up to this lift. Padding does not raise the rank, since the padding branches ⊤ and ⊥ have rank 0; this includes an empty source carrier, where every branch is padding.

Main definitions #

Main results #

References #

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 carrier's ordinal universe: 0 on atoms, the maximum on implication, the successor under ∀, and the supremum of the branches at an infinitary node.

Instances For
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_falsum {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} :
    falsum.qrank = 0

    The false formula has rank 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

    An equation has rank 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

    A relational atom has rank 0.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_imp {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormulaInf ι α n} :
    (φ.imp ψ).qrank = max φ.qrank ψ.qrank

    An implication has the larger rank of its two sides.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_all {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf ι α (n + 1)} :
    φ.all.qrank = Order.succ φ.qrank

    Universal quantification raises the rank by one.

    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

    A disjunction over the carrier has the supremum of the ranks of its branches.

    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

    A conjunction over the carrier has the supremum of the ranks of its branches.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_not {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} :
    φ.not.qrank = φ.qrank

    Negation does not change the rank.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_bot {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} :
    ⊥.qrank = 0

    ⊥ has rank 0.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_top {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} :
    ⊤.qrank = 0

    ⊤ has rank 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

    Existential quantification raises the rank by one.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_alls {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} :
    qrank φ.alls = φ.qrank + ↑n

    Closing all n bound-variable slots universally adds n to the rank.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_exs {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf ι α n} :
    qrank φ.exs = φ.qrank + ↑n

    Closing all n bound-variable slots existentially adds n to the rank.

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

    Carrier transport preserves quantifier rank, up to Ordinal.lift into a common universe, for every coding, including from an empty carrier.

    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

    The rank of a finitary formula does not depend on the carrier, up to Ordinal.lift.

    source
    theorem FirstOrder.Language.BoundedFormulaInf.qrank_toInf_lt_omega0 {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) :
    φ.toInf.qrank < Ordinal.omega0

    The rank of a finitary formula is finite.