Documentation

LeanPool.Incompleteness.Arithmetization.Basic.Ind

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₂) :

𝐈Sgs₁ ⊆ 𝐈Sgs₂

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

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

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

V ⊧ₘ* 𝐈open

Imported declaration from the Incompleteness formalization.

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

V ⊧ₘ* 𝐈Sgn₁

Imported declaration from the Incompleteness formalization.

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

V ⊧ₘ* 𝐏𝐀⁻

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

V ⊧ₘ* 𝐈open

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

V ⊧ₘ* 𝐈Sg0

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

V ⊧ₘ* 𝐈Pgn

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

V ⊧ₘ* 𝐈Sgn

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

V ⊧ₘ* 𝐈Sgn ↔ V ⊧ₘ* 𝐈Pgn

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

V ⊧ₘ* 𝐈𝐍𝐃Γ n

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

P x