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

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, FirstOrder.Language.BoundedFormulaInf.imp φ ψ⟩ = {⟨fst, φ⟩, ⟨fst, ψ⟩}
• FirstOrder.Language.bfSubformulas ⟨fst, FirstOrder.Language.BoundedFormulaInf.all φ⟩ = {⟨fst + 1, φ⟩}
• FirstOrder.Language.bfSubformulas ⟨fst, FirstOrder.Language.BoundedFormulaInf.iSup φs⟩ = Set.range fun (k : ℕ) => ⟨fst, φs k⟩
• FirstOrder.Language.bfSubformulas ⟨fst, FirstOrder.Language.BoundedFormulaInf.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.