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 φ — the standard measure indexing Ehrenfeucht–Fraïssé games and ≡ₙ n-equivalence, the foundation of every first-order inexpressibility result (e.g. Studies.BarwiseCooper1981's most ∉ FO, whose ad-hoc numQuant this generalizes).

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

Main definitions

• FirstOrder.Language.BoundedFormula.qr — quantifier rank (max quantifier nesting).

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

Quantifier rank: the maximal nesting depth of quantifiers in a formula. Atomic formulas have rank 0, imp takes the max, 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

@[simp]

theorem FirstOrder.Language.BoundedFormula.qr_falsum {L : Language} {α : Type u_1} {n : ℕ} : falsum.qr = 0

@[simp]

theorem FirstOrder.Language.BoundedFormula.qr_bot {L : Language} {α : Type u_1} {n : ℕ} : ⊥.qr = 0

@[simp]

theorem FirstOrder.Language.BoundedFormula.qr_equal {L : Language} {α : Type u_1} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : (equal t₁ t₂).qr = 0

@[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

@[simp]

theorem FirstOrder.Language.BoundedFormula.qr_imp {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) : (φ.imp ψ).qr = max φ.qr ψ.qr

@[simp]

theorem FirstOrder.Language.BoundedFormula.qr_all {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) : φ.all.qr = φ.qr + 1

@[simp]

theorem FirstOrder.Language.BoundedFormula.qr_not {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α n) : φ.not.qr = φ.qr

@[simp]

theorem FirstOrder.Language.BoundedFormula.qr_top {L : Language} {α : Type u_1} {n : ℕ} : ⊤.qr = 0

@[simp]

theorem FirstOrder.Language.BoundedFormula.qr_inf {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) : (φ ⊓ ψ).qr = max φ.qr ψ.qr

@[simp]

theorem FirstOrder.Language.BoundedFormula.qr_sup {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) : (φ ⊔ ψ).qr = max φ.qr ψ.qr

@[simp]

theorem FirstOrder.Language.BoundedFormula.qr_iff {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) : (φ.iff ψ).qr = max φ.qr ψ.qr

@[simp]

theorem FirstOrder.Language.BoundedFormula.qr_ex {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) : φ.ex.qr = φ.qr + 1

@[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).

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.

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.