Documentation

LeanPool.InfinitaryLogic.ModelTheory.CountableCompanion

The controlling fragment and the countable companion (issue #17 chunk 2) #

One countable seed controls the whole back-and-forth: over every arity it contains each isolating formula χ_p of a realized type, and the one-variable existential closure (χ_p).ex of every (n+1)-ary isolator (BoundedFormulaω.ex is ¬∀¬, and realize_ex quantifies exactly the coordinate added by Fin.snoc — no renaming formulas are needed). The component-closed fragment it generates is countable, and the genuine downward Löwenheim–Skolem theorem (#13) yields the countable companion N ≺_A M.

Still language-general (countable function symbols only — relationality first enters at the BF/Scott packaging boundary, per the frozen audit).

source
def FirstOrder.Language.isolatorFragment {L : Language} {M : Type w} [L.Structure M] (hsmall : Lomega1omegaSmall M) :
L.Fragment

The controlling fragment: the component-closed fragment generated by the seed.

Equations
Instances For
    source
    theorem FirstOrder.Language.isolatingFormula_mem_isolatorFragment {L : Language} {M : Type w} [L.Structure M] (hsmall : Lomega1omegaSmall M) {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} (hp : p ∈ RealizedInfinitaryTypes M n) :
    ⟨n, isolatingFormula ⋯ p⟩ ∈ (isolatorFragment hsmall).toSet
    source
    theorem FirstOrder.Language.isolatingFormula_ex_mem_isolatorFragment {L : Language} {M : Type w} [L.Structure M] (hsmall : Lomega1omegaSmall M) {n : ℕ} {p : Set (L.BoundedFormulaω Empty (n + 1))} (hp : p ∈ RealizedInfinitaryTypes M (n + 1)) :
    ⟨n, (isolatingFormula ⋯ p).ex⟩ ∈ (isolatorFragment hsmall).toSet
    source
    theorem FirstOrder.Language.exists_countable_companion {L : Language} {M : Type w} [L.Structure M] [Countable ((n : ℕ) × L.Functions n)] (hsmall : Lomega1omegaSmall M) :
    ∃ (N : L.Substructure M), Countable ↥N ∧ AElementary (isolatorFragment hsmall) N.subtype

    The countable companion (issue #17 chunk 2 endpoint): a small structure over countably many function symbols has a countable substructure that is elementary for the controlling fragment.