Staged set-closure (generic core for the Skolem-closed family Γ*)

The bespoke EM truth lemma inducts over a countable formula family Γ* that is closed under subformulas, countable-connective components, existential Skolem-witness instances, and the template renamings. This file provides the language-agnostic staged-closure machinery — closing a seed set Γ₀ under a pointwise expansion stepOne : α → Set α via explicit stages (no impredicative least-closure) — together with countability and the consumer-facing closure lemma.

The concrete formula stepOne (subformulas / components / Skolem witnesses / renamings) inside skolemColim L is layered on top in a later chunk; Γ* will be setClosure of that step applied to the lifted EM starting family.

def FirstOrder.Language.iterClosure {α : Type u_1} (stepOne : α → Set α) (Γ₀ : Set α) : ℕ → Set α

Stages of closing Γ₀ under the pointwise expansion stepOne: stage 0 is the seed, each successor adds stepOne x for every x already present. Increasing by construction.

Equations

• FirstOrder.Language.iterClosure stepOne Γ₀ 0 = Γ₀
• FirstOrder.Language.iterClosure stepOne Γ₀ k.succ = FirstOrder.Language.iterClosure stepOne Γ₀ k ∪ ⋃ x ∈ FirstOrder.Language.iterClosure stepOne Γ₀ k, stepOne x

def FirstOrder.Language.setClosure {α : Type u_1} (stepOne : α → Set α) (Γ₀ : Set α) : Set α

The staged closure of Γ₀ under stepOne: the union over all finite stages.

Equations

• FirstOrder.Language.setClosure stepOne Γ₀ = ⋃ (k : ℕ), FirstOrder.Language.iterClosure stepOne Γ₀ k

theorem FirstOrder.Language.subset_setClosure {α : Type u_1} (stepOne : α → Set α) (Γ₀ : Set α) : Γ₀ ⊆ setClosure stepOne Γ₀

The seed is contained in the closure (it is stage 0).

theorem FirstOrder.Language.stepOne_subset_setClosure {α : Type u_1} (stepOne : α → Set α) (Γ₀ : Set α) {x : α} (hx : x ∈ setClosure stepOne Γ₀) : stepOne x ⊆ setClosure stepOne Γ₀

Closure property (consumer-facing): the expansion of any member stays in the closure. If x ∈ Γ* then stepOne x ⊆ Γ*.

theorem FirstOrder.Language.iterClosure_countable {α : Type u_1} (stepOne : α → Set α) {Γ₀ : Set α} (hΓ₀ : Γ₀.Countable) (hstep : ∀ (x : α), (stepOne x).Countable) (k : ℕ) : (iterClosure stepOne Γ₀ k).Countable

Each stage is countable, given a countable seed and a pointwise-countable step.

theorem FirstOrder.Language.setClosure_countable {α : Type u_1} (stepOne : α → Set α) {Γ₀ : Set α} (hΓ₀ : Γ₀.Countable) (hstep : ∀ (x : α), (stepOne x).Countable) : (setClosure stepOne Γ₀).Countable

The closure is countable, given a countable seed and a pointwise-countable step.

Subformula / connective-component step (any language)

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

Immediate subformulas and countable-connective components of a formula, over any language: imp gives both parts, all gives the body (one higher arity), iSup/iInf give all countably-many components, and the atomic forms give none.

Equations

• FirstOrder.Language.bfSubformulas ⟨fst, φ.imp ψ⟩ = {⟨fst, φ⟩, ⟨fst, ψ⟩}
• FirstOrder.Language.bfSubformulas ⟨fst, φ.all⟩ = {⟨fst + 1, φ⟩}
• FirstOrder.Language.bfSubformulas ⟨fst, FirstOrder.Language.BoundedFormulaω.iSup φs⟩ = Set.range fun (k : ℕ) => ⟨fst, φs k⟩
• FirstOrder.Language.bfSubformulas ⟨fst, FirstOrder.Language.BoundedFormulaω.iInf φs⟩ = Set.range fun (k : ℕ) => ⟨fst, φs k⟩
• FirstOrder.Language.bfSubformulas x✝ = ∅

theorem FirstOrder.Language.bfSubformulas_countable {Λ : Language} (χ : (n : ℕ) × Λ.BoundedFormulaω Empty n) : (bfSubformulas χ).Countable

bfSubformulas is pointwise countable.

Staged formulas and the colimit projection

@[reducible, inline]

abbrev FirstOrder.Language.ColimFormula (L : Language) : Type

A colimit-language formula packaged with its arity.

Equations

• L.ColimFormula = ((n : ℕ) × L.skolemColim.BoundedFormulaω Empty n)

@[reducible, inline]

abbrev FirstOrder.Language.SkFormula (L : Language) : Type

A formula tagged with the finite language stage at which it lives. The closure works at this staged level — so the existential-witness Skolem term is directly available at the next stage — and projects to a colimit formula only via toColimFormula. This avoids ever inverting the colimit quotient.

Equations

• L.SkFormula = ((k : ℕ) × (n : ℕ) × (L.skolemStage k).BoundedFormulaω Empty n)

def FirstOrder.Language.toColimFormula (L : Language) : L.SkFormula → L.ColimFormula

Project a staged formula to a colimit-language formula, transporting along the stage inclusion skolemStageInclusion L k. Γ* in the colimit language is the image of the staged closure under this map.

Equations

• L.toColimFormula ⟨k, ⟨n, φ⟩⟩ = ⟨n, FirstOrder.Language.BoundedFormulaω.mapLanguage (L.skolemStageInclusion k) φ⟩

def FirstOrder.Language.skSubStep (L : Language) : L.SkFormula → Set L.SkFormula

The subformula/component step at the staged level: take bfSubformulas of the stage-k formula, keeping the stage k fixed.

Equations

• L.skSubStep ⟨k, χ⟩ = (fun (p : (n : ℕ) × (L.skolemStage k).BoundedFormulaω Empty n) => ⟨k, p⟩) '' FirstOrder.Language.bfSubformulas χ

theorem FirstOrder.Language.skSubStep_countable (L : Language) (χ : L.SkFormula) : (L.skSubStep χ).Countable

The staged subformula step is pointwise countable.

Existential Skolem-witness step (stage k → k+1)

def FirstOrder.Language.skolemWitnessFormula (L : Language) {k n : ℕ} (ψ : (L.skolemStage k).BoundedFormulaω Empty (n + 1)) : (L.skolemStage (k + 1)).BoundedFormulaω Empty n

The Skolem-witness body of ∃x ψ (with ψ the (n+1)-ary matrix at stage k): substitute the stage-(k+1) Skolem term skolemTerm ψ (of the remaining n variables) for the witnessed variable. Built with the template substitution pattern openBounds → subst → relabel, placing the Skolem term in the last slot. Lives at stage k+1 and arity n.

Equations

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

def FirstOrder.Language.skWitnessStep (L : Language) : L.SkFormula → Set L.SkFormula

The Skolem-witness step: Skolemize the (primitive) universal quantifier. For ∀x φ at stage k, add the witness body of its negation ∃x ¬φ, namely (¬φ)[skolemTerm (¬φ)], at stage k+1. Since ∃xψ = ¬∀x¬ψ, this covers existentials too. Other forms add nothing.

Equations

• L.skWitnessStep ⟨k, ⟨n, φ.all⟩⟩ = {⟨k + 1, ⟨n, L.skolemWitnessFormula φ.not⟩⟩}
• L.skWitnessStep x✝ = ∅

theorem FirstOrder.Language.skWitnessStep_countable (L : Language) (χ : L.SkFormula) : (L.skWitnessStep χ).Countable

The Skolem-witness step is pointwise countable (a singleton on ∀, empty otherwise).

The Skolem-closed staged family Γ*

def FirstOrder.Language.skStep (L : Language) (χ : L.SkFormula) : Set L.SkFormula

The full staged closure step: subformulas/components together with Skolem witnesses. (Template renamings are added where the truth lemma needs them, in a later chunk.)

Equations

• L.skStep χ = L.skSubStep χ ∪ L.skWitnessStep χ

theorem FirstOrder.Language.skStep_countable (L : Language) (χ : L.SkFormula) : (L.skStep χ).Countable

def FirstOrder.Language.Γstar (L : Language) (Γ₀ : Set L.SkFormula) : Set L.SkFormula

The Skolem-closed staged family generated by a seed set of staged formulas.

Equations

• L.Γstar Γ₀ = FirstOrder.Language.setClosure L.skStep Γ₀

theorem FirstOrder.Language.Γstar_countable (L : Language) {Γ₀ : Set L.SkFormula} (hΓ₀ : Γ₀.Countable) : (L.Γstar Γ₀).Countable

Γ* is countable when the seed is.

theorem FirstOrder.Language.subset_Γstar (L : Language) (Γ₀ : Set L.SkFormula) : Γ₀ ⊆ L.Γstar Γ₀

The seed is contained in Γ*.

theorem FirstOrder.Language.skStep_subset_Γstar (L : Language) {Γ₀ : Set L.SkFormula} {χ : L.SkFormula} (hχ : χ ∈ L.Γstar Γ₀) : L.skStep χ ⊆ L.Γstar Γ₀

Closure property of Γ*: the full step of any member stays in Γ*.

theorem FirstOrder.Language.skSubStep_subset_Γstar (L : Language) {Γ₀ : Set L.SkFormula} {χ : L.SkFormula} (hχ : χ ∈ L.Γstar Γ₀) : L.skSubStep χ ⊆ L.Γstar Γ₀

Subformulas/components of a Γ* member stay in Γ*.

theorem FirstOrder.Language.skWitnessStep_subset_Γstar (L : Language) {Γ₀ : Set L.SkFormula} {χ : L.SkFormula} (hχ : χ ∈ L.Γstar Γ₀) : L.skWitnessStep χ ⊆ L.Γstar Γ₀

The Skolem witness of a Γ* member stays in Γ*.

Colimit image and enumeration

theorem FirstOrder.Language.toColimFormula_image_Γstar_countable (L : Language) {Γ₀ : Set L.SkFormula} (hΓ₀ : Γ₀.Countable) : (L.toColimFormula '' L.Γstar Γ₀).Countable

The colimit-language image of Γ* is countable.

theorem FirstOrder.Language.exists_ΓEnum (L : Language) {Γ₀ : Set L.SkFormula} (hΓ₀ : Γ₀.Countable) (hne : (L.toColimFormula '' L.Γstar Γ₀).Nonempty) : ∃ (ΓEnum : ℕ → L.ColimFormula), L.toColimFormula '' L.Γstar Γ₀ = Set.range ΓEnum

An enumeration of Γ*'s colimit image as a sequence ℕ → ColimFormula L, suitable as the formula family fed to morleyHanfExtractionTail_holds (whose extraction yields tail-indiscernibility on Set.range). Exists since the image is countable and nonempty.