Documentation

Arithmetization.Basic.Ind

theorem LO.FirstOrder.Arith.iSigma_subset_mono {s₁ : } {s₂ : } (h : s₁ s₂) :
theorem LO.Arith.induction {V : Type u_1} [LO.ORingStruc V] {C : LO.FirstOrder.Semiformula ℒₒᵣ 1Prop} [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ C] {P : VProp} (hP : ∃ (e : V) (p : LO.FirstOrder.Semiformula ℒₒᵣ 1), C p ∀ (x : V), P x (LO.FirstOrder.Semiformula.Evalm V ![x] e) p) :
P 0(∀ (x : V), P xP (x + 1))∀ (x : V), P x
theorem LO.Arith.induction_h {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : LO.Polarity) (m : ) [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ m)] {P : VProp} (hP : { Γ := Γ.coe, rank := m }-Predicate P) (zero : P 0) (succ : ∀ (x : V), P xP (x + 1)) (x : V) :
P x
theorem LO.Arith.order_induction_h {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : LO.Polarity) (m : ) [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ m)] {P : VProp} (hP : { Γ := Γ.coe, rank := m }-Predicate P) (ind : ∀ (x : V), (y < x, P y)P x) (x : V) :
P x
theorem LO.Arith.least_number_h {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : LO.Polarity) (m : ) [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ m)] {P : VProp} (hP : { Γ := Γ.coe, rank := m }-Predicate P) {x : V} (h : P x) :
∃ (y : V), P y z < y, ¬P z
theorem LO.Arith.induction_hh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : LO.SigmaPiDelta) (m : ) [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy 𝚺 m)] {P : VProp} (hP : { Γ := Γ, rank := m }-Predicate P) (zero : P 0) (succ : ∀ (x : V), P xP (x + 1)) (x : V) :
P x
theorem LO.Arith.order_induction_hh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : LO.SigmaPiDelta) (m : ) [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy 𝚺 m)] {P : VProp} (hP : { Γ := Γ, rank := m }-Predicate P) (ind : ∀ (x : V), (y < x, P y)P x) (x : V) :
P x
theorem LO.Arith.least_number_hh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : LO.SigmaPiDelta) (m : ) [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy 𝚺 m)] {P : VProp} (hP : { Γ := Γ, rank := m }-Predicate P) {x : V} (h : P x) :
∃ (y : V), P y z < y, ¬P z
Equations
  • =
Instances For
    def LO.Arith.mod_ISigma_of_le {V : Type u_1} [LO.ORingStruc V] {n₁ : } {n₂ : } (h : n₁ n₂) [V ⊧ₘ* 𝐈𝚺n₂] :
    Equations
    • =
    Instances For
      theorem LO.Arith.induction_sigma0 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {P : VProp} (hP : 𝚺₀-Predicate P) (zero : P 0) (succ : ∀ (x : V), P xP (x + 1)) (x : V) :
      P x
      theorem LO.Arith.induction_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : VProp} (hP : 𝚺₁-Predicate P) (zero : P 0) (succ : ∀ (x : V), P xP (x + 1)) (x : V) :
      P x
      theorem LO.Arith.induction_pi1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : VProp} (hP : 𝚷₁-Predicate P) (zero : P 0) (succ : ∀ (x : V), P xP (x + 1)) (x : V) :
      P x
      theorem LO.Arith.order_induction_sigma0 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {P : VProp} (hP : 𝚺₀-Predicate P) (ind : ∀ (x : V), (y < x, P y)P x) (x : V) :
      P x
      theorem LO.Arith.order_induction_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : VProp} (hP : 𝚺₁-Predicate P) (ind : ∀ (x : V), (y < x, P y)P x) (x : V) :
      P x
      theorem LO.Arith.order_induction_pi1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : VProp} (hP : 𝚷₁-Predicate P) (ind : ∀ (x : V), (y < x, P y)P x) (x : V) :
      P x
      theorem LO.Arith.least_number_sigma0 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {P : VProp} (hP : 𝚺₀-Predicate P) {x : V} (h : P x) :
      ∃ (y : V), P y z < y, ¬P z
      theorem LO.Arith.induction_h_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) (zero : P 0) (succ : ∀ (x : V), P xP (x + 1)) (x : V) :
      P x
      theorem LO.Arith.order_induction_h_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) (ind : ∀ (x : V), (y < x, P y)P x) (x : V) :
      P x