Fair enumeration for a fragment-relative consistency property (issue #8 tranche 2, commit 3)

Generic over a universe U and a ConsistencyPropertyEqOn U: a finite consistent S₀ ⊆ U extends to a Henkin-complete S* ⊇ S₀. The schedule is a prefix sweep — stage (n+1) processes requests 0,…,n starting from stage n — so, given a surjection e : ℕ → Request U, each request e k is processed during every sweep after k (fairness with no arithmetic about Nat.pair), while each sweep adds only finitely many sentences.

Branching / witness rules make a classical choice at the moment the request fires; the triggering sentence stays present, so re-processing is harmless. The union S* is never claimed to be in C.sets (Finding 1) — only that each closure target cohabits a later stage.

The remaining piece (the HenkinComplete Sstar acceptance theorem) is the per-field limit proof; it consumes request_fires_after plus per-request "what process adds" facts.

inductive FirstOrder.Language.Request {L : Language} (U : Set (L.withConstants ℕ).Sentenceω) : Type

A scheduling request. Decomposition rules dispatch on the trigger's outermost shape; idx supplies the per-index parameter (component / instance / which negated-implication conclusion) and is ignored by the classical-choice rules.

• decompose {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} (t : ↑U) (idx : ℕ) : Request U
• impC1 {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} (t : ↑U) : Request U
• eqRefl {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) : Request U
• eqSymm {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} (a b : ℕ) : Request U
• eqTrans {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} (a b d : ℕ) : Request U
• relCongr {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} (l : ℕ) (R : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ) : Request U

instance FirstOrder.Language.Request.instCountable {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} [Countable ↑U] [Countable ((l : ℕ) × L.Relations l)] : Countable (Request U)

The request type is countable when U and the relation symbols are.

One processing step

@[reducible, inline]

abbrev FirstOrder.Language.SetIn {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} (P : ConsistencyPropertyEqOn U) : Type

A member of the consistency family, bundled with its membership proof.

Equations

• FirstOrder.Language.SetIn P = { T : Set (L.withConstants ℕ).Sentenceω // T ∈ P.sets }

The prefix-sweep schedule

noncomputable def FirstOrder.Language.stage {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (S₀ : SetIn P) : ℕ → SetIn P

stage (n+1) processes requests 0,…,n starting from stage n.

Equations

• FirstOrder.Language.stage e S₀ 0 = S₀
• FirstOrder.Language.stage e S₀ n.succ = FirstOrder.Language.sweep✝ e (FirstOrder.Language.stage e S₀ n) n

noncomputable def FirstOrder.Language.Sstar {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (S₀ : SetIn P) : Set (L.withConstants ℕ).Sentenceω

The limit of the enumeration.

Equations

• FirstOrder.Language.Sstar e S₀ = ⋃ (n : ℕ), ↑(FirstOrder.Language.stage e S₀ n)

The firing API

What each firing adds (process specs)

The limit is Henkin-complete

theorem FirstOrder.Language.exists_henkinComplete {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (S₀ : SetIn P) [Countable ↑U] [Countable ((l : ℕ) × L.Relations l)] : ∃ (Sstar : Set (L.withConstants ℕ).Sentenceω), ↑S₀ ⊆ Sstar ∧ Sstar ⊆ U ∧ HenkinComplete U Sstar

Fair enumeration (the acceptance theorem): a consistent set in a ConsistencyPropertyEqOn U (over a countable U and countable relation symbols) extends to a Henkin-complete S* ⊇ S₀ inside U.