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 }

noncomputable def FirstOrder.Language.processDecompose {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (S : SetIn P) (t : ↑U) (idx : ℕ) : SetIn P

Process a decomposition request: if the trigger t is present, add the target dictated by its outermost shape (the per-index rules use idx; the branching/witness rules choose classically).

Equations

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

noncomputable def FirstOrder.Language.processImpC1 {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (S : SetIn P) (t : ↑U) : SetIn P

Process a C1 request: inspects only the outer imp constructor (so it reduces on φ.imp ψ regardless of whether φ/ψ later specialize to the negation encoding — the field that a shape-dispatching decompose leaves stuck).

Equations

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

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

Process one request.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.process S (FirstOrder.Language.Request.decompose t idx) = FirstOrder.Language.processDecompose S t idx
• FirstOrder.Language.process S (FirstOrder.Language.Request.impC1 t) = FirstOrder.Language.processImpC1 S t
• FirstOrder.Language.process S (FirstOrder.Language.Request.eqRefl c) = ⟨↑S ∪ {FirstOrder.Language.constEq c c}, ⋯⟩
• FirstOrder.Language.process S (FirstOrder.Language.Request.eqSymm a b) = if h : FirstOrder.Language.constEq a b ∈ ↑S then ⟨↑S ∪ {FirstOrder.Language.constEq b a}, ⋯⟩ else S

The prefix-sweep schedule

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

One sweep: process requests e 0, …, e n in order.

Equations

• FirstOrder.Language.sweep e S 0 = FirstOrder.Language.process S (e 0)
• FirstOrder.Language.sweep e S n.succ = FirstOrder.Language.process (FirstOrder.Language.sweep e S n) (e (n + 1))

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.