L_{ω₁ω} Skolem functions

Infinitary analogue of Mathlib's Language.skolem₁: a Skolem function symbol for each L_{ω₁ω} formula ψ(x₀, …, x_{n-1}, x_n), interpreted by Hilbert choice to witness ∃ x_n, ψ. This is the ambient one-layer Skolem language iterated by the skolemStage/skolemColim tower (SkolemColimit.lean) and consumed by the Ehrenfeucht–Mostowski term model (EMTermModel.lean), whose Skolem-witness transport (skWitness_universal) is powered by skolem₁ω_funMap_spec. Note skolem₁ω L is uncountable (a symbol per BoundedFormulaω); the countable family-restricted variant is localSkolem (LocalSkolem.lean), which adjoins symbols only for a countable family Γ and is the basis of the Llocal/Γlocal re-base.

Only ∃ is Skolemized here. The countable connectives ⋁/⋀ are not given object-language selectors — witnessing them is external (the EM term model's OmegaComplete mixin). So this layer adds function symbols only; iSup/iInf are untouched.

Main definitions

• skolem₁ω L — the Skolem language (arity-n symbol per L.BoundedFormulaω Empty (n+1)).
• skolem₁ωStructure — the Hilbert-choice interpretation on any L-structure.
• skolemTerm ψ ts — the Skolem witness term in L.sum (skolem₁ω L).

Main result

• skolem₁ω_funMap_spec — the Skolem axiom schema (semantic form): if ∃ a, ψ(x, a) then ψ holds at x extended by the Skolem value. Consumed by the EM term model's skWitness_universal (the all-case Skolem input of truthLemmaStage).

def FirstOrder.Language.skolem₁ω (L : Language) : Language

The L_{ω₁ω} Skolem language: an arity-n function symbol for every formula ψ : L.BoundedFormulaω Empty (n+1) (to witness the last variable x_n), and no relation symbols. Infinitary analogue of Language.skolem₁.

Equations

• L.skolem₁ω = { Functions := fun (n : ℕ) => L.BoundedFormulaω Empty (n + 1), Relations := fun (x : ℕ) => Empty }

@[implicit_reducible]

noncomputable instance FirstOrder.Language.skolem₁ωStructure {L : Language} {M : Type w} [L.Structure M] [Nonempty M] : L.skolem₁ω.Structure M

The Skolem structure on M: each Skolem symbol ψ is interpreted as a Hilbert-choice witness for ∃ x_n, ψ(x, x_n) (junk choice when no witness exists).

Equations

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

def FirstOrder.Language.skolemTerm {L : Language} {γ : Type u'} {n : ℕ} (ψ : L.BoundedFormulaω Empty (n + 1)) (ts : Fin n → (L.sum L.skolem₁ω).Term γ) : (L.sum L.skolem₁ω).Term γ

The Skolem witness term for ∃ x_n, ψ(ts, x_n): the Skolem function symbol ψ (in the skolem₁ω summand) applied to the argument terms ts, as a term of L.sum (skolem₁ω L).

Equations

• FirstOrder.Language.skolemTerm ψ ts = FirstOrder.Language.func (Sum.inr ψ) ts

theorem FirstOrder.Language.skolem₁ω_funMap_spec {L : Language} {M : Type w} [L.Structure M] [Nonempty M] {n : ℕ} (ψ : L.BoundedFormulaω Empty (n + 1)) (x : Fin n → M) (h : ∃ (a : M), ψ.Realize Empty.elim (Fin.snoc x a)) : ψ.Realize Empty.elim (Fin.snoc x (Structure.funMap ψ x))

Skolem axiom schema (semantic form). If ∃ a, ψ(x, a) holds in M, then ψ holds at x extended by the Skolem value funMap ψ x. This is Classical.epsilon_spec; it is exactly what lets the C7 quantifier-witness rule be discharged by a skolemTerm.

Syntactic-to-semantic bridge: the Skolem term realizes to the chosen witness

These connect the syntactic skolemTerm to the semantic Skolem function of skolem₁ωStructure. Currently unused API: the envisioned consistency-property consumer (a C7 quantifier-witness discharge) never materialized — the live consumer of this file is the EM term model, which uses skolem₁ω_funMap_spec directly. Kept as the natural entry points for any future syntactic Skolemization.

theorem FirstOrder.Language.realize_skolemTerm {L : Language} {M : Type w} [L.Structure M] [Nonempty M] {γ : Type u'} {n : ℕ} (ψ : L.BoundedFormulaω Empty (n + 1)) (ts : Fin n → (L.sum L.skolem₁ω).Term γ) (v : γ → M) : Term.realize v (skolemTerm ψ ts) = Structure.funMap ψ fun (i : Fin n) => Term.realize v (ts i)

The syntactic Skolem term evaluates to the semantic Skolem function value: realizing skolemTerm ψ ts under v is funMap ψ applied to the realized arguments. Definitional, via Term.realize_func and funMap_sumInr.

theorem FirstOrder.Language.exists_witness_skolemTerm {L : Language} {M : Type w} [L.Structure M] [Nonempty M] {γ : Type u'} {n : ℕ} (ψ : L.BoundedFormulaω Empty (n + 1)) (ts : Fin n → (L.sum L.skolem₁ω).Term γ) (v : γ → M) (h : ∃ (a : M), ψ.Realize Empty.elim (Fin.snoc (fun (i : Fin n) => Term.realize v (ts i)) a)) : ψ.Realize Empty.elim (Fin.snoc (fun (i : Fin n) => Term.realize v (ts i)) (Term.realize v (skolemTerm ψ ts)))

Skolem witness lemma (currently unused). If, under the assignment given by ts, the formula ψ has a witness for its last variable, then the Skolem term skolemTerm ψ ts is such a witness: ψ holds at the realized arguments extended by the realized Skolem term.