Documentation

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.isolatorSeed {L : Language} {M : Type} [L.Structure M] (hsmall : Lomega1omegaSmall M) :
Set ((n : ℕ) × L.BoundedFormulaω Empty n)

The controlling seed: all isolators, and the existential closures of all isolators of one higher arity.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem FirstOrder.Language.isolatorSeed_countable {L : Language} {M : Type} [L.Structure M] (hsmall : Lomega1omegaSmall M) :
    (isolatorSeed hsmall).Countable
    source
    def FirstOrder.Language.isolatorFragment {L : Language} {M : Type} [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.isolatorFragment_countable {L : Language} {M : Type} [L.Structure M] (hsmall : Lomega1omegaSmall M) :
      (isolatorFragment hsmall).toSet.Countable
      source
      theorem FirstOrder.Language.isolatingFormula_mem_isolatorFragment {L : Language} {M : Type} [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} [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} [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.