The countable local Skolem tower Llocal / Γlocal

localSkolem L Γ (in LocalSkolem.lean) adjoins a Skolem function symbol only for the formulas of a countable family Γ, and so stays countable. But one layer is not closed under its own witness formulas, so — exactly as skolemStage/skolemColim do for the uncountable full Skolemization — we iterate. Here the family Γ grows in lock-step with the language, so the language and the family are mutually recursive:

• L₀ = L, Γ₀ = the seed family;
• L_{k+1} = L_k.sum (localSkolem L_k (skolemNeed Γ_k)) — adjoin Skolem symbols for the Skolem-need family skolemNeed Γ_k = Γ_k ∪ {¬ψ | ∀ψ ∈ Γ_k}: the EM truth lemma's all case consumes the witness symbol of the negated body ¬ψ (cf. skWitnessStep in SkolemClosure.lean and skWitnessTerm … ψ₀.not in EMTermModel.lean), so Skolemizing Γ_k alone would miss exactly the symbol the rebased truth lemma needs;
• Γ_{k+1} = the subformula/component closure of a seed built from skolemNeed Γ_k (lifted along the language inclusion), the Skolem-witness bodies of the new symbols, and a reserved deForm-closure slot.

The mutual recursion is packaged as one ℕ-indexed sequence of LocalStage bundles (language plus family and countability certificates), sidestepping dependent-recursion sprawl. The deliverable of this chunk is that every stage is countable — both the language's symbol types and the family Γ_k — which is what keeps the eventual local colimit L_Γ countable (the fatal size problem that localSkolem was introduced to fix). The local colimit, its cocone inclusions, and the transported countability live in LocalColimit.lean; here we stop at the tower and its stagewise countability.

Countability of Language.sum symbol types

A sum language's arity-graded symbol type is the fibrewise disjoint sum, so its total Σ-type is countable as soon as both summands' Σ-types are. These feed the successor-language countability certificate in LocalStage.succ.

The local Skolem witness term and formula

For a symbol of localSkolem L Γ — that is, a formula φ ∈ Γ of arity n+1 — the witness body of ∃ xₙ, φ is φ[skolemTerm], built with the template pattern openBounds → subst → relabel exactly as skolemWitnessFormula does in SkolemClosure.lean, but using the local Skolem symbol (which exists precisely because φ ∈ Γ). This is the arity-n formula, over L.sum (localSkolem L Γ), added to the successor family.

def FirstOrder.Language.localSkolemTerm {L : Language} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {γ : Type u_1} {n : ℕ} (sym : (L.localSkolem Γ).Functions n) (ts : Fin n → (L.sum (L.localSkolem Γ)).Term γ) : (L.sum (L.localSkolem Γ)).Term γ

The local Skolem witness term for the symbol sym (a formula φ ∈ Γ of arity n+1): the function symbol sym — in the localSkolem summand — applied to the argument terms ts, as a term of L.sum (localSkolem L Γ). Local analogue of skolemTerm.

Equations

• FirstOrder.Language.localSkolemTerm sym ts = FirstOrder.Language.func (Sum.inr sym) ts

def FirstOrder.Language.localSkolemWitnessFormula {L : Language} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} (sym : (L.localSkolem Γ).Functions n) : (L.sum (L.localSkolem Γ)).BoundedFormulaω Empty n

The local Skolem witness formula for the symbol sym (a formula φ ∈ Γ of arity n+1): substitute the local Skolem term for the witnessed last variable of φ, yielding the arity-n formula φ[skolemTerm] over L.sum (localSkolem L Γ). Local analogue of skolemWitnessFormula.

Equations

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

The Skolem-need family: Γ plus the negated bodies of its universals

The EM truth lemma's all case for ∀ψ uses the Skolem witness of the negation of the body: skWitnessTerm … ψ.not (mirroring skWitnessStep in the full Γ*, which adds the witness body of ¬ψ for every .all ψ). So the successor language must carry a local Skolem symbol for ¬ψ, not just for the members of Γ themselves. skolemNeed Γ is the countable enlargement that provisions exactly these symbols.

def FirstOrder.Language.allNegBody {L : Language} : (n : ℕ) × L.BoundedFormulaω Empty n → Set ((n : ℕ) × L.BoundedFormulaω Empty n)

The negated body contributed by a single family member: a universal ∀ψ (arity n) contributes ¬ψ (arity n+1) — the formula whose local Skolem symbol the EM all-case consumes; every other form contributes nothing.

Equations

• FirstOrder.Language.allNegBody ⟨fst, FirstOrder.Language.BoundedFormulaInf.all ψ⟩ = {⟨fst + 1, ψ.not⟩}
• FirstOrder.Language.allNegBody x✝ = ∅

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

The Skolem-need family: Γ together with the negated bodies of its universal members. This — not Γ itself — is the family the successor stage Skolemizes.

Equations

• FirstOrder.Language.skolemNeed Γ = Γ ∪ ⋃ p ∈ Γ, FirstOrder.Language.allNegBody p

def FirstOrder.Language.skolemNeedSymbol {L : Language} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {ψ : L.BoundedFormulaω Empty (n + 1)} (h : ⟨n, ψ.all⟩ ∈ Γ) : (L.localSkolem (skolemNeed Γ)).Functions n

The local Skolem witness symbol for (the negated body of) a universal family member — the arity-n function symbol of localSkolem L (skolemNeed Γ) witnessing ∃ xₙ, ¬ψ.

Equations

• FirstOrder.Language.skolemNeedSymbol h = ⟨ψ.not, ⋯⟩

Seed of the successor family

The seed of Γ_{k+1} (before the subformula/component closure) has three parts. Each is countable when Γ is, so the whole seed is.

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

The lift of Γ into the successor language L.sum (localSkolem L Γ) along the left injection LHom.sumInl. Arity is preserved.

Equations

• FirstOrder.Language.liftGamma Γ = (fun (p : (n : ℕ) × L.BoundedFormulaω Empty n) => ⟨p.fst, FirstOrder.Language.BoundedFormulaω.mapLanguage FirstOrder.Language.LHom.sumInl p.snd⟩) '' Γ

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

The Skolem-witness seed: the witness formula of every local Skolem symbol. Indexed by the symbol type Σ n, (localSkolem L Γ).Functions n, which is countable when Γ is.

Equations

• FirstOrder.Language.localSkWitnessSeed Γ = Set.range fun (sym : (n : ℕ) × (L.localSkolem Γ).Functions n) => ⟨sym.fst, FirstOrder.Language.localSkolemWitnessFormula sym.snd⟩

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

Reserved deForm-closure seed (placeholder). The truth lemma's family must be closed under the de-substituted formulas deForm S φ ts of its members; but deForm is defined over a term-model carrier J (see EMTermModel.deForm), which does not exist at the pure language-tower level. This named slot is empty until the local colimit and its term model are in place.

Equations

• FirstOrder.Language.deFormSeed Γ = ∅

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

The full seed of the successor family: the lift of Γ, the Skolem-witness bodies, and the reserved deForm slot.

Equations

• FirstOrder.Language.localSeed Γ = FirstOrder.Language.liftGamma Γ ∪ FirstOrder.Language.localSkWitnessSeed Γ ∪ FirstOrder.Language.deFormSeed Γ

The successor family Γ_{k+1}

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

The successor family: the subformula/component closure (setClosure bfSubformulas) of the successor seed. Closing under bfSubformulas makes Γ_{k+1} closed under immediate subformulas and countable-connective components — the structural-induction requirement of the truth lemma — while the Skolem-witness and (reserved) deForm generators sit in the seed.

Equations

• FirstOrder.Language.localGammaNext Γ = FirstOrder.Language.setClosure FirstOrder.Language.bfSubformulas (FirstOrder.Language.localSeed Γ)

The stage bundle and the tower

structure FirstOrder.Language.LocalStage : Type 1

A single stage of the local Skolem tower: a language, a family of its formulas, and countability certificates for the family and the language's symbol types. Bundling these keeps the mutual language/family recursion a plain ℕ-indexed sequence rather than a dependent recursion.

• Lang : Language

  The stage language.

• Gamma : Set ((n : ℕ) × self.Lang.BoundedFormulaω Empty n)

  The stage family of formulas of Lang.

• gamma_countable : self.Gamma.Countable

  The stage family is countable.

• fun_countable : Countable ((n : ℕ) × self.Lang.Functions n)

  The stage language has countably many function symbols.

• rel_countable : Countable ((n : ℕ) × self.Lang.Relations n)

  The stage language has countably many relation symbols.

def FirstOrder.Language.LocalStage.succ (s : LocalStage) : LocalStage

The successor stage: Skolemize the current Skolem-need family (Lang.sum (localSkolem Lang (skolemNeed Gamma)) — skolemNeed so the EM all-case witness symbol for ¬ψ of each ∀ψ ∈ Gamma exists) and replace the family by its successor closure. Every countability certificate is carried forward: the family via localGammaNext_countable, the language via sum_sigma_functions_countable / sum_sigma_relations_countable together with localSkolem's own countability (fed by skolemNeed_countable).

Equations

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

def FirstOrder.Language.localStage (s₀ : LocalStage) : ℕ → LocalStage

The local Skolem tower seeded at s₀: stage 0 is the seed and each successor Skolemizes the current stage.

Equations

• FirstOrder.Language.localStage s₀ 0 = s₀
• FirstOrder.Language.localStage s₀ k.succ = (FirstOrder.Language.localStage s₀ k).succ

Projections consumed by the later local-colimit chunk

def FirstOrder.Language.Llocal (s₀ : LocalStage) (k : ℕ) : Language

The stage-k local language L_k.

Equations

• FirstOrder.Language.Llocal s₀ k = (FirstOrder.Language.localStage s₀ k).Lang

def FirstOrder.Language.Γlocal (s₀ : LocalStage) (k : ℕ) : Set ((n : ℕ) × (Llocal s₀ k).BoundedFormulaω Empty n)

The stage-k local family Γ_k.

Equations

• FirstOrder.Language.Γlocal s₀ k = (FirstOrder.Language.localStage s₀ k).Gamma

def FirstOrder.Language.LlocalHom (s₀ : LocalStage) (k : ℕ) : Llocal s₀ k →ᴸ Llocal s₀ (k + 1)

The stage-k → stage-(k+1) language inclusion: the left injection of the Skolemizing sum. The later colimit's cocone is assembled from these.

Equations

• FirstOrder.Language.LlocalHom s₀ k = FirstOrder.Language.LHom.sumInl

theorem FirstOrder.Language.Γlocal_countable (s₀ : LocalStage) (k : ℕ) : (Γlocal s₀ k).Countable

Each stage-k family is countable.

theorem FirstOrder.Language.Llocal_fun_countable (s₀ : LocalStage) (k : ℕ) : Countable ((n : ℕ) × (Llocal s₀ k).Functions n)

Each stage-k language has countably many function symbols.

theorem FirstOrder.Language.Llocal_rel_countable (s₀ : LocalStage) (k : ℕ) : Countable ((n : ℕ) × (Llocal s₀ k).Relations n)

Each stage-k language has countably many relation symbols.

Family-membership coherence up the tower

theorem FirstOrder.Language.liftGamma_mem_Γlocal_succ (s₀ : LocalStage) {k : ℕ} {p : (n : ℕ) × (Llocal s₀ k).BoundedFormulaω Empty n} (hp : p ∈ Γlocal s₀ k) : ⟨p.fst, BoundedFormulaω.mapLanguage (LlocalHom s₀ k) p.snd⟩ ∈ Γlocal s₀ (k + 1)

Lift stability: a stage-k family member, lifted along the stage inclusion LlocalHom, lies in the successor family (via subset_skolemNeed, the liftGamma part of the seed, and localSeed_subset_localGammaNext).

theorem FirstOrder.Language.bfSubformulas_subset_Γlocal_succ (s₀ : LocalStage) {k : ℕ} {p : (n : ℕ) × (Llocal s₀ (k + 1)).BoundedFormulaω Empty n} (hp : p ∈ Γlocal s₀ (k + 1)) : bfSubformulas p ⊆ Γlocal s₀ (k + 1)

Successor-stage closure: every successor family is closed under immediate subformulas/components (it is a setClosure bfSubformulas).

theorem FirstOrder.Language.liftNegBody_mem_Γlocal_succ (s₀ : LocalStage) {k n : ℕ} {ψ : (Llocal s₀ k).BoundedFormulaω Empty (n + 1)} (h : ⟨n, ψ.all⟩ ∈ Γlocal s₀ k) : ⟨n + 1, BoundedFormulaω.mapLanguage (LlocalHom s₀ k) ψ.not⟩ ∈ Γlocal s₀ (k + 1)

The lift of the negated body of a universal family member is in the successor family (the seed lifts the whole skolemNeed enlargement, not just Γ_k). Feeds the local truth lemma's all case, whose Skolemized body ¬ψ lives one stage up.