Documentation

CslibFrontier.Logics.FirstOrder.QuantifierRank

Quantifier rank #

The quantifier rank of a first-order formula is the maximal nesting depth of its quantifiers. It is the syntactic measure matched by the number of rounds of Ehrenfeucht–Fraïssé games (CslibFrontier.Logics.FirstOrder.EhrenfeuchtFraisse.Hintikka). The notion is stated for Mathlib's bounded formulas over an arbitrary language; no finiteness assumption is involved.

Main definitions #

Main results #

References #

source
def Cslib.Logic.FO.quantifierRank {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} :
L.BoundedFormula α n → ℕ

The quantifier rank of a bounded formula: the maximal nesting depth of quantifiers.

Instances For
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_falsum {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} :
    quantifierRank FirstOrder.Language.BoundedFormula.falsum = 0
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_bot {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} :
    quantifierRank ⊥ = 0
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_equal {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) :
    quantifierRank (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = 0
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_rel {L : FirstOrder.Language} {α : Type u_1} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) :
    quantifierRank (FirstOrder.Language.BoundedFormula.rel R ts) = 0
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_bdEqual {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) :
    quantifierRank (t₁.bdEqual t₂) = 0
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_relations_boundedFormula {L : FirstOrder.Language} {α : Type u_1} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) :
    quantifierRank (R.boundedFormula ts) = 0
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_relations_boundedFormula₁ {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (R : L.Relations 1) (t : L.Term (α ⊕ Fin n)) :
    quantifierRank (R.boundedFormula₁ t) = 0
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_relations_boundedFormula₂ {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (R : L.Relations 2) (t₁ t₂ : L.Term (α ⊕ Fin n)) :
    quantifierRank (R.boundedFormula₂ t₁ t₂) = 0
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_imp {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) :
    quantifierRank (φ.imp ψ) = max (quantifierRank φ) (quantifierRank ψ)
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_all {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) :
    quantifierRank φ.all = quantifierRank φ + 1
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_not {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α n) :
    quantifierRank φ.not = quantifierRank φ
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_ex {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) :
    quantifierRank φ.ex = quantifierRank φ + 1
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_top {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} :
    quantifierRank ⊤ = 0
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_inf {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) :
    quantifierRank (φ ⊓ ψ) = max (quantifierRank φ) (quantifierRank ψ)
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_sup {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) :
    quantifierRank (φ ⊔ ψ) = max (quantifierRank φ) (quantifierRank ψ)
    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_iff {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormula α n) :
    quantifierRank (φ.iff ψ) = max (quantifierRank φ) (quantifierRank ψ)
    source
    theorem Cslib.Logic.FO.quantifierRank_iInf_le {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} {β : Type u_2} [Finite β] {f : β → L.BoundedFormula α n} {m : ℕ} (h : ∀ (b : β), quantifierRank (f b) ≤ m) :
    quantifierRank (FirstOrder.Language.BoundedFormula.iInf f) ≤ m

    A finite conjunction has quantifier rank at most m when each conjunct does.

    source
    theorem Cslib.Logic.FO.quantifierRank_iSup_le {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} {β : Type u_2} [Finite β] {f : β → L.BoundedFormula α n} {m : ℕ} (h : ∀ (b : β), quantifierRank (f b) ≤ m) :
    quantifierRank (FirstOrder.Language.BoundedFormula.iSup f) ≤ m

    A finite disjunction has quantifier rank at most m when each disjunct does.

    Invariance under Mathlib's syntactic maps #

    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_castLE {L : FirstOrder.Language} {α : Type u_1} {m m' : ℕ} (h : m ≤ m') (φ : L.BoundedFormula α m) :
    quantifierRank (FirstOrder.Language.BoundedFormula.castLE h φ) = quantifierRank φ

    Raising the number of bound variables in scope does not change the rank.

    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_relabel {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} {β : Type u_2} (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormula α k) :
    quantifierRank (FirstOrder.Language.BoundedFormula.relabel g φ) = quantifierRank φ

    Relabeling variables does not change the rank.

    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_formula_relabel {L : FirstOrder.Language} {α : Type u_1} {β : Type u_2} (g : α → β) (φ : L.Formula α) :
    quantifierRank (FirstOrder.Language.Formula.relabel g φ) = quantifierRank φ

    Relabeling the free variables of a formula does not change the rank.

    source
    @[simp]
    theorem Cslib.Logic.FO.quantifierRank_toFormula {L : FirstOrder.Language} {α : Type u_1} {k : ℕ} (φ : L.BoundedFormula α k) :
    quantifierRank φ.toFormula = quantifierRank φ

    Turning the bound variables in scope into free variables does not change the rank.