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.

Named lemmas exposed for the inseparable-pair instance and the limit proof: the schedule (stage_mono, subset_stage, stage_subset_U; stage-in-C.sets is automatic via the SetIn subtype), the firing API (request_fires_after — every request fires in a sweep after any given stage, via beforeRequest/process_beforeRequest_eq_sweep/sweep_mono), and finite-stage preservation (finite_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

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

Processing only grows the set (processDecompose).

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

theorem FirstOrder.Language.subset_process {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (S : SetIn P) (r : Request U) : ↑S ⊆ ↑(process S r)

Processing only grows the set.

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

theorem FirstOrder.Language.subset_sweep {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (S : SetIn P) (n : ℕ) : ↑S ⊆ ↑(sweep e S n)

theorem FirstOrder.Language.stage_subset_succ {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (S₀ : SetIn P) (n : ℕ) : ↑(stage e S₀ n) ⊆ ↑(stage e S₀ (n + 1))

Stage monotonicity (one step).

theorem FirstOrder.Language.stage_mono {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (S₀ : SetIn P) {m n : ℕ} (h : m ≤ n) : ↑(stage e S₀ m) ⊆ ↑(stage e S₀ n)

Stage monotonicity.

theorem FirstOrder.Language.subset_stage {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (S₀ : SetIn P) (n : ℕ) : ↑S₀ ⊆ ↑(stage e S₀ n)

S₀ ⊆ every stage.

theorem FirstOrder.Language.stage_subset_U {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (S₀ : SetIn P) (n : ℕ) : ↑(stage e S₀ n) ⊆ U

Each stage lies in U.

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)

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

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

theorem FirstOrder.Language.mem_Sstar_iff {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (S₀ : SetIn P) {x : (L.withConstants ℕ).Sentenceω} : x ∈ Sstar e S₀ ↔ ∃ (n : ℕ), x ∈ ↑(stage e S₀ n)

The firing API

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

The accumulated set just before request e k is processed in a sweep from S.

Equations

• FirstOrder.Language.beforeRequest e S 0 = S
• FirstOrder.Language.beforeRequest e S n.succ = FirstOrder.Language.sweep e S n

theorem FirstOrder.Language.subset_beforeRequest {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (S : SetIn P) (k : ℕ) : ↑S ⊆ ↑(beforeRequest e S k)

theorem FirstOrder.Language.process_beforeRequest_eq_sweep {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (S : SetIn P) (k : ℕ) : process (beforeRequest e S k) (e k) = sweep e S k

Processing e k at its accumulated point advances the sweep by one — nearly definitional.

theorem FirstOrder.Language.sweep_mono {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (S : SetIn P) {k n : ℕ} (h : k ≤ n) : ↑(sweep e S k) ⊆ ↑(sweep e S n)

Sweeps are monotone in the number of requests processed.

theorem FirstOrder.Language.request_fires_after {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (he : Function.Surjective e) (S₀ : SetIn P) (r : Request U) (m : ℕ) : ∃ (n : ℕ), m ≤ n ∧ ∃ (acc : SetIn P), ↑(stage e S₀ m) ⊆ ↑acc ∧ ↑(process acc r) ⊆ ↑(stage e S₀ (n + 1))

The firing consumer lemma (fairness): for a surjective schedule, every request fires in some sweep after any given stage m — the pre-accumulator contains stage m, and the process output at the firing lands inside stage (n+1).

Finite-stage preservation

theorem FirstOrder.Language.finite_processDecompose {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} {S : SetIn P} (t : ↑U) (idx : ℕ) (hS : (↑S).Finite) : (↑(processDecompose S t idx)).Finite

theorem FirstOrder.Language.finite_processImpC1 {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} {S : SetIn P} (t : ↑U) (hS : (↑S).Finite) : (↑(processImpC1 S t)).Finite

theorem FirstOrder.Language.finite_process {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} {S : SetIn P} (r : Request U) (hS : (↑S).Finite) : (↑(process S r)).Finite

theorem FirstOrder.Language.finite_sweep {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) {S : SetIn P} (hS : (↑S).Finite) (n : ℕ) : (↑(sweep e S n)).Finite

theorem FirstOrder.Language.finite_stage {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) {S₀ : SetIn P} (hS₀ : (↑S₀).Finite) (n : ℕ) : (↑(stage e S₀ n)).Finite

Finite-stage preservation: from a finite initial set, every stage is finite (documenting that the construction stays inside the finite-pair instance).

What each firing adds (process specs)

theorem FirstOrder.Language.spec_impC1 {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (φ ψ : (L.withConstants ℕ).Sentenceω) (hU : BoundedFormulaω.imp φ ψ ∈ U) (hmem : BoundedFormulaω.imp φ ψ ∈ ↑acc) : BoundedFormulaω.not φ ∈ ↑(process acc (Request.impC1 ⟨BoundedFormulaω.imp φ ψ, hU⟩)) ∨ ψ ∈ ↑(process acc (Request.impC1 ⟨BoundedFormulaω.imp φ ψ, hU⟩))

theorem FirstOrder.Language.spec_negImp {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (φ ψ : (L.withConstants ℕ).Sentenceω) (hU : (BoundedFormulaω.imp φ ψ).not ∈ U) (hmem : (BoundedFormulaω.imp φ ψ).not ∈ ↑acc) (idx : ℕ) : (idx = 0 → φ ∈ ↑(process acc (Request.decompose ⟨(BoundedFormulaω.imp φ ψ).not, hU⟩ idx))) ∧ (idx ≠ 0 → BoundedFormulaω.not ψ ∈ ↑(process acc (Request.decompose ⟨(BoundedFormulaω.imp φ ψ).not, hU⟩ idx)))

theorem FirstOrder.Language.spec_iInf {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hU : BoundedFormulaω.iInf φs ∈ U) (idx : ℕ) (hmem : BoundedFormulaω.iInf φs ∈ ↑acc) : φs idx ∈ ↑(process acc (Request.decompose ⟨BoundedFormulaω.iInf φs, hU⟩ idx))

theorem FirstOrder.Language.spec_negIInf {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hU : (BoundedFormulaω.iInf φs).not ∈ U) (idx : ℕ) (hmem : (BoundedFormulaω.iInf φs).not ∈ ↑acc) : ∃ (k : ℕ), BoundedFormulaω.not (φs k) ∈ ↑(process acc (Request.decompose ⟨(BoundedFormulaω.iInf φs).not, hU⟩ idx))

theorem FirstOrder.Language.spec_iSup {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hU : BoundedFormulaω.iSup φs ∈ U) (idx : ℕ) (hmem : BoundedFormulaω.iSup φs ∈ ↑acc) : ∃ (k : ℕ), φs k ∈ ↑(process acc (Request.decompose ⟨BoundedFormulaω.iSup φs, hU⟩ idx))

theorem FirstOrder.Language.spec_negISup {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hU : (BoundedFormulaω.iSup φs).not ∈ U) (idx : ℕ) (hmem : (BoundedFormulaω.iSup φs).not ∈ ↑acc) : BoundedFormulaω.not (φs idx) ∈ ↑(process acc (Request.decompose ⟨(BoundedFormulaω.iSup φs).not, hU⟩ idx))

theorem FirstOrder.Language.spec_allInst {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hU : φ.all ∈ U) (idx : ℕ) (hmem : φ.all ∈ ↑acc) : instConst idx φ ∈ ↑(process acc (Request.decompose ⟨φ.all, hU⟩ idx))

theorem FirstOrder.Language.spec_negAll {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hU : φ.all.not ∈ U) (idx : ℕ) (hmem : φ.all.not ∈ ↑acc) : ∃ (c : ℕ), BoundedFormulaω.not (instConst c φ) ∈ ↑(process acc (Request.decompose ⟨φ.all.not, hU⟩ idx))

theorem FirstOrder.Language.spec_eqRefl {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (c : ℕ) : constEq c c ∈ ↑(process acc (Request.eqRefl c))

theorem FirstOrder.Language.spec_eqSymm {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (a b : ℕ) (hmem : constEq a b ∈ ↑acc) : constEq b a ∈ ↑(process acc (Request.eqSymm a b))

theorem FirstOrder.Language.spec_eqTrans {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (a b d : ℕ) (h1 : constEq a b ∈ ↑acc) (h2 : constEq b d ∈ ↑acc) : constEq a d ∈ ↑(process acc (Request.eqTrans a b d))

theorem FirstOrder.Language.spec_relCongr {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (acc : SetIn P) (l : ℕ) (R : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ) (h1 : relInst R g ∈ ↑acc) (h2 : constEq (g i) b ∈ ↑acc) : relInst R (Function.update g i b) ∈ ↑(process acc (Request.relCongr l R g i b))

The limit is Henkin-complete

theorem FirstOrder.Language.mem_Sstar_of_fires {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (he : Function.Surjective e) (S₀ : SetIn P) {member target : (L.withConstants ℕ).Sentenceω} (r : Request U) (hmem : member ∈ Sstar e S₀) (hspec : ∀ (acc : SetIn P), member ∈ ↑acc → target ∈ ↑(process acc r)) : target ∈ Sstar e S₀

If a firing of r on any accumulator containing member adds target, and member ∈ S*, then target ∈ S*.

theorem FirstOrder.Language.or_mem_Sstar_of_fires {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (he : Function.Surjective e) (S₀ : SetIn P) {member t₁ t₂ : (L.withConstants ℕ).Sentenceω} (r : Request U) (hmem : member ∈ Sstar e S₀) (hspec : ∀ (acc : SetIn P), member ∈ ↑acc → t₁ ∈ ↑(process acc r) ∨ t₂ ∈ ↑(process acc r)) : t₁ ∈ Sstar e S₀ ∨ t₂ ∈ Sstar e S₀

Disjunctive variant (for branching fields).

theorem FirstOrder.Language.exists_mem_Sstar_of_fires {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (he : Function.Surjective e) (S₀ : SetIn P) {member : (L.withConstants ℕ).Sentenceω} {α : Sort u_1} {motive : α → (L.withConstants ℕ).Sentenceω} (r : Request U) (hmem : member ∈ Sstar e S₀) (hspec : ∀ (acc : SetIn P), member ∈ ↑acc → ∃ (a : α), motive a ∈ ↑(process acc r)) : ∃ (a : α), motive a ∈ Sstar e S₀

Existential variant (for witness fields).

theorem FirstOrder.Language.mem_Sstar_of_fires_uncond {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (he : Function.Surjective e) (S₀ : SetIn P) {target : (L.withConstants ℕ).Sentenceω} (r : Request U) (hspec : ∀ (acc : SetIn P), target ∈ ↑(process acc r)) : target ∈ Sstar e S₀

Unconditional variant (for reflexivity, which has no trigger).

theorem FirstOrder.Language.mem_Sstar_of_fires₂ {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (he : Function.Surjective e) (S₀ : SetIn P) {m₁ m₂ target : (L.withConstants ℕ).Sentenceω} (r : Request U) (h₁ : m₁ ∈ Sstar e S₀) (h₂ : m₂ ∈ Sstar e S₀) (hspec : ∀ (acc : SetIn P), m₁ ∈ ↑acc → m₂ ∈ ↑acc → target ∈ ↑(process acc r)) : target ∈ Sstar e S₀

Two-premise variant (for transitivity / relation congruence).

theorem FirstOrder.Language.henkinComplete_Sstar {L : Language} {U : Set (L.withConstants ℕ).Sentenceω} {P : ConsistencyPropertyEqOn U} (e : ℕ → Request U) (he : Function.Surjective e) (S₀ : SetIn P) : HenkinComplete U (Sstar e S₀)

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.