Documentation

LeanPool.InfinitaryLogic.Scott.Formula

Scott Formulas #

This file defines Scott formulas, which are Lω₁ω formulas that capture back-and-forth equivalence at each ordinal level.

Main Definitions #

Main Results #

Implementation Notes #

The Scott formula at ordinal α is defined by recursion on α:

For the forth and back conditions, we need to quantify over elements of M, which requires [Countable M] to form the countable conjunction/disjunction.

The key technical challenge is handling the variable binding correctly. When we have a formula φ(x₀,...,xₙ) with n+1 free variables and want to existentially quantify over the last variable, we use relabel to move it into a bound position.

source
def FirstOrder.Language.existsLastVar {L : Language} {n : ℕ} (φ : L.Formulaω (Fin (n + 1))) :
L.Formulaω (Fin n)

Existentially quantify over the last free variable of a formula.

Equations
Instances For
    source
    def FirstOrder.Language.forallLastVar {L : Language} {n : ℕ} (φ : L.Formulaω (Fin (n + 1))) :
    L.Formulaω (Fin n)

    Universally quantify over the last free variable of a formula.

    Equations
    Instances For
      source
      noncomputable def FirstOrder.Language.scottFormula {L : Language} {M : Type w} [L.Structure M] [Countable ((l : ℕ) × L.Relations l)] [Countable M] {n : ℕ} (a : Fin n → M) (α : Ordinal.{u_1}) :
      L.Formulaω (Fin n)

      The Scott formula for a tuple a at ordinal level α.

      At level 0: the atomic diagram of a. At successor α + 1: formula at α ∧ (forth condition) ∧ (back condition) At limit λ: conjunction over all β < λ.

      The formula has free variables indexed by Fin n (representing the positions in the tuple). Requires [Countable M] to quantify over elements of M in the forth/back conditions.

      The definition uses Ordinal.limitRecOn with a motive that is constant in the ordinal (always (n : ℕ) → (Fin n → M) → L.Formulaω (Fin n)), allowing uniform treatment of tuples of different lengths in the recursion.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem FirstOrder.Language.scottFormula_zero {L : Language} {M : Type w} [L.Structure M] [Countable ((l : ℕ) × L.Relations l)] [Countable M] {n : ℕ} (a : Fin n → M) :
        scottFormula a 0 = atomicDiagram a
        source
        theorem FirstOrder.Language.scottFormula_succ {L : Language} {M : Type w} [L.Structure M] [Countable ((l : ℕ) × L.Relations l)] [Countable M] {n : ℕ} (a : Fin n → M) (α : Ordinal.{u_1}) :
        scottFormula a (Order.succ α) = (scottFormula a α ⊓ BoundedFormulaω.einf fun (m : M) => existsLastVar (scottFormula (Fin.snoc a m) α)) ⊓ forallLastVar (BoundedFormulaω.esup fun (m : M) => scottFormula (Fin.snoc a m) α)
        source
        theorem FirstOrder.Language.realize_scottFormula_iff_BFEquiv {L : Language} {M : Type w} [L.Structure M] [Countable ((l : ℕ) × L.Relations l)] [Countable M] {N : Type w'} [L.Structure N] {n : ℕ} (a : Fin n → M) (b : Fin n → N) (α : Ordinal.{u_1}) (hα : α < Ordinal.omega 1) :
        (scottFormula a α).Realize b ↔ BFEquiv α n a b

        The fundamental correspondence: a tuple b realizes the Scott formula for a at level α if and only if a and b are BF-equivalent at level α.

        Important: This theorem only holds for α < ω₁. For α ≥ ω₁, scottFormula returns ⊤ (which is always realized) while BFEquiv may fail, so the equivalence breaks down. For Scott analysis of countable structures, we only use ordinals < ω₁.

        The proof proceeds by ordinal induction using limitRecOn:

        • Zero case: follows from sameAtomicType_iff_realize_atomicDiagram
        • Successor case: uses realize_existsLastVar and realize_forallLastVar
        • Limit case: uses realize_einf