Supporting results for pointwise provable equality.

Σ_{s+1}-collection

Every Σ_{s+1} predicate bounded pointwise by a witness admits a single bound w that witnesses all instances at once (sigma_exists_bound_witness).

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sigma_exists_bound_witness {V : Type u_1} {n s : ℕ} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ(s + 1)] {θ : ArithmeticSemisentence (n + 2)} (hθ : Hierarchy Σ (s + 1) θ) (e : Fin n → V) (a : V) (h : ∀ x < a, ∃ (u : V), (Semiformula.Evalb (u :> x :> e)) θ) : ∃ (w : V), ∀ x < a, ∃ u ≤ w, (Semiformula.Evalb (u :> x :> e)) θ