Iterated Skolemization: the staged language tower and its colimit L^Sk

The bespoke Ehrenfeucht–Mostowski term model needs a language in which every formula's existential has a Skolem function (so the term-model truth lemma can witness nested ∃'s). One layer (skolem₁ω) is not closed under its own witness formulas, so we iterate:

• L₀ = L, L_{k+1} = L_k.sum (skolem₁ω L_k) (skolemStage);
• the colimit L^Sk = colim_k L_k (next) is Skolem-complete: an L^Sk-formula lives at some finite stage k, and its existential's Skolem function appears at stage k+1.

This is ambient infrastructure: the family Γ* consumed by the truth lemma is a countable staged closure inside L^Sk. Caveat: the EM term model's EMContext also needs the full atom diagram over L^Sk, which does enumerate its continuum-many symbols — the reason for the countable family-restricted re-base (localSkolem and the Llocal/Γlocal tower in LocalSkolem.lean/LocalTower.lean); skolemColim is retained as exploratory infrastructure.

For L : Language.{0,0} every stage stays in Type 0 (BoundedFormulaω Empty n over a {0,0} language is Type 0), so the tower has no universe blowup.

def FirstOrder.Language.skolemStage (L : Language) : ℕ → Language

The staged Skolem language tower: skolemStage L 0 = L and skolemStage L (k+1) = (skolemStage L k).sum (skolem₁ω (skolemStage L k)). Each step adjoins a Skolem function symbol for every formula of the previous stage.

Equations

• L.skolemStage 0 = L
• L.skolemStage k.succ = (L.skolemStage k).sum (L.skolemStage k).skolem₁ω

@[simp]

theorem FirstOrder.Language.skolemStage_zero (L : Language) : L.skolemStage 0 = L

@[simp]

theorem FirstOrder.Language.skolemStage_succ (L : Language) (k : ℕ) : L.skolemStage (k + 1) = (L.skolemStage k).sum (L.skolemStage k).skolem₁ω

def FirstOrder.Language.skolemStageHom (L : Language) (k : ℕ) : L.skolemStage k →ᴸ L.skolemStage (k + 1)

The stage-k → stage-(k+1) language embedding: the left injection of the sum. Its onFunction/onRelation carry stage-k symbols into stage-(k+1).

Equations

• L.skolemStageHom k = FirstOrder.Language.LHom.sumInl

Sequential colimit of types

def FirstOrder.Language.DirectedColim (F : ℕ → Type) (φ : (k : ℕ) → F k → F (k + 1)) : Type

The sequential colimit of a tower of types F 0 → F 1 → … along maps φ, as the quotient of Σ k, F k identifying ⟨k, x⟩ with ⟨k+1, φ k x⟩.

Equations

• FirstOrder.Language.DirectedColim F φ = Quot fun (a b : (k : ℕ) × F k) => b = ⟨a.fst + 1, φ a.fst a.snd⟩

def FirstOrder.Language.DirectedColim.incl {F : ℕ → Type} {φ : (k : ℕ) → F k → F (k + 1)} (k : ℕ) (x : F k) : DirectedColim F φ

The canonical inclusion of stage k into the colimit.

Equations

• FirstOrder.Language.DirectedColim.incl k x = Quot.mk (fun (a b : (k : ℕ) × F k) => b = ⟨a.fst + 1, φ a.fst a.snd⟩) ⟨k, x⟩

theorem FirstOrder.Language.DirectedColim.incl_step {F : ℕ → Type} {φ : (k : ℕ) → F k → F (k + 1)} (k : ℕ) (x : F k) : incl (k + 1) (φ k x) = incl k x

Inclusions commute with the tower maps: a stage-k element and its image at stage k+1 have the same colimit class.

The colimit language L^Sk and the stage cocone

def FirstOrder.Language.skolemColim (L : Language) : Language

The iterated-Skolemization colimit language L^Sk = colim_k (skolemStage L k). Its function/relation symbols at each arity are the sequential colimits of the staged symbol types. An L^Sk-symbol lives at a finite stage; in particular every L^Sk-formula's existential acquires a Skolem function at the next stage, so L^Sk is Skolem-complete.

Equations

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

def FirstOrder.Language.skolemStageInclusion (L : Language) (k : ℕ) : L.skolemStage k →ᴸ L.skolemColim

The cocone: the inclusion of stage k into the colimit language L^Sk. On symbols it is the colimit inclusion DirectedColim.incl k.

Equations

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

Stage structures on a fixed model

@[implicit_reducible]

noncomputable def FirstOrder.Language.skolemStageStructure (L : Language) {M : Type} [L.Structure M] [Nonempty M] (k : ℕ) : (L.skolemStage k).Structure M

The stage-k structure on a fixed L-model M: stage 0 is M's own L-structure, and each successor stage adds the Hilbert-choice interpretation of the new Skolem symbols (skolem₁ωStructure) on top of the previous stage, via the sum structure.

Equations

• One or more equations did not get rendered due to their size.
• L.skolemStageStructure 0 = inst✝¹

theorem FirstOrder.Language.skolemStageStructure_funMap_succ (L : Language) {M : Type} [L.Structure M] [Nonempty M] {k m : ℕ} (f : (L.skolemStage k).Functions m) (x : Fin m → M) : Structure.funMap ((L.skolemStageHom k).onFunction f) x = Structure.funMap f x

Stage coherence (functions): a stage-k symbol pushed to stage k+1 interprets the same way. This is the cocone-compatibility witnessing the colimit interpretation is well-defined.

theorem FirstOrder.Language.skolemStageStructure_relMap_succ (L : Language) {M : Type} [L.Structure M] [Nonempty M] {k m : ℕ} (r : (L.skolemStage k).Relations m) (x : Fin m → M) : Structure.RelMap ((L.skolemStageHom k).onRelation r) x = Structure.RelMap r x

Stage coherence (relations).

@[implicit_reducible]

noncomputable def FirstOrder.Language.skolemColimStructure (L : Language) {M : Type} [L.Structure M] [Nonempty M] : L.skolemColim.Structure M

The colimit structure L^Sk-structure on M: a colimit symbol is interpreted through any stage representative, well-defined by the (definitional) stage coherence above.

Equations

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

theorem FirstOrder.Language.skolemStageInclusion_isExpansionOn (L : Language) {M : Type} [L.Structure M] [Nonempty M] (k : ℕ) : (L.skolemStageInclusion k).IsExpansionOn M

The stage inclusion is an expansion: the colimit structure restricts to the stage structure along skolemStageInclusion (the colimit funMap/RelMap on an included symbol computes — by rfl — to the stage interpretation).

theorem FirstOrder.Language.realize_map_stageInclusion (L : Language) {M : Type} [L.Structure M] [Nonempty M] (k : ℕ) {n : ℕ} (φ : (L.skolemStage k).BoundedFormulaω Empty n) (v : Empty → M) (xs : Fin n → M) : (BoundedFormulaω.mapLanguage (L.skolemStageInclusion k) φ).Realize v xs ↔ φ.Realize v xs

Semantic preservation by stage inclusion (deliverable 4): transporting a stage-k formula into L^Sk along skolemStageInclusion preserves its realization in M. Immediate from realize_mapLanguage and the expansion property above.