Documentation

Linglib.Core.ModelTheory.QuantifierRank

Quantifier rank of first-order formulas #

[UPSTREAM] candidate. mathlib's ModelTheory has formula complexity classes (IsQF, IsPrenex, IsUniversal) but no quantifier-rank function. qr φ is the maximal nesting depth of quantifiers in φ ([Lib04] Definition 3.8; [Hod93] §3.3), the measure indexing Ehrenfeucht–Fraïssé games and ≡ₙ n-equivalence. It is bounded by the number of quantifiers, and the gap can be exponential.

mathlib has the ∞-rank apparatus (ElementarilyEquivalent, the unbounded back-and-forth IsExtensionPair); qr is the bottom of the missing finite-rank layer.

Main definitions #

References #

source
def FirstOrder.Language.BoundedFormula.qr {L : Language} {α : Type u_1} {n : ℕ} :
L.BoundedFormula α n → ℕ

The quantifier rank of a formula is the maximal nesting depth of its quantifiers. Atomic formulas have rank 0, an implication has the larger rank of its two sides, and all adds one.

Equations
  • FirstOrder.Language.BoundedFormula.falsum.qr = 0
  • (FirstOrder.Language.BoundedFormula.equal t₁ t₂).qr = 0
  • (FirstOrder.Language.BoundedFormula.rel R ts).qr = 0
  • (f₁.imp f₂).qr = max f₁.qr f₂.qr
  • f.all.qr = f.qr + 1
Instances For
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_falsum {L : Language} {α : Type u_1} {n : ℕ} :
    falsum.qr = 0
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_bot {L : Language} {α : Type u_1} {n : ℕ} :
    ⊥.qr = 0
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_equal {L : Language} {α : Type u_1} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) :
    (equal t₁ t₂).qr = 0
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_rel {L : Language} {α : Type u_1} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) :
    (rel R ts).qr = 0
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_imp {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) :
    (φ.imp ψ).qr = max φ.qr ψ.qr
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_all {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) :
    φ.all.qr = φ.qr + 1
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_not {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α n) :
    φ.not.qr = φ.qr
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_top {L : Language} {α : Type u_1} {n : ℕ} :
    ⊤.qr = 0
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_inf {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) :
    (φ ⊓ ψ).qr = max φ.qr ψ.qr
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_sup {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) :
    (φ ⊔ ψ).qr = max φ.qr ψ.qr
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_iff {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) :
    (φ.iff ψ).qr = max φ.qr ψ.qr
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_ex {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) :
    φ.ex.qr = φ.qr + 1
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.qr_relabelEquiv {L : Language} {α : Type u_1} {β : Type u_2} (g : α ≃ β) {n : ℕ} (φ : L.BoundedFormula α n) :
    ((relabelEquiv g) φ).qr = φ.qr

    Quantifier rank is invariant under relabelling free variables along a bijection (relabelEquiv acts structurally, only on the terms inside atomic formulas).

    source
    theorem FirstOrder.Language.BoundedFormula.qr_iInf_le {L : Language} {α : Type u_1} {n : ℕ} {β : Type u_2} [Finite β] {f : β → L.BoundedFormula α n} {k : ℕ} (h : ∀ (b : β), (f b).qr ≤ k) :
    (iInf f).qr ≤ k
    source
    theorem FirstOrder.Language.BoundedFormula.qr_iSup_le {L : Language} {α : Type u_1} {n : ℕ} {β : Type u_2} [Finite β] {f : β → L.BoundedFormula α n} {k : ℕ} (h : ∀ (b : β), (f b).qr ≤ k) :
    (iSup f).qr ≤ k
    source
    theorem FirstOrder.Language.BoundedFormula.IsAtomic.qr_eq_zero {L : Language} {α : Type u_1} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsAtomic) :
    φ.qr = 0

    An atomic formula has quantifier rank 0.

    source
    theorem FirstOrder.Language.BoundedFormula.IsQF.qr_eq_zero {L : Language} {α : Type u_1} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsQF) :
    φ.qr = 0

    A quantifier-free formula has quantifier rank 0.