Documentation

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
      theorem FirstOrder.Language.realize_relabel_insertLastBound_zero {L : Language} {N : Type w'} [L.Structure N] {n : ℕ} (φ : L.Formulaω (Fin (n + 1))) (v : Fin n → N) (xs : Fin 1 → N) :
      (BoundedFormulaω.relabel insertLastBound φ).Realize v xs ↔ φ.Realize (Fin.snoc v (xs 0))

      The key semantics lemma for formulas with 0 bound variables: relabeling with insertLastBound shifts the last free variable to a bound variable position.

      For φ : L.Formulaω (Fin (n+1)) (a formula with n+1 free vars and 0 bound vars):

      • φ.relabel insertLastBound : L.BoundedFormulaω (Fin n) 1 has n free vars and 1 bound var
      • When we evaluate with free var assignment v : Fin n → N and bound var assignment xs : Fin 1 → N, this corresponds to evaluating the original formula with snoc v (xs 0) : Fin (n+1) → N
      source
      theorem FirstOrder.Language.realize_existsLastVar {L : Language} {N : Type w'} [L.Structure N] {n : ℕ} (φ : L.Formulaω (Fin (n + 1))) (v : Fin n → N) :
      (existsLastVar φ).Realize v ↔ ∃ (x : N), φ.Realize (Fin.snoc v x)

      Semantics of existsLastVar: existentially quantifies over the last variable.

      Uses realize_relabel_insertLastBound_zero to show that:

      • existsLastVar φ = (φ.relabel insertLastBound).ex
      • This quantifies existentially over the last (n-th) free variable
      source
      theorem FirstOrder.Language.realize_forallLastVar {L : Language} {N : Type w'} [L.Structure N] {n : ℕ} (φ : L.Formulaω (Fin (n + 1))) (v : Fin n → N) :
      (forallLastVar φ).Realize v ↔ ∀ (x : N), φ.Realize (Fin.snoc v x)

      Semantics of forallLastVar: universally quantifies over the last variable.

      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: