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.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.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.

The successor family Γ_{k+1}

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.