Documentation

Arithmetization.Basic.Ind

theorem LO.FirstOrder.Arith.mem_indScheme_of_mem {C : LO.FirstOrder.Semiformula ℒₒᵣ ℕ 1 → Prop} {p : LO.FirstOrder.Semiformula ℒₒᵣ ℕ 1} (hp : C p) :

LO.FirstOrder.succInd p ∈ LO.FirstOrder.Theory.indScheme ℒₒᵣ C

theorem LO.FirstOrder.Arith.mem_iOpen_of_qfree {p : LO.FirstOrder.Semiformula ℒₒᵣ ℕ 1} (hp : p.Open) :

LO.FirstOrder.succInd p ∈ LO.FirstOrder.Theory.indScheme ℒₒᵣ LO.FirstOrder.Semiformula.Open

theorem LO.FirstOrder.Arith.indScheme_subset {C : LO.FirstOrder.Semiformula ℒₒᵣ ℕ 1 → Prop} {C' : LO.FirstOrder.Semiformula ℒₒᵣ ℕ 1 → Prop} (h : ∀ {p : LO.FirstOrder.Semiformula ℒₒᵣ ℕ 1}, C p → C' p) :

LO.FirstOrder.Theory.indScheme ℒₒᵣ C ⊆ LO.FirstOrder.Theory.indScheme ℒₒᵣ C'

theorem LO.FirstOrder.Arith.iSigma_subset_mono {s₁ : ℕ} {s₂ : ℕ} (h : s₁ ≤ s₂) :

𝐈𝚺s₁ ⊆ 𝐈𝚺s₂

theorem LO.Arith.induction {V : Type u_1} [LO.ORingStruc V] {C : LO.FirstOrder.Semiformula ℒₒᵣ ℕ 1 → Prop} [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ C] {P : V → Prop} (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 x → P (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 : V → Prop} (hP : { Γ := Γ.coe, rank := m }-Predicate P) (zero : P 0) (succ : ∀ (x : V), P x → P (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 : V → Prop} (hP : { Γ := Γ.coe, rank := m }-Predicate P) (ind : ∀ (x : V), (∀ y < x, P y) → P x) (x : V) :

P x

theorem LO.Arith.models_indScheme_alt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : LO.Polarity) (m : ℕ) [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ m)] :

V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ.alt m)

instance LO.Arith.instModelsTheoryIndSchemeORingHierarchyNatAlt_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : LO.Polarity) (m : ℕ) [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ m)] :

V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ.alt m)

Equations

⋯ = ⋯

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 : V → Prop} (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 : V → Prop} (hP : { Γ := Γ, rank := m }-Predicate P) (zero : P 0) (succ : ∀ (x : V), P x → P (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 : V → Prop} (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 : V → Prop} (hP : { Γ := Γ, rank := m }-Predicate P) {x : V} (h : P x) :

∃ (y : V), P y ∧ ∀ z < y, ¬P z

instance LO.Arith.instModelsTheoryIndSchemeORingHierarchyNatOfSigmaPolarity_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {m : ℕ} {Γ : LO.Polarity} [V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy 𝚺 m)] :

V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ m)

Equations

⋯ = ⋯

def LO.Arith.mod_IOpen_of_mod_indH {V : Type u_1} [LO.ORingStruc V] (Γ : LO.Polarity) (n : ℕ) [V ⊧ₘ* 𝐈𝐍𝐃Γ n] :

V ⊧ₘ* 𝐈open

Equations

⋯ = ⋯

Instances For

def LO.Arith.mod_ISigma_of_le {V : Type u_1} [LO.ORingStruc V] {n₁ : ℕ} {n₂ : ℕ} (h : n₁ ≤ n₂) [V ⊧ₘ* 𝐈𝚺n₂] :

V ⊧ₘ* 𝐈𝚺n₁

Equations

⋯ = ⋯

Instances For

instance LO.Arith.instModelsTheoryPAMinusOfIOpen_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] :

V ⊧ₘ* 𝐏𝐀⁻

Equations

⋯ = ⋯

instance LO.Arith.instModelsTheoryIOpenOfISigmaOfNatNat_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

V ⊧ₘ* 𝐈open

Equations

⋯ = ⋯

instance LO.Arith.instModelsTheoryISigmaOfNatNat_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

V ⊧ₘ* 𝐈𝚺₀

Equations

⋯ = ⋯

instance LO.Arith.instModelsTheoryIPiOfISigma_arithmetization {V : Type u_1} [LO.ORingStruc V] {n : ℕ} [V ⊧ₘ* 𝐈𝚺n] :

V ⊧ₘ* 𝐈𝚷n

Equations

⋯ = ⋯

instance LO.Arith.instModelsTheoryISigmaOfIPi_arithmetization {V : Type u_1} [LO.ORingStruc V] {n : ℕ} [V ⊧ₘ* 𝐈𝚷n] :

V ⊧ₘ* 𝐈𝚺n

Equations

⋯ = ⋯

theorem LO.Arith.models_ISigma_iff_models_IPi {V : Type u_1} [LO.ORingStruc V] {n : ℕ} :

V ⊧ₘ* 𝐈𝚺n ↔ V ⊧ₘ* 𝐈𝚷n

instance LO.Arith.instModelsTheoryIndHOfISigma_arithmetization {V : Type u_1} [LO.ORingStruc V] {n : ℕ} {Γ : LO.Polarity} [V ⊧ₘ* 𝐈𝚺n] :

V ⊧ₘ* 𝐈𝐍𝐃Γ n

Equations

⋯ = ⋯

theorem LO.Arith.induction_sigma0 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {P : V → Prop} (hP : 𝚺₀ -Predicate P) (zero : P 0) (succ : ∀ (x : V), P x → P (x + 1)) (x : V) :

P x

theorem LO.Arith.induction_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : V → Prop} (hP : 𝚺₁ -Predicate P) (zero : P 0) (succ : ∀ (x : V), P x → P (x + 1)) (x : V) :

P x

theorem LO.Arith.induction_pi1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : V → Prop} (hP : 𝚷₁ -Predicate P) (zero : P 0) (succ : ∀ (x : V), P x → P (x + 1)) (x : V) :

P x

theorem LO.Arith.order_induction_sigma0 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {P : V → Prop} (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 : V → Prop} (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 : V → Prop} (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 : V → Prop} (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 : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (zero : P 0) (succ : ∀ (x : V), P x → P (x + 1)) (x : V) :

P x

theorem LO.Arith.order_induction_h_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (ind : ∀ (x : V), (∀ y < x, P y) → P x) (x : V) :

P x