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

theorem 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 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 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 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 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 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 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 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