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. The difference is that 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 a single ℕ-indexed sequence of LocalStage bundles (language + family + 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.

theorem FirstOrder.Language.sum_sigma_functions_countable {L L' : Language} (h : Countable ((n : ℕ) × L.Functions n)) (h' : Countable ((n : ℕ) × L'.Functions n)) : Countable ((n : ℕ) × (L.sum L').Functions n)

The full function-symbol type of L.sum L' is countable when both summands' are.

theorem FirstOrder.Language.sum_sigma_relations_countable {L L' : Language} (h : Countable ((n : ℕ) × L.Relations n)) (h' : Countable ((n : ℕ) × L'.Relations n)) : Countable ((n : ℕ) × (L.sum L').Relations n)

The full relation-symbol type of L.sum L' is countable when both summands' are.

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, ψ.all⟩ = {⟨fst + 1, ψ.not⟩}
• FirstOrder.Language.allNegBody x✝ = ∅

theorem FirstOrder.Language.allNegBody_countable {L : Language} (p : (n : ℕ) × L.BoundedFormulaω Empty n) : (allNegBody p).Countable

allNegBody is pointwise countable (a singleton on ∀, empty otherwise).

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

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

The Skolem-need family is countable when Γ is.

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

Γ is contained in its Skolem-need family.

theorem FirstOrder.Language.not_mem_skolemNeed_of_all_mem {L : Language} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {ψ : L.BoundedFormulaω Empty (n + 1)} (h : ⟨n, ψ.all⟩ ∈ Γ) : ⟨n + 1, ψ.not⟩ ∈ skolemNeed Γ

The guarantee the EM all-case needs: if ∀ψ ∈ Γ then ¬ψ ∈ skolemNeed Γ, so the local Skolem language over skolemNeed Γ carries a witness symbol for ∃ xₙ, ¬ψ.

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⟩) '' Γ

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

The lift of a countable family is countable (image of a countable set).

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⟩

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

The Skolem-witness seed is countable: it is the range of a map out of the (countable) local Skolem symbol type.

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. So this slot is currently empty and will be filled once the local colimit and its term model are in place. It is named (not left implicit) so the closure and its countability certificate already route through it.

Equations

• FirstOrder.Language.deFormSeed Γ = ∅

theorem FirstOrder.Language.deFormSeed_countable {L : Language} (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : (deFormSeed Γ).Countable

The reserved deForm seed is (trivially) countable.

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 Γ

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

The successor seed is countable when Γ is.

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 Γ)

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

The successor family is countable when Γ is: setClosure of a countable seed under the pointwise-countable subformula step.

theorem FirstOrder.Language.localSeed_subset_localGammaNext {L : Language} (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : localSeed Γ ⊆ localGammaNext Γ

The seed is contained in the successor family.

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

@[simp]

theorem FirstOrder.Language.localStage_zero (s₀ : LocalStage) : localStage s₀ 0 = s₀

@[simp]

theorem FirstOrder.Language.localStage_succ (s₀ : LocalStage) (k : ℕ) : localStage s₀ (k + 1) = (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

@[simp]

theorem FirstOrder.Language.Llocal_zero (s₀ : LocalStage) : Llocal s₀ 0 = s₀.Lang

@[simp]

theorem FirstOrder.Language.Llocal_succ (s₀ : LocalStage) (k : ℕ) : Llocal s₀ (k + 1) = (Llocal s₀ k).sum ((Llocal s₀ k).localSkolem (skolemNeed (Γlocal s₀ k)))

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). Stage 0 — the raw seed — need not be closed, hence the lift wrapper bfSubformulas_lift_subset_Γlocal_succ below.

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

Lift-into-closure wrapper: the subformulas/components of the lift of any stage-k member lie in the (subformula-closed) successor family. Working one stage up always makes closure available, even from the unclosed seed stage.

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.

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

Witness-body membership: for every universal member ∀ψ of the stage-k family, the local Skolem witness body of ¬ψ (built from the skolemNeed symbol) lies in the successor family — the formula the rebased EM truth lemma's all case will need in its readiness data.