theorem
LO.FirstOrder.Arith.mem_indScheme_of_mem
{C : LO.FirstOrder.Semiformula ℒₒᵣ ℕ 1 → Prop}
{p : LO.FirstOrder.Semiformula ℒₒᵣ ℕ 1}
(hp : C p)
:
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)
:
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)]
:
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)]
:
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)
:
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)
:
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)]
:
Equations
- ⋯ = ⋯
def
LO.Arith.mod_IOpen_of_mod_indH
{V : Type u_1}
[LO.ORingStruc V]
(Γ : LO.Polarity)
(n : ℕ)
[V ⊧ₘ* 𝐈𝐍𝐃Γ n]
:
Equations
- ⋯ = ⋯
Instances For
instance
LO.Arith.instModelsTheoryPAMinusOfIOpen_arithmetization
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈open]
:
Equations
- ⋯ = ⋯
instance
LO.Arith.instModelsTheoryIOpenOfISigmaOfNatNat_arithmetization
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
Equations
- ⋯ = ⋯
instance
LO.Arith.instModelsTheoryISigmaOfNatNat_arithmetization
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
Equations
- ⋯ = ⋯
instance
LO.Arith.instModelsTheoryIPiOfISigma_arithmetization
{V : Type u_1}
[LO.ORingStruc V]
{n : ℕ}
[V ⊧ₘ* 𝐈𝚺n]
:
Equations
- ⋯ = ⋯
instance
LO.Arith.instModelsTheoryISigmaOfIPi_arithmetization
{V : Type u_1}
[LO.ORingStruc V]
{n : ℕ}
[V ⊧ₘ* 𝐈𝚷n]
:
Equations
- ⋯ = ⋯
instance
LO.Arith.instModelsTheoryIndHOfISigma_arithmetization
{V : Type u_1}
[LO.ORingStruc V]
{n : ℕ}
{Γ : LO.Polarity}
[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)
:
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