Documentation

Arithmetization.Basic.Ind

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

succInd φ ∈ Theory.indScheme ℒₒᵣ C

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

succInd φ ∈ Theory.indScheme ℒₒᵣ Semiformula.Open

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

Theory.indScheme ℒₒᵣ C ⊆ 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} [ORingStruc V] {C : FirstOrder.Semiformula ℒₒᵣ ℕ 1 → Prop} [V ⊧ₘ* FirstOrder.Theory.indScheme ℒₒᵣ C] {P : V → Prop} (hP : ∃ (e : ℕ → V) (φ : FirstOrder.Semiformula ℒₒᵣ ℕ 1), C φ ∧ ∀ (x : V), P x ↔ (FirstOrder.Semiformula.Evalm V ![x] e) φ) :

P 0 → (∀ (x : V), P x → P (x + 1)) → ∀ (x : V), P x

theorem LO.Arith.induction_h {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : Polarity) (m : ℕ) [V ⊧ₘ* FirstOrder.Theory.indScheme ℒₒᵣ (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} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : Polarity) (m : ℕ) [V ⊧ₘ* FirstOrder.Theory.indScheme ℒₒᵣ (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} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : Polarity) (m : ℕ) [V ⊧ₘ* FirstOrder.Theory.indScheme ℒₒᵣ (FirstOrder.Arith.Hierarchy Γ m)] :

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

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

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

theorem LO.Arith.least_number_h {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : Polarity) (m : ℕ) [V ⊧ₘ* FirstOrder.Theory.indScheme ℒₒᵣ (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} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : SigmaPiDelta) (m : ℕ) [V ⊧ₘ* FirstOrder.Theory.indScheme ℒₒᵣ (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} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : SigmaPiDelta) (m : ℕ) [V ⊧ₘ* FirstOrder.Theory.indScheme ℒₒᵣ (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} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : SigmaPiDelta) (m : ℕ) [V ⊧ₘ* FirstOrder.Theory.indScheme ℒₒᵣ (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} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {m : ℕ} {Γ : Polarity} [V ⊧ₘ* FirstOrder.Theory.indScheme ℒₒᵣ (FirstOrder.Arith.Hierarchy 𝚺 m)] :

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

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

V ⊧ₘ* 𝐈open

Equations

⋯ = ⋯

Instances For

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

V ⊧ₘ* 𝐈𝚺n₁

Equations

⋯ = ⋯

Instances For

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

V ⊧ₘ* 𝐏𝐀⁻

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

V ⊧ₘ* 𝐈open

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

V ⊧ₘ* 𝐈𝚺₀

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

V ⊧ₘ* 𝐈𝚷n

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

V ⊧ₘ* 𝐈𝚺n

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

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

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

V ⊧ₘ* 𝐈𝐍𝐃Γ n

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

P x