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.seed_subset_genU {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} : seed r₁ r₂ ⊆ GenU r₁ r₂

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)

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

Countability of the generated universe (component-path encoding)

def FirstOrder.Language.uStep {L : Language} (p : (L.withConstants ℕ).Sentenceω) (c : ℕ × ℕ) : Option (L.withConstants ℕ).Sentenceω

One decomposition step, coded by (tag, index). Matching on the tag first keeps the step reducible on concrete members (the sentence discriminant is inspected only after the tag has already selected the intended rule).

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.uStep (FirstOrder.Language.BoundedFormulaInf.imp φ ψ) c = some φ.not
• FirstOrder.Language.uStep (FirstOrder.Language.BoundedFormulaInf.imp φ ψ) c = some ψ
• FirstOrder.Language.uStep ((FirstOrder.Language.BoundedFormulaInf.imp φ ψ).imp FirstOrder.Language.BoundedFormulaInf.falsum) c = some φ
• FirstOrder.Language.uStep ((FirstOrder.Language.BoundedFormulaInf.imp φ ψ).imp FirstOrder.Language.BoundedFormulaInf.falsum) c = some ψ.not
• FirstOrder.Language.uStep (FirstOrder.Language.BoundedFormulaInf.iInf φs) c = some (φs c.2)
• FirstOrder.Language.uStep ((FirstOrder.Language.BoundedFormulaInf.iInf φs).imp FirstOrder.Language.BoundedFormulaInf.falsum) c = some (φs c.2).not
• FirstOrder.Language.uStep (FirstOrder.Language.BoundedFormulaInf.iSup φs) c = some (φs c.2)
• FirstOrder.Language.uStep ((FirstOrder.Language.BoundedFormulaInf.iSup φs).imp FirstOrder.Language.BoundedFormulaInf.falsum) c = some (φs c.2).not
• FirstOrder.Language.uStep (FirstOrder.Language.BoundedFormulaInf.all φ) c = some (FirstOrder.Language.instConst c.2 φ)
• FirstOrder.Language.uStep p✝ c = none

def FirstOrder.Language.uPath {L : Language} (p : (L.withConstants ℕ).Sentenceω) : List (ℕ × ℕ) → Option (L.withConstants ℕ).Sentenceω

Iterated steps along a list of codes.

Equations

• FirstOrder.Language.uPath p [] = some p
• FirstOrder.Language.uPath p (c :: l) = (FirstOrder.Language.uStep p c).bind fun (x : (L.withConstants ℕ).Sentenceω) => FirstOrder.Language.uPath x l

theorem FirstOrder.Language.uPath_append {L : Language} (p : (L.withConstants ℕ).Sentenceω) (l₁ l₂ : List (ℕ × ℕ)) : uPath p (l₁ ++ l₂) = (uPath p l₁).bind fun (x : (L.withConstants ℕ).Sentenceω) => uPath x l₂

theorem FirstOrder.Language.ReachFrom.of_uStep {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {q p : (L.withConstants ℕ).Sentenceω} {c : ℕ × ℕ} (hq : ReachFrom S q) (h : uStep q c = some p) : ReachFrom S p

A single coded step lands inside the reachability set.

theorem FirstOrder.Language.reachFrom_iff_path {L : Language} {S : Set (L.withConstants ℕ).Sentenceω} {p : (L.withConstants ℕ).Sentenceω} : ReachFrom S p ↔ ∃ s ∈ S, ∃ (l : List (ℕ × ℕ)), uPath s l = some p

The path characterization: ReachFrom S is exactly what is reachable from S by finitely many coded steps.

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

theorem FirstOrder.Language.genU_le {L : Language} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {P : Set (L.withConstants ℕ).Sentenceω} (hseed : seed r₁ r₂ ⊆ P) (himp_negleft : ∀ {φ ψ : (L.withConstants ℕ).Sentenceω}, BoundedFormulaω.imp φ ψ ∈ P → BoundedFormulaω.not φ ∈ P) (himp_right : ∀ {φ ψ : (L.withConstants ℕ).Sentenceω}, BoundedFormulaω.imp φ ψ ∈ P → ψ ∈ P) (hnegimp_left : ∀ {φ ψ : (L.withConstants ℕ).Sentenceω}, (BoundedFormulaω.imp φ ψ).not ∈ P → φ ∈ P) (hnegimp_right : ∀ {φ ψ : (L.withConstants ℕ).Sentenceω}, (BoundedFormulaω.imp φ ψ).not ∈ P → BoundedFormulaω.not ψ ∈ P) (hiInf : ∀ {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ), BoundedFormulaω.iInf φs ∈ P → φs k ∈ P) (hnegiInf : ∀ {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ), (BoundedFormulaω.iInf φs).not ∈ P → BoundedFormulaω.not (φs k) ∈ P) (hiSup : ∀ {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ), BoundedFormulaω.iSup φs ∈ P → φs k ∈ P) (hnegiSup : ∀ {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ), (BoundedFormulaω.iSup φs).not ∈ P → BoundedFormulaω.not (φs k) ∈ P) (hall : ∀ {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (c : ℕ), φ.all ∈ P → instConst c φ ∈ P) (hnegall : ∀ {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (c : ℕ), φ.all.not ∈ P → BoundedFormulaω.not (instConst c φ) ∈ P) : GenU r₁ r₂ ⊆ P