Various induction-related principles in $\mathsf{I}\Sigma_n$ #
theorem
LO.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
LO.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
LO.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
LO.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
LO.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
LO.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
LO.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)
: