L∞ω Quantifier Rank #

This file defines the quantifier rank of L∞ω formulas and the "agree up to rank α" relation between structures.

Main Definitions #

BoundedFormulaInf.qrank: The quantifier rank of an L∞ω formula.
EquivQRInf: Two structures are equivalent up to quantifier rank α if they satisfy the same sentences of quantifier rank ≤ α.

Main Results #

EquivQRInf.refl, EquivQRInf.symm, EquivQRInf.trans: Equivalence relation properties.
EquivQRInf.monotone: Higher rank equivalence implies lower rank equivalence.

References #

[KK04]

Quantifier Rank #

source

noncomputable def FirstOrder.Language.BoundedFormulaInf.qrank {L : Language} {α : Type u_1} {n : ℕ} :

L.BoundedFormulaInf α n → Ordinal.{0}

The quantifier rank of an L∞ω formula.

Atomic formulas (falsum, equal, rel) have rank 0
Implication takes the max of its arguments
Universal quantification adds 1
Infinitary connectives take the sup of their arguments

Equations

FirstOrder.Language.BoundedFormulaInf.falsum.qrank = 0
(FirstOrder.Language.BoundedFormulaInf.equal t₁ t₂).qrank = 0
(FirstOrder.Language.BoundedFormulaInf.rel R ts).qrank = 0
(φ.imp ψ).qrank = max φ.qrank ψ.qrank
φ.all.qrank = φ.qrank + 1
(FirstOrder.Language.BoundedFormulaInf.iSup φs).qrank = ⨆ (i : ι), (φs i).qrank
(FirstOrder.Language.BoundedFormulaInf.iInf φs).qrank = ⨆ (i : ι), (φs i).qrank

Instances For

source

@[reducible, inline]

noncomputable abbrev FirstOrder.Language.FormulaInf.qrank {L : Language} {α : Type u_1} (φ : L.FormulaInf α) :

Ordinal.{0}

Quantifier rank of a formula (no bound variables).

Equations

φ.qrank = FirstOrder.Language.BoundedFormulaInf.qrank φ

Instances For

source

@[reducible, inline]

noncomputable abbrev FirstOrder.Language.SentenceInf.qrank {L : Language} (φ : L.SentenceInf) :

Ordinal.{0}

Quantifier rank of a sentence.

Equations

φ.qrank = FirstOrder.Language.BoundedFormulaInf.qrank φ

Instances For

Quantifier Rank Lemmas #

source

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.qrank_falsum {L : Language} {α : Type u_1} {n : ℕ} :

falsum.qrank = 0

source

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.qrank_bot {L : Language} {α : Type u_1} {n : ℕ} :

⊥.qrank = 0

source

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.qrank_equal {L : Language} {α : Type u_1} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) :

(equal t₁ t₂).qrank = 0

source

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.qrank_rel {L : Language} {α : Type u_1} {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_1} {n : ℕ} (φ ψ : L.BoundedFormulaInf α n) :

(φ.imp ψ).qrank = max φ.qrank ψ.qrank

source

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.qrank_all {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormulaInf α (n + 1)) :

φ.all.qrank = φ.qrank + 1

source

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.qrank_iSup {L : Language} {α : Type u_1} {n : ℕ} {ι : Type u_2} (φs : ι → L.BoundedFormulaInf α n) :

(iSup φs).qrank = ⨆ (i : ι), (φs i).qrank

source

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.qrank_iInf {L : Language} {α : Type u_1} {n : ℕ} {ι : Type u_2} (φs : ι → L.BoundedFormulaInf α n) :

(iInf φs).qrank = ⨆ (i : ι), (φs i).qrank

source

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.qrank_top {L : Language} {α : Type u_1} {n : ℕ} :

⊤.qrank = 0

The top formula has rank 0.

source

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.qrank_not {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormulaInf α n) :

φ.not.qrank = φ.qrank

Negation preserves quantifier rank.

source

theorem FirstOrder.Language.BoundedFormulaInf.qrank_and {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormulaInf α n) :

(φ.and ψ).qrank = max φ.qrank ψ.qrank

Conjunction takes max of ranks.

source

theorem FirstOrder.Language.BoundedFormulaInf.qrank_or {L : Language} {α : Type u_1} {n : ℕ} (φ ψ : L.BoundedFormulaInf α n) :

(φ.or ψ).qrank = max φ.qrank ψ.qrank

Disjunction takes max of ranks.

source

theorem FirstOrder.Language.BoundedFormulaInf.qrank_ex {L : Language} {α : Type u_1} {n : ℕ} (φ : L.BoundedFormulaInf α (n + 1)) :

φ.ex.qrank = φ.qrank + 1

Existential quantification adds 1 to rank.

source

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.qrank_mapFreeVars {L : Language} {α α' : Type w'} (f : α → α') {n : ℕ} (φ : L.BoundedFormulaInf α n) :

(mapFreeVars f φ).qrank = φ.qrank

mapFreeVars preserves quantifier rank. Renaming free variables does not change the logical complexity of a formula.

Equivalence up to Quantifier Rank #

source

def FirstOrder.Language.EquivQRInf (L : Language) (α : Ordinal.{0}) (M N : Type w) [L.Structure M] [L.Structure N] :

Prop

Two structures are equivalent up to quantifier rank α if they satisfy the same sentences of quantifier rank ≤ α.

The current definition pins both the ordinal α and the formula universe to Ordinal.{0} and BoundedFormulaInf.{u, v, 0, 0} respectively. This is a practical choice: qrank returns Ordinal.{0}, so the inequality φ.qrank ≤ α requires α : Ordinal.{0}. See LinfEquiv for discussion of the uι = 0 choice.

Equations

L.EquivQRInf α M N = ∀ (φ : L.BoundedFormulaInf Empty 0), φ.qrank ≤ α → (FirstOrder.Language.SentenceInf.Realize φ M ↔ FirstOrder.Language.SentenceInf.Realize φ N)

Instances For

source

theorem FirstOrder.Language.EquivQRInf.refl {L : Language} {M : Type w} [L.Structure M] (α : Ordinal.{0}) :

L.EquivQRInf α M M

Equivalence up to quantifier rank is reflexive.

source

theorem FirstOrder.Language.EquivQRInf.symm {L : Language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] {α : Ordinal.{0}} (h : L.EquivQRInf α M N) :

L.EquivQRInf α N M

Equivalence up to quantifier rank is symmetric.

source

theorem FirstOrder.Language.EquivQRInf.trans {L : Language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] {P : Type w} [L.Structure P] {α : Ordinal.{0}} (h₁ : L.EquivQRInf α M N) (h₂ : L.EquivQRInf α N P) :

L.EquivQRInf α M P

Equivalence up to quantifier rank is transitive.

source

theorem FirstOrder.Language.EquivQRInf.monotone {L : Language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] {α β : Ordinal.{0}} (hαβ : α ≤ β) (h : L.EquivQRInf β M N) :

L.EquivQRInf α M N

Equivalence at higher rank implies equivalence at lower rank.

source

theorem FirstOrder.Language.EquivQRInf.zero_iff_agree_atomic {L : Language} {M : Type w} [L.Structure M] {N : Type w} [L.Structure N] :

L.EquivQRInf 0 M N ↔ ∀ (φ : L.BoundedFormulaInf Empty 0), φ.qrank = 0 → (SentenceInf.Realize φ M ↔ SentenceInf.Realize φ N)

Equivalence at rank 0 means agreement on all quantifier-free sentences.

Universe-correct Equivalence up to Quantifier Rank #

source

def FirstOrder.Language.EquivQRInfW (L : Language) (α : Ordinal.{0}) (M N : Type w) [L.Structure M] [L.Structure N] :

Prop

Equivalence up to quantifier rank α with index types matching the structure universe.

Unlike EquivQRInf which pins uι = 0, this version uses BoundedFormulaInf.{u, v, 0, w} so that index types for iSup/iInf may be any Type w. This is the companion of LinfEquivW for tracking quantifier rank bounds.

Equations