Quantifier Rank of Scott Formulas

This file proves bounds on the quantifier rank of Scott formulas and connects BF-equivalence to agreement on Lω₁ω formulas of bounded quantifier rank.

Main Results

• scottFormula_qrank_le: The Scott formula at level α has quantifier rank ≤ α.
• BFEquiv_iff_EquivQRω_formulas: BF-equivalence at level α between tuples is equivalent to agreement on all Lω₁ω formulas of quantifier rank ≤ α (for α < ω₁).

References

• [Mar16]
• [KK04]

theorem FirstOrder.Language.atomicDiagram_qrank_eq_zero {L : Language} [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : (atomicDiagram a).qrank = 0

The atomic diagram has quantifier rank 0.

theorem FirstOrder.Language.qrank_existsLastVar {L : Language} {n : ℕ} (φ : L.Formulaω (Fin (n + 1))) : (existsLastVar φ).qrank = φ.qrank + 1

existsLastVar adds 1 to quantifier rank.

theorem FirstOrder.Language.qrank_forallLastVar {L : Language} {n : ℕ} (φ : L.Formulaω (Fin (n + 1))) : (forallLastVar φ).qrank = φ.qrank + 1

forallLastVar adds 1 to quantifier rank.

theorem FirstOrder.Language.scottFormula_qrank_le {L : Language} [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] [Countable M] {n : ℕ} (a : Fin n → M) (α : Ordinal.{0}) (hα : α < Ordinal.omega 1) : (scottFormula a α).qrank ≤ α

The Scott formula at level α has quantifier rank ≤ α.

This is proved by ordinal induction:

• At level 0: the atomic diagram has rank 0.
• At successor α + 1: the formula at α has rank ≤ α, and the forth/back conditions add one quantifier, giving rank ≤ α + 1.
• At limit λ: the conjunction over β < λ has rank ≤ λ.

theorem FirstOrder.Language.BFEquiv_implies_agree_formulas_omega {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] {n : ℕ} (a : Fin n → M) (b : Fin n → N) (α : Ordinal.{0}) (_hα : α < Ordinal.omega 1) : BFEquiv α n a b → ∀ (φ : L.Formulaω (Fin n)), φ.qrank ≤ α → (φ.Realize a ↔ φ.Realize b)

BF-equivalence at level α implies agreement on Lω₁ω formulas of quantifier rank ≤ α.

This is the carrier-ℕ case of the forward direction of the Karp lemma (BFEquiv_implies_agreeQR). There is no embedding step: L.Formulaω is L.BoundedFormulaInf ℕ and the ω rank is the carrier-generic rank, so specializing the carrier is the whole proof.

theorem FirstOrder.Language.agree_formulas_omega_implies_BFEquiv {L : Language} [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] {n : ℕ} (a : Fin n → M) (b : Fin n → N) (α : Ordinal.{0}) (hα : α < Ordinal.omega 1) : (∀ (φ : L.Formulaω (Fin n)), φ.qrank ≤ α → (φ.Realize a ↔ φ.Realize b)) → BFEquiv α n a b

Agreement on all Lω₁ω formulas of quantifier rank ≤ α implies BF-equivalence.

This direction uses the Scott formula: if all rank-≤-α formulas agree, then in particular the Scott formula at level α agrees, which by realize_scottFormula_iff_BFEquiv gives BFEquiv at level α.

theorem FirstOrder.Language.BFEquiv_iff_agree_formulas_omega {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] {n : ℕ} (a : Fin n → M) (b : Fin n → N) (α : Ordinal.{0}) (hα : α < Ordinal.omega 1) : BFEquiv α n a b ↔ ∀ (φ : L.Formulaω (Fin n)), φ.qrank ≤ α → (φ.Realize a ↔ φ.Realize b)

BF-equivalence at level α between tuples is equivalent to agreement on all Lω₁ω formulas of quantifier rank ≤ α (for α < ω₁).

This is the Lω₁ω version of the Karp lemma.