Supporting results for pointwise provable equality.

Various induction-related principles in $\mathsf{I}\Sigma_n$

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sigma1_pos_succ_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {P : V → Prop} (hP : Σ₁-Predicate P) (zero : P 0) (one : P 1) (succ : ∀ (x : V), P (x + 1) → P (x + 2)) (x : V) : P x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.bounded_all_sigma1_order_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {f : V → V → V} (hf : Σ₁-Function₂ f) {P : V → V → Prop} (hP : Σ₁-Relation P) (ind : ∀ (x y : V), (∀ x' < x, ∀ y' ≤ f x y, P x' y') → P x y) (x y : V) : P x y

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.bounded_all_sigma1_order_induction' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {f : V → V} (hf : Σ₁-Function₁ f) {P : V → V → Prop} (hP : Σ₁-Relation P) (ind : ∀ (x y : V), (∀ x' < x, ∀ y' ≤ f y, P x' y') → P x y) (x y : V) : P x y

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.bounded_all_sigma1_order_induction₂ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {fy fz : V → V → V → V} (hfy : Σ₁-Function₃ fy) (hfz : Σ₁-Function₃ fz) {P : V → V → V → Prop} (hP : Σ₁-Relation₃ P) (ind : ∀ (x y z : V), (∀ x' < x, ∀ y' ≤ fy x y z, ∀ z' ≤ fz x y z, P x' y' z') → P x y z) (x y z : V) : P x y z

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.bounded_all_sigma1_order_induction₃ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {fy fz fw : V → V → V → V → V} (hfy : Σ₁-Function₄ fy) (hfz : Σ₁-Function₄ fz) (hfw : Σ₁-Function₄ fw) {P : V → V → V → V → Prop} (hP : Σ₁-Relation₄ P) (ind : ∀ (x y z w : V), (∀ x' < x, ∀ y' ≤ fy x y z w, ∀ z' ≤ fz x y z w, ∀ w' ≤ fw x y z w, P x' y' z' w') → P x y z w) (x y z w : V) : P x y z w

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.measured_bounded_sigma1_order_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {m f : V → V} {P : V → Prop} (hm : Σ₁-Function₁ m) (hf : Σ₁-Function₁ f) (hP : Σ₁-Predicate P) (H : ∀ (a : V), (∀ b ≤ f a, m b < m a → P b) → P a) (a : V) : P a

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sigma_or_pi_succ_induction {V : Type u_1} [ORingStructure V] (m : ℕ) [Fact (1 ≤ m)] [V↓[ℒₒᵣ] ⊧* 𝐈𝐍𝐃 Σ m] {P Q : V → Prop} (hP : { Γ := Σ, rank := m }-Predicate P) (hQ : { Γ := Π, rank := m }-Predicate Q) (zero : P 0 ∨ Q 0) (succ : ∀ (x : V), P x ∨ Q x → P (x + 1) ∨ Q (x + 1)) (x : V) : P x ∨ Q x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sigma_or_pi_order_induction {V : Type u_1} [ORingStructure V] (m : ℕ) [Fact (1 ≤ m)] [V↓[ℒₒᵣ] ⊧* 𝐈𝐍𝐃 Σ m] {P Q : V → Prop} (hP : { Γ := Σ, rank := m }-Predicate P) (hQ : { Γ := Π, rank := m }-Predicate Q) (ind : ∀ (x : V), (∀ y < x, P y ∨ Q y) → P x ∨ Q x) (x : V) : P x ∨ Q x