The generated enumeration universe U (issue #8 tranche 2, commit 1)

GenU r₁ r₂ is the countable domain the fair Henkin enumeration runs through: the two roots r₁, r₂, all constant equalities, and all atomic relation instances over constants, closed under the unary C0–C4/quantifier decomposition targets. Per the audit (§6b, §8) it is NOT closed under forming new infinitary conjunctions/disjunctions — only components of existing ones.

Design. The binary atomic closures (equality symmetry/transitivity, relation one-coordinate replacement) are handled by seeding: all constant equalities and all constant atomic relation instances are put in the seed (countably many, using [Countable (Σ l, L.Relations l)]), so those closure targets already lie in U. Only the unary connective / quantifier rules need reachability closure, which admits the component-path countability argument of Fragment.generated_countable.

Acceptance gate (this commit): both roots ∈ U; closure under every C0–C4 decomposition target and under instConst; all constant reflexivity/symmetry/transitivity equalities and atomic relation replacements present; Countable ↥U; every member has finite constant support. The relational-core collapse lemma exists_eq_constTerm (every closed term is a constant) is included — it drives the later term-model plumbing.

The relational-core collapse lemma

theorem FirstOrder.Language.exists_eq_constTerm {L : Language} [L.IsRelational] (t : (L.withConstants ℕ).Term Empty) : ∃ (c : ℕ), t = constTerm c

Collapse (relational core): over a relational base, every closed L[[ℕ]]-term is a constant.

Seeds

def FirstOrder.Language.constTermS {L : Language} (c : ℕ) : (L.withConstants ℕ).Term (Empty ⊕ Fin 0)

A constant as a term inside a sentence (Empty ⊕ Fin 0 variable context).

Equations

• FirstOrder.Language.constTermS c = FirstOrder.Language.func (Sum.inr c) Fin.elim0

theorem FirstOrder.Language.constTerm_relabel_inl {L : Language} (a : ℕ) : Term.relabel Sum.inl (constTerm a) = constTermS a

The closed constant constTerm a, relabeled into the sentence-term context, is constTermS a.

def FirstOrder.Language.constEq {L : Language} (a b : ℕ) : (L.withConstants ℕ).Sentenceω

The constant equality c_a = c_b.

Equations

• FirstOrder.Language.constEq a b = FirstOrder.Language.BoundedFormulaω.equal (FirstOrder.Language.constTermS a) (FirstOrder.Language.constTermS b)

def FirstOrder.Language.relInst {L : Language} {l : ℕ} (R : L.Relations l) (g : Fin l → ℕ) : (L.withConstants ℕ).Sentenceω

The atomic relation instance R(c_{g 0}, …).

Equations

• FirstOrder.Language.relInst R g = FirstOrder.Language.BoundedFormulaω.rel (Sum.inl R) fun (i : Fin l) => FirstOrder.Language.constTermS (g i)

def FirstOrder.Language.seed {L : Language} (r₁ r₂ : (L.withConstants ℕ).Sentenceω) : Set (L.withConstants ℕ).Sentenceω

The seed: the two roots, all constant equalities, all constant atomic relation instances.

Equations

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

Reachability under the unary decomposition rules

inductive FirstOrder.Language.ReachFrom {L : Language} (S : Set (L.withConstants ℕ).Sentenceω) : (L.withConstants ℕ).Sentenceω → Prop

One-step reachability under the unary C0–C4/quantifier decomposition targets.

• base {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {p : (L.withConstants ℕ).Sentenceω} : p ∈ S → ReachFrom S p
• imp_negleft {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {φ ψ : (L.withConstants ℕ).Sentenceω} : ReachFrom S (BoundedFormulaω.imp φ ψ) → ReachFrom S (BoundedFormulaω.not φ)
• imp_right {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {φ ψ : (L.withConstants ℕ).Sentenceω} : ReachFrom S (BoundedFormulaω.imp φ ψ) → ReachFrom S ψ
• negimp_left {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {φ ψ : (L.withConstants ℕ).Sentenceω} : ReachFrom S (BoundedFormulaω.imp φ ψ).not → ReachFrom S φ
• negimp_right {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {φ ψ : (L.withConstants ℕ).Sentenceω} : ReachFrom S (BoundedFormulaω.imp φ ψ).not → ReachFrom S (BoundedFormulaω.not ψ)
• iInf_comp {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) : ReachFrom S (BoundedFormulaω.iInf φs) → ReachFrom S (φs k)
• negiInf_comp {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) : ReachFrom S (BoundedFormulaω.iInf φs).not → ReachFrom S (BoundedFormulaω.not (φs k))
• iSup_comp {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) : ReachFrom S (BoundedFormulaω.iSup φs) → ReachFrom S (φs k)
• negiSup_comp {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) : ReachFrom S (BoundedFormulaω.iSup φs).not → ReachFrom S (BoundedFormulaω.not (φs k))
• all_inst {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (c : ℕ) : ReachFrom S φ.all → ReachFrom S (instConst c φ)
• negall_inst {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (c : ℕ) : ReachFrom S φ.all.not → ReachFrom S (BoundedFormulaω.not (instConst c φ))

def FirstOrder.Language.GenU {L : Language} (r₁ r₂ : (L.withConstants ℕ).Sentenceω) : Set (L.withConstants ℕ).Sentenceω

The generated universe.

Equations

• FirstOrder.Language.GenU r₁ r₂ = {p : (L.withConstants ℕ).Sentenceω | FirstOrder.Language.ReachFrom (FirstOrder.Language.seed r₁ r₂) p}

theorem FirstOrder.Language.root₁_mem {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} : r₁ ∈ GenU r₁ r₂

theorem FirstOrder.Language.root₂_mem {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} : r₂ ∈ GenU r₁ r₂

theorem FirstOrder.Language.constEq_mem {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (a b : ℕ) : constEq a b ∈ GenU r₁ r₂

theorem FirstOrder.Language.eqRefl_mem {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (c : ℕ) : constEq c c ∈ GenU r₁ r₂

theorem FirstOrder.Language.relInst_mem {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {l : ℕ} (R : L.Relations l) (g : Fin l → ℕ) : relInst R g ∈ GenU r₁ r₂

Closure under the decomposition targets

theorem FirstOrder.Language.imp_negleft_mem {L : Language} {r₁ r₂ φ ψ : (L.withConstants ℕ).Sentenceω} (h : BoundedFormulaω.imp φ ψ ∈ GenU r₁ r₂) : BoundedFormulaω.not φ ∈ GenU r₁ r₂

theorem FirstOrder.Language.imp_right_mem {L : Language} {r₁ r₂ φ ψ : (L.withConstants ℕ).Sentenceω} (h : BoundedFormulaω.imp φ ψ ∈ GenU r₁ r₂) : ψ ∈ GenU r₁ r₂

theorem FirstOrder.Language.negimp_left_mem {L : Language} {r₁ r₂ φ ψ : (L.withConstants ℕ).Sentenceω} (h : (BoundedFormulaω.imp φ ψ).not ∈ GenU r₁ r₂) : φ ∈ GenU r₁ r₂

theorem FirstOrder.Language.negimp_right_mem {L : Language} {r₁ r₂ φ ψ : (L.withConstants ℕ).Sentenceω} (h : (BoundedFormulaω.imp φ ψ).not ∈ GenU r₁ r₂) : BoundedFormulaω.not ψ ∈ GenU r₁ r₂

theorem FirstOrder.Language.iInf_comp_mem {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) (h : BoundedFormulaω.iInf φs ∈ GenU r₁ r₂) : φs k ∈ GenU r₁ r₂

theorem FirstOrder.Language.negiInf_comp_mem {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) (h : (BoundedFormulaω.iInf φs).not ∈ GenU r₁ r₂) : BoundedFormulaω.not (φs k) ∈ GenU r₁ r₂

theorem FirstOrder.Language.iSup_comp_mem {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) (h : BoundedFormulaω.iSup φs ∈ GenU r₁ r₂) : φs k ∈ GenU r₁ r₂

theorem FirstOrder.Language.negiSup_comp_mem {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) (h : (BoundedFormulaω.iSup φs).not ∈ GenU r₁ r₂) : BoundedFormulaω.not (φs k) ∈ GenU r₁ r₂

theorem FirstOrder.Language.all_inst_mem {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (c : ℕ) (h : φ.all ∈ GenU r₁ r₂) : instConst c φ ∈ GenU r₁ r₂

theorem FirstOrder.Language.negall_inst_mem {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (c : ℕ) (h : φ.all.not ∈ GenU r₁ r₂) : BoundedFormulaω.not (instConst c φ) ∈ GenU r₁ r₂

Countability of the seed

theorem FirstOrder.Language.countable_relations_each {L : Language} [Countable ((l : ℕ) × L.Relations l)] (l : ℕ) : Countable (L.Relations l)

Countability of the generated universe (component-path encoding)

theorem FirstOrder.Language.genU_countable {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} [Countable ((l : ℕ) × L.Relations l)] : (GenU r₁ r₂).Countable

Countability of U.

Finite constant support

theorem FirstOrder.Language.sentenceJConsts_all {L : Language} (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : sentenceJConsts φ.all = sentenceJConsts φ

theorem FirstOrder.Language.sentenceJConsts_instConst_subset {L : Language} (c : ℕ) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : sentenceJConsts (instConst c φ) ⊆ sentenceJConsts φ.all ∪ {c}

theorem FirstOrder.Language.constTermS_jConsts {L : Language} (c : ℕ) : (constTermS c).jConsts ⊆ {c}

theorem FirstOrder.Language.genU_finite_support {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (hr₁ : (sentenceJConsts r₁).Finite) (hr₂ : (sentenceJConsts r₂).Finite) (p : (L.withConstants ℕ).Sentenceω) : p ∈ GenU r₁ r₂ → (sentenceJConsts p).Finite

Finite constant support: assuming the roots have finite constant support, every member of U does.

Minimality

GenU is the smallest set containing the seed and closed under the unary rules: the generic induction principle for the generated universe. (The current paired construction carries its side-membership bound as an explicit invariant instead of instantiating this principle, so genU_le presently has no in-tree consumer; it is the library-level minimality statement.)