Documentation

InfinitaryLogic.Scott.Code

Countable Code Layer for Lω₁ω Formulas #

Legacy / off-path. The Scott analysis pipeline was decoupled from the FormulaCode bridge (see the notes around per_tuple_stabilization_below_omega1 in Scott/Sentence.lean), so this module is no longer imported by any library root; it is kept for its public FormulaCode API and is reachable via InfinitaryLogic.Everything.

This file defines a countable code type for Lω₁ω formulas over a countable relational language, and proves the key bridge lemma: if two tuples agree on all codes of bounded quantifier rank, they are BFEquiv.

Main Definitions #

Main Results #

Implementation Notes #

In our Lean formalization, BoundedFormulaω is uncountable (due to ℕ → BoundedFormulaω in iSup/iInf). The FormulaCode type provides a countable proxy: it uses an explicit list structure instead of ℕ → for branching, making the type countable. While FormulaCode cannot represent all Lω₁ω formulas, every Lω₁ω formula (including every Scott formula) is logically equivalent to a conjunction of code-representable formulas, because codes capture all atomic facts and all finite approximations of countable conjunctions/disjunctions.

source
inductive FirstOrder.Language.FormulaCode (L : Language) :
ℕ → Type ((max u v) + 1)

Countable codes for Lω₁ω formulas. Uses an explicit cons/nil list (instead of ℕ →) for conjunctions/disjunctions. The key property is Countable (FormulaCode L n).

Instances For
    source
    inductive FirstOrder.Language.FormulaCodeList (L : Language) :
    ℕ → Type ((max u v) + 1)

    List of formula codes, used for countable conjunctions/disjunctions.

    Instances For
      source
      @[instance_reducible]
      noncomputable instance FirstOrder.Language.FormulaCode.instEncodableSigmaNatRelations {L : Language} [Countable ((l : ℕ) × L.Relations l)] :
      Encodable ((l : ℕ) × L.Relations l)
      Equations
      source
      noncomputable def FirstOrder.Language.FormulaCode.encode {L : Language} [Countable ((l : ℕ) × L.Relations l)] {n : ℕ} :
      L.FormulaCode n → ℕ
      Equations
      Instances For
        source
        noncomputable def FirstOrder.Language.FormulaCode.encodeList {L : Language} [Countable ((l : ℕ) × L.Relations l)] {n : ℕ} :
        L.FormulaCodeList n → ℕ
        Equations
        Instances For
          source
          instance FirstOrder.Language.FormulaCode.instCountable {L : Language} [Countable ((l : ℕ) × L.Relations l)] (n : ℕ) :
          Countable (L.FormulaCode n)
          source
          instance FirstOrder.Language.FormulaCode.instCountableList {L : Language} [Countable ((l : ℕ) × L.Relations l)] (n : ℕ) :
          Countable (L.FormulaCodeList n)
          source
          noncomputable def FirstOrder.Language.FormulaCode.toFormulaω {L : Language} {n : ℕ} :
          L.FormulaCode n → L.Formulaω (Fin n)

          Interpret a code as an actual Lω₁ω formula.

          Equations
          Instances For
            source
            noncomputable def FirstOrder.Language.FormulaCode.toFormulaωList {L : Language} {n : ℕ} :
            L.FormulaCodeList n → List (L.Formulaω (Fin n))

            Interpret a code list as a list of Lω₁ω formulas.

            Equations
            Instances For
              source
              noncomputable def FirstOrder.Language.FormulaCode.Realize {L : Language} {n : ℕ} {N : Type w} [L.Structure N] (c : L.FormulaCode n) (b : Fin n → N) :
              Prop

              Semantics of a code: realized iff its formula interpretation is realized.

              Equations
              Instances For
                source
                theorem FirstOrder.Language.BFEquiv_implies_agree_codes {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) (hBF : BFEquiv α n a b) (c : L.FormulaCode n) (hc : c.toFormulaω.qrank ≤ α) :
                c.Realize a ↔ c.Realize b

                BFEquiv implies agreement on all formula codes of bounded quantifier rank.