Realized-type isolators (issue #17 chunk 1)

The decisive lemma of the small-model → complete-sentence chain, stated LANGUAGE-GENERAL (independent of fragments, Löwenheim–Skolem, Scott infrastructure, and relationality, per the frozen audit): in a structure realizing only countably many complete n-types, every realized type p is ISOLATED AMONG THE REALIZED TYPES by a single L_{ω₁ω}-formula

χ_p = ⋀_{q realized} θ_{p,q},

where θ_{p,q} is an oriented separator (true at realizers of p, false at realizers of q; a membership-difference formula or its negation) and the countable conjunction is ciInf over the countable subtype of realized types. Universes are pinned to Language.{0,0}/Type 0 (ciInf's index universe) — "language-general" means arbitrary function and relation symbols, no relationality assumption. The characterization:

realize_isolatingFormula_iff : χ_p.Realize Empty.elim a ↔ infinitaryType M a = p.

theorem FirstOrder.Language.mem_infinitaryType_iff {L : Language} {M : Type} [L.Structure M] {n : ℕ} {φ : L.BoundedFormulaω Empty n} {a : Fin n → M} : φ ∈ infinitaryType M a ↔ φ.Realize Empty.elim a

theorem FirstOrder.Language.exists_separator {L : Language} {M : Type} [L.Structure M] {n : ℕ} {p q : Set (L.BoundedFormulaω Empty n)} (hne : p ≠ q) : ∃ (θ : L.BoundedFormulaω Empty n), (∀ (a : Fin n → M), infinitaryType M a = p → θ.Realize Empty.elim a) ∧ ∀ (b : Fin n → M), infinitaryType M b = q → ¬θ.Realize Empty.elim b

Oriented separators exist between distinct realized types: a formula true at every realizer of p and false at every realizer of q.

noncomputable def FirstOrder.Language.isolatingFormula {L : Language} {M : Type} [L.Structure M] {n : ℕ} (hcount : (RealizedInfinitaryTypes M n).Countable) (p : Set (L.BoundedFormulaω Empty n)) : L.BoundedFormulaω Empty n

The isolating formula χ_p of a realized type, over a structure with countably many realized n-types: the countable conjunction of the oriented separators against every realized type (a tautology at p itself).

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.realize_isolatingFormula_iff {L : Language} {M : Type} [L.Structure M] {n : ℕ} (hcount : (RealizedInfinitaryTypes M n).Countable) (p : Set (L.BoundedFormulaω Empty n)) (a : Fin n → M) : (isolatingFormula hcount p).Realize Empty.elim a ↔ infinitaryType M a = p

The decisive characterization: χ_p holds at a tuple exactly when its complete type is p.

theorem FirstOrder.Language.exists_realize_isolatingFormula {L : Language} {M : Type} [L.Structure M] {n : ℕ} (hcount : (RealizedInfinitaryTypes M n).Countable) {p : Set (L.BoundedFormulaω Empty n)} (hp : p ∈ RealizedInfinitaryTypes M n) : ∃ (a : Fin n → M), (isolatingFormula hcount p).Realize Empty.elim a

Realizers exist: χ_p is satisfiable in M (by any tuple realizing p).