Local (family-restricted) Skolem language localSkolem

The full Skolem language skolem₁ω L adjoins a function symbol for every L_{ω₁ω} formula, so it is uncountable (BoundedFormulaω is uncountable). That makes the colimit skolemColim L and its de-substituted atom diagram uncountable, which is fatal for the Ehrenfeucht–Mostowski term model: the extracted tail-indiscernible family Γ would have to be uncountable, but the cheap infinite-Ramsey extraction (MorleyHanfExtractionTail) only produces indiscernibility over a countable family.

The fix is to Skolemize only a countable family Γ of formulas. localSkolem L Γ adjoins one arity-n function symbol per (n+1)-ary formula in Γ. When Γ is countable, localSkolem L Γ is countable — the first ingredient of the countable local Skolem tower Llocal/Γlocal that will re-base the EM term model (keeping skolemColim as exploratory infrastructure).

This file builds the language, its Hilbert-choice structure, and its countability. The mutually recursive language/closure tower is a later chunk.

def FirstOrder.Language.localSkolem (L : Language) (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : Language

The local Skolem language over a family Γ of L-formulas: an arity-n function symbol for each (n+1)-ary formula that lies in Γ (witnessing its last existential), and no relation symbols. Unlike skolem₁ω L (which Skolemizes all formulas and is uncountable), this stays countable whenever Γ is.

Equations

• L.localSkolem Γ = { Functions := fun (n : ℕ) => { φ : L.BoundedFormulaω Empty (n + 1) // ⟨n + 1, φ⟩ ∈ Γ }, Relations := fun (x : ℕ) => Empty }

@[implicit_reducible]

noncomputable instance FirstOrder.Language.localSkolemStructure {L : Language} {M : Type w} [L.Structure M] [Nonempty M] (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : (L.localSkolem Γ).Structure M

The local Skolem structure on M: each symbol (a formula φ of Γ) is interpreted as a Hilbert-choice witness for ∃ xₙ, φ, exactly as in skolem₁ωStructure but only for the symbols of the restricted family.

Equations

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

theorem FirstOrder.Language.localSkolem_funMap_spec {L : Language} {M : Type w} [L.Structure M] [Nonempty M] {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} (φ : (L.localSkolem Γ).Functions n) (x : Fin n → M) (h : ∃ (a : M), (↑φ).Realize Empty.elim (Fin.snoc x a)) : (↑φ).Realize Empty.elim (Fin.snoc x (Structure.funMap φ x))

Local Skolem axiom schema (semantic form). If ∃ a, φ(x, a) holds in M, then the witnessed body φ holds at x extended by the Skolem value funMap φ x. This is Classical.epsilon_spec; the local analogue of skolem₁ω_funMap_spec, powering the local EM term model's Skolem-witness transport.

theorem FirstOrder.Language.localSkolem_functions_countable {L : Language} (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) (hΓ : Γ.Countable) (n : ℕ) : Countable ((L.localSkolem Γ).Functions n)

The arity-n function symbols of localSkolem L Γ are countable when Γ is: each is a formula of Γ, so they inject into ↥Γ.

theorem FirstOrder.Language.localSkolem_sigma_functions_countable {L : Language} (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) (hΓ : Γ.Countable) : Countable ((n : ℕ) × (L.localSkolem Γ).Functions n)

The full (all-arity) function-symbol type of localSkolem L Γ is countable when Γ is.

theorem FirstOrder.Language.localSkolem_sigma_relations_countable {L : Language} (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : Countable ((n : ℕ) × (L.localSkolem Γ).Relations n)

localSkolem L Γ has no relation symbols, so its relation-symbol type is (trivially) countable.