Induction and least number schemata of Arithmetic

References

• [HP98, §I.2(a), I.2.3]

Axiom formulas

def FFL.FirstOrder.Arithmetic.succInd {L : Language} [L.ORing] {ξ : Type u_3} (φ : Semiformula L ξ 1) : Formula L ξ

Equations

• FFL.FirstOrder.Arithmetic.succInd φ = φ/[↑0] 🡒 ∀¹ (φ/[FFL.FirstOrder.Semiterm.bvar 0] 🡒 φ/[‘(!!(FFL.FirstOrder.Semiterm.bvar 0) + 1)’]) 🡒 ∀¹ φ/[FFL.FirstOrder.Semiterm.bvar 0]

def FFL.FirstOrder.Arithmetic.orderInd {L : Language} [L.ORing] {ξ : Type u_3} (φ : Semiformula L ξ 1) : Formula L ξ

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Arithmetic.leastNumber {L : Language} [L.ORing] {ξ : Type u_3} (φ : Semiformula L ξ 1) : Formula L ξ

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Arithmetic.collectionAxiom {L : Language} [L.ORing] {ξ : Type u_3} (φ : Semiformula L ξ 2) : Formula L ξ

Equations

• One or more equations did not get rendered due to their size.

Induction schemata

def FFL.FirstOrder.Arithmetic.InductionScheme (L : Language) [L.ORing] (Γ : Semiformula L ℕ 1 → Prop) : Theory L

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.IOpen : ArithmeticTheory

Equations

• 𝗜𝗢𝗽𝗲𝗻 = 𝗣𝗔⁻ ∪ FFL.FirstOrder.Arithmetic.InductionScheme ℒₒᵣ FFL.FirstOrder.Semiformula.Open

def FFL.FirstOrder.Arithmetic.«term𝗜𝗢𝗽𝗲𝗻» : Lean.ParserDescr

Equations

• FFL.FirstOrder.Arithmetic.«term𝗜𝗢𝗽𝗲𝗻» = Lean.ParserDescr.node `FFL.FirstOrder.Arithmetic.«term𝗜𝗢𝗽𝗲𝗻» 1024 (Lean.ParserDescr.symbol "𝗜𝗢𝗽𝗲𝗻")

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.InductionOnHierarchy (Γ : Polarity) (s : ℕ) : ArithmeticTheory

Equations

• 𝗜𝗡𝗗 Γ s = 𝗣𝗔⁻ ∪ FFL.FirstOrder.Arithmetic.InductionScheme ℒₒᵣ (FFL.FirstOrder.Arithmetic.Hierarchy Γ s)

def FFL.FirstOrder.Arithmetic.«term𝗜𝗡𝗗_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.ISigma (s : ℕ) : ArithmeticTheory

Equations

• 𝗜𝚺s = 𝗜𝗡𝗗 𝚺 s

def FFL.FirstOrder.Arithmetic.«term𝗜𝚺_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Arithmetic.«term𝗜𝚺₀» : Lean.ParserDescr

Equations

• FFL.FirstOrder.Arithmetic.«term𝗜𝚺₀» = Lean.ParserDescr.node `FFL.FirstOrder.Arithmetic.«term𝗜𝚺₀» 1024 (Lean.ParserDescr.symbol "𝗜𝚺₀")

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.IPi (s : ℕ) : ArithmeticTheory

Equations

• 𝗜𝚷s = 𝗜𝗡𝗗 𝚷 s

def FFL.FirstOrder.Arithmetic.«term𝗜𝚷_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Arithmetic.«term𝗜𝚷₀» : Lean.ParserDescr

Equations

• FFL.FirstOrder.Arithmetic.«term𝗜𝚷₀» = Lean.ParserDescr.node `FFL.FirstOrder.Arithmetic.«term𝗜𝚷₀» 1024 (Lean.ParserDescr.symbol "𝗜𝚷₀")

def FFL.FirstOrder.Arithmetic.«term𝗜𝚺₁» : Lean.ParserDescr

Equations

• FFL.FirstOrder.Arithmetic.«term𝗜𝚺₁» = Lean.ParserDescr.node `FFL.FirstOrder.Arithmetic.«term𝗜𝚺₁» 1024 (Lean.ParserDescr.symbol "𝗜𝚺₁")

def FFL.FirstOrder.Arithmetic.«term𝗜𝚷₁» : Lean.ParserDescr

Equations

• FFL.FirstOrder.Arithmetic.«term𝗜𝚷₁» = Lean.ParserDescr.node `FFL.FirstOrder.Arithmetic.«term𝗜𝚷₁» 1024 (Lean.ParserDescr.symbol "𝗜𝚷₁")

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.Peano : ArithmeticTheory

Equations

• 𝗣𝗔 = 𝗣𝗔⁻ ∪ FFL.FirstOrder.Arithmetic.InductionScheme ℒₒᵣ Set.univ

def FFL.FirstOrder.Arithmetic.«term𝗣𝗔» : Lean.ParserDescr

Equations

• FFL.FirstOrder.Arithmetic.«term𝗣𝗔» = Lean.ParserDescr.node `FFL.FirstOrder.Arithmetic.«term𝗣𝗔» 1024 (Lean.ParserDescr.symbol "𝗣𝗔")

Least number schemata

def FFL.FirstOrder.Arithmetic.LeastNumberScheme (Γ : ArithmeticSemiformula ℕ 1 → Prop) : ArithmeticTheory

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.LeastNumberOnHierarchy (Γ : Polarity) (s : ℕ) : ArithmeticTheory

Equations

• 𝗟 Γ s = 𝗣𝗔⁻ ∪ FFL.FirstOrder.Arithmetic.LeastNumberScheme (FFL.FirstOrder.Arithmetic.Hierarchy Γ s)

def FFL.FirstOrder.Arithmetic.«term𝗟_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.LSigma (s : ℕ) : ArithmeticTheory

Equations

• 𝗟𝚺s = 𝗟 𝚺 s

def FFL.FirstOrder.Arithmetic.«term𝗟𝚺_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.LPi (s : ℕ) : ArithmeticTheory

Equations

• 𝗟𝚷s = 𝗟 𝚷 s

def FFL.FirstOrder.Arithmetic.«term𝗟𝚷_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

Collection schemata

def FFL.FirstOrder.Arithmetic.CollectionScheme (Γ : Set (ArithmeticSemiformula ℕ 2)) : Set ArithmeticSentence

Equations

• FFL.FirstOrder.Arithmetic.CollectionScheme Γ = (fun (φ : FFL.FirstOrder.Semiformula ℒₒᵣ ℕ 2) => FFL.FirstOrder.Semiformula.univCl (FFL.FirstOrder.Arithmetic.collectionAxiom φ)) '' Γ

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.CollectionOnHierarchy (Γ : Polarity) (s : ℕ) : ArithmeticTheory

Equations

• 𝗕 Γ s = 𝗜𝚺₀ ∪ FFL.FirstOrder.Arithmetic.CollectionScheme (FFL.FirstOrder.Arithmetic.StrictHierarchy Γ s)

def FFL.FirstOrder.Arithmetic.«term𝗕_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.BSigma (s : ℕ) : ArithmeticTheory

Equations

• 𝗕𝚺s = 𝗕 𝚺 s

def FFL.FirstOrder.Arithmetic.«term𝗕𝚺_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Arithmetic.«term𝗕𝚺₁» : Lean.ParserDescr

Equations

• FFL.FirstOrder.Arithmetic.«term𝗕𝚺₁» = Lean.ParserDescr.node `FFL.FirstOrder.Arithmetic.«term𝗕𝚺₁» 1024 (Lean.ParserDescr.symbol "𝗕𝚺₁")

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.BPi (s : ℕ) : ArithmeticTheory

Equations

• 𝗕𝚷s = 𝗕 𝚷 s

def FFL.FirstOrder.Arithmetic.«term𝗕𝚷_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.CollectionOnBroadHierarchy (Γ : Polarity) (s : ℕ) : ArithmeticTheory

The collection scheme for the broad hierarchy Hierarchy Γ s, i.e. Buss's BΓ_s⁺.

Equations

• 𝗕⁺ Γ s = 𝗜𝚺₀ ∪ FFL.FirstOrder.Arithmetic.CollectionScheme (FFL.FirstOrder.Arithmetic.Hierarchy Γ s)

def FFL.FirstOrder.Arithmetic.«term𝗕⁺_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

Induction scheme lemmas

theorem FFL.FirstOrder.Arithmetic.InductionScheme_subset {C C' : ArithmeticSemiformula ℕ 1 → Prop} (h : ∀ {φ : ArithmeticSemiformula ℕ 1}, C φ → C' φ) : InductionScheme ℒₒᵣ C ⊆ InductionScheme ℒₒᵣ C'

theorem FFL.FirstOrder.Arithmetic.mem_InductionScheme_of_mem {C : ArithmeticSemiformula ℕ 1 → Prop} {φ : ArithmeticSemiformula ℕ 1} (hp : C φ) : Semiformula.univCl (succInd φ) ∈ InductionScheme ℒₒᵣ C

theorem FFL.FirstOrder.Arithmetic.mem_IOpen_of_qfree {φ : ArithmeticSemiformula ℕ 1} (hp : Semiformula.Open φ) : Semiformula.univCl (succInd φ) ∈ InductionScheme ℒₒᵣ Semiformula.Open

theorem FFL.FirstOrder.Arithmetic.ISigma_subset_mono {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : 𝗜𝚺s₁ ⊆ 𝗜𝚺s₂

theorem FFL.FirstOrder.Arithmetic.ISigma_weakerThan_of_le {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : 𝗜𝚺s₁ ⪯ 𝗜𝚺s₂

theorem FFL.FirstOrder.Arithmetic.ISigma_weakerThan_of_le_trans {T : ArithmeticTheory} {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) (hT : 𝗜𝚺s₂ ⪯ T) : 𝗜𝚺s₁ ⪯ T

Least number scheme lemmas

theorem FFL.FirstOrder.Arithmetic.LeastNumberScheme_subset {C C' : ArithmeticSemiformula ℕ 1 → Prop} (h : ∀ {φ : ArithmeticSemiformula ℕ 1}, C φ → C' φ) : LeastNumberScheme C ⊆ LeastNumberScheme C'

theorem FFL.FirstOrder.Arithmetic.mem_LeastNumberScheme_of_mem {C : ArithmeticSemiformula ℕ 1 → Prop} {φ : ArithmeticSemiformula ℕ 1} (hφ : C φ) : Semiformula.univCl (leastNumber φ) ∈ LeastNumberScheme C

theorem FFL.FirstOrder.Arithmetic.LeastNumberOnHierarchy_subset_mono {Γ : Polarity} {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : 𝗟 Γ s₁ ⊆ 𝗟 Γ s₂

theorem FFL.FirstOrder.Arithmetic.LeastNumberOnHierarchy_weakerThan_of_le {Γ : Polarity} {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : 𝗟 Γ s₁ ⪯ 𝗟 Γ s₂

Collection scheme lemmas

theorem FFL.FirstOrder.Arithmetic.CollectionScheme_subset {C C' : ArithmeticSemiformula ℕ 2 → Prop} (h : ∀ {φ : ArithmeticSemiformula ℕ 2}, C φ → C' φ) : CollectionScheme C ⊆ CollectionScheme C'

theorem FFL.FirstOrder.Arithmetic.mem_CollectionScheme_of_mem {C : ArithmeticSemiformula ℕ 2 → Prop} {φ : ArithmeticSemiformula ℕ 2} (hφ : C φ) : Semiformula.univCl (collectionAxiom φ) ∈ CollectionScheme C

theorem FFL.FirstOrder.Arithmetic.CollectionOnHierarchy_subset_mono {Γ : Polarity} {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : 𝗕 Γ s₁ ⊆ 𝗕 Γ s₂

theorem FFL.FirstOrder.Arithmetic.CollectionOnHierarchy_weakerThan_of_le {Γ : Polarity} {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : 𝗕 Γ s₁ ⪯ 𝗕 Γ s₂

theorem FFL.FirstOrder.Arithmetic.CollectionOnHierarchy_subset_of_lt {Γ Γ' : Polarity} {s s' : ℕ} (h : s < s') : 𝗕 Γ s ⊆ 𝗕 Γ' s'

theorem FFL.FirstOrder.Arithmetic.CollectionOnHierarchy_weakerThan_of_lt {Γ Γ' : Polarity} {s s' : ℕ} (h : s < s') : 𝗕 Γ s ⪯ 𝗕 Γ' s'

theorem FFL.FirstOrder.Arithmetic.CollectionOnHierarchy_subset_BSigma_succ (Γ : Polarity) (s : ℕ) : 𝗕 Γ s ⊆ 𝗕𝚺(s + 1)

theorem FFL.FirstOrder.Arithmetic.CollectionOnHierarchy_weakerThan_BSigma_succ (Γ : Polarity) (s : ℕ) : 𝗕 Γ s ⪯ 𝗕𝚺(s + 1)

theorem FFL.FirstOrder.Arithmetic.CollectionOnHierarchy_subset_CollectionOnBroadHierarchy {Γ : Polarity} {s : ℕ} : 𝗕 Γ s ⊆ 𝗕⁺ Γ s

Relations between the theories

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiomInductionOnHierarchy {Γ : Polarity} {s : ℕ} : 𝗘𝗤 ℒₒᵣ ⪯ 𝗜𝗡𝗗 Γ s

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiomIOpen : 𝗘𝗤 ℒₒᵣ ⪯ 𝗜𝗢𝗽𝗲𝗻

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryIOpenInductionOnHierarchy {Γ : Polarity} {s : ℕ} : 𝗜𝗢𝗽𝗲𝗻 ⪯ 𝗜𝗡𝗗 Γ s

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryISigmaOfNatNat : 𝗜𝚺₀ ⪯ 𝗜𝚺₁

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryISigmaPeano {s : ℕ} : 𝗜𝚺s ⪯ 𝗣𝗔

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusIOpen : 𝗣𝗔⁻ ⪯ 𝗜𝗢𝗽𝗲𝗻

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryIOpenISigmaOfNatNat : 𝗜𝗢𝗽𝗲𝗻 ⪯ 𝗜𝚺₀

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryISigmaOfNatNatPeano : 𝗜𝚺₁ ⪯ 𝗣𝗔

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiomPeano : 𝗘𝗤 ℒₒᵣ ⪯ 𝗣𝗔

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusLeastNumberOnHierarchy (Γ : Polarity) (s : ℕ) : 𝗣𝗔⁻ ⪯ 𝗟 Γ s

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiomLeastNumberOnHierarchy (Γ : Polarity) (s : ℕ) : 𝗘𝗤 ℒₒᵣ ⪯ 𝗟 Γ s

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryISigmaOfNatNatCollectionOnHierarchy (Γ : Polarity) (s : ℕ) : 𝗜𝚺₀ ⪯ 𝗕 Γ s

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiomCollectionOnHierarchy (Γ : Polarity) (s : ℕ) : 𝗘𝗤 ℒₒᵣ ⪯ 𝗕 Γ s

instance FFL.FirstOrder.Arithmetic.CollectionOnHierarchy_weakerThan_CollectionOnBroadHierarchy (Γ : Polarity) (s : ℕ) : 𝗕 Γ s ⪯ 𝗕⁺ Γ s

theorem FFL.FirstOrder.Arithmetic.eq_weakerThan_of_ISigma {T : ArithmeticTheory} {s : ℕ} [𝗜𝚺s ⪯ T] : 𝗘𝗤 ℒₒᵣ ⪯ T

theorem FFL.FirstOrder.Arithmetic.eq_weakerThan_of_BSigma {T : ArithmeticTheory} {s : ℕ} [𝗕𝚺s ⪯ T] : 𝗘𝗤 ℒₒᵣ ⪯ T

theorem FFL.FirstOrder.Arithmetic.InductionScheme.succ_induction {V : Type u_1} [ORingStructure V] {C : ArithmeticSemiformula ℕ 1 → Prop} [V↓[ℒₒᵣ] ⊧* InductionScheme ℒₒᵣ C] {P : V → Prop} (hP : ∃ (e : ℕ → V) (φ : ArithmeticSemiformula ℕ 1), C φ ∧ ∀ (x : V), P x ↔ (Semiformula.Eval ![x] e) φ) : P 0 → (∀ (x : V), P x → P (x + 1)) → ∀ (x : V), P x

instance FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrInductionSchemeHierarchyNat {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ s] : V↓[ℒₒᵣ] ⊧* InductionScheme ℒₒᵣ (Hierarchy Γ s)

theorem FFL.FirstOrder.Arithmetic.InductionOnHierarchy.succ_induction {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ s] {P : V → Prop} (hP : { Γ := Γ.coe, rank := s }-Predicate P) (zero : P 0) (succ : ∀ (x : V), P x → P (x + 1)) (x : V) : P x

theorem FFL.FirstOrder.Arithmetic.InductionOnHierarchy.order_induction {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ s] {P : V → Prop} (hP : { Γ := Γ.coe, rank := s }-Predicate P) (ind : ∀ (x : V), (∀ y < x, P y) → P x) (x : V) : P x

instance FFL.FirstOrder.Arithmetic.InductionOnHierarchy.models_InductionScheme_alt {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ s] : V↓[ℒₒᵣ] ⊧* InductionScheme ℒₒᵣ (Hierarchy Γ.alt s)

instance FFL.FirstOrder.Arithmetic.InductionOnHierarchy.models_alt {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ s] : V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ.alt s

theorem FFL.FirstOrder.Arithmetic.InductionOnHierarchy.least_number {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ s] {P : V → Prop} (hP : { Γ := Γ.coe, rank := s }-Predicate P) {x : V} (h : P x) : ∃ (y : V), P y ∧ ∀ z < y, ¬P z

theorem FFL.FirstOrder.Arithmetic.InductionOnHierarchy.succ_induction_sigma {V : Type u_1} [ORingStructure V] (Γ : SigmaPiDelta) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 𝚺 s] {P : V → Prop} (hP : { Γ := Γ, rank := s }-Predicate P) (zero : P 0) (succ : ∀ (x : V), P x → P (x + 1)) (x : V) : P x

theorem FFL.FirstOrder.Arithmetic.InductionOnHierarchy.order_induction_sigma {V : Type u_1} [ORingStructure V] (Γ : SigmaPiDelta) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 𝚺 s] {P : V → Prop} (hP : { Γ := Γ, rank := s }-Predicate P) (ind : ∀ (x : V), (∀ y < x, P y) → P x) (x : V) : P x

theorem FFL.FirstOrder.Arithmetic.InductionOnHierarchy.least_number_sigma {V : Type u_1} [ORingStructure V] (Γ : SigmaPiDelta) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 𝚺 s] {P : V → Prop} (hP : { Γ := Γ, rank := s }-Predicate P) {x : V} (h : P x) : ∃ (y : V), P y ∧ ∀ z < y, ¬P z

instance FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrOfSigmaPolarity {V : Type u_1} [ORingStructure V] {s : ℕ} {Γ : Polarity} [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 𝚺 s] : V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ s

instance FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrOfPiPolarity {V : Type u_1} [ORingStructure V] {s : ℕ} {Γ : Polarity} [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 𝚷 s] : V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ s

theorem FFL.FirstOrder.Arithmetic.InductionOnHierarchy.mod_ISigma_of_le {V : Type u_1} [ORingStructure V] {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) [V↓[ℒₒᵣ] ⊧* 𝗜𝚺s₂] : V↓[ℒₒᵣ] ⊧* 𝗜𝚺s₁

instance FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrISigmaOfNatNat {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀

instance FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrIPiOfISigma {V : Type u_1} [ORingStructure V] {s : ℕ} [V↓[ℒₒᵣ] ⊧* 𝗜𝚺s] : V↓[ℒₒᵣ] ⊧* 𝗜𝚷s

instance FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrISigmaOfIPi {V : Type u_1} [ORingStructure V] {s : ℕ} [V↓[ℒₒᵣ] ⊧* 𝗜𝚷s] : V↓[ℒₒᵣ] ⊧* 𝗜𝚺s

theorem FFL.FirstOrder.Arithmetic.InductionOnHierarchy.models_ISigma_iff_models_IPi {V : Type u_1} [ORingStructure V] {s : ℕ} : V↓[ℒₒᵣ] ⊧* 𝗜𝚺s ↔ V↓[ℒₒᵣ] ⊧* 𝗜𝚷s

instance FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrOfISigma {V : Type u_1} [ORingStructure V] {s : ℕ} {Γ : Polarity} [V↓[ℒₒᵣ] ⊧* 𝗜𝚺s] : V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ s

theorem FFL.FirstOrder.Arithmetic.ISigma0.succ_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {P : V → Prop} (hP : 𝚺₀-Predicate P) (zero : P 0) (succ : ∀ (x : V), P x → P (x + 1)) (x : V) : P x

theorem FFL.FirstOrder.Arithmetic.ISigma1.sigma1_succ_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {P : V → Prop} (hP : 𝚺₁-Predicate P) (zero : P 0) (succ : ∀ (x : V), P x → P (x + 1)) (x : V) : P x

theorem FFL.FirstOrder.Arithmetic.ISigma1.pi1_succ_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {P : V → Prop} (hP : 𝚷₁-Predicate P) (zero : P 0) (succ : ∀ (x : V), P x → P (x + 1)) (x : V) : P x

theorem FFL.FirstOrder.Arithmetic.ISigma0.order_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {P : V → Prop} (hP : 𝚺₀-Predicate P) (ind : ∀ (x : V), (∀ y < x, P y) → P x) (x : V) : P x

theorem FFL.FirstOrder.Arithmetic.ISigma1.sigma1_order_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {P : V → Prop} (hP : 𝚺₁-Predicate P) (ind : ∀ (x : V), (∀ y < x, P y) → P x) (x : V) : P x

theorem FFL.FirstOrder.Arithmetic.ISigma1.pi1_order_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {P : V → Prop} (hP : 𝚷₁-Predicate P) (ind : ∀ (x : V), (∀ y < x, P y) → P x) (x : V) : P x

theorem FFL.FirstOrder.Arithmetic.ISigma0.least_number {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {P : V → Prop} (hP : 𝚺₀-Predicate P) {x : V} (h : P x) : ∃ (y : V), P y ∧ ∀ z < y, ¬P z

theorem FFL.FirstOrder.Arithmetic.ISigma1.succ_induction {V : Type u_1} [ORingStructure 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 FFL.FirstOrder.Arithmetic.ISigma1.order_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (Γ : SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (ind : ∀ (x : V), (∀ y < x, P y) → P x) (x : V) : P x

instance FFL.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrPeanoMinusOfIOpen {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻

instance FFL.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrIOpenOfISigmaOfNatNat {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻

instance FFL.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrISigmaOfNatNat {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.mod_ISigma_of_le {V : Type u_1} [ORingStructure V] {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) [V↓[ℒₒᵣ] ⊧* 𝗜𝚺s₂] : V↓[ℒₒᵣ] ⊧* 𝗜𝚺s₁

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.mod_BSigma_of_le {V : Type u_1} [ORingStructure V] {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) [V↓[ℒₒᵣ] ⊧* 𝗕𝚺s₂] : V↓[ℒₒᵣ] ⊧* 𝗕𝚺s₁

Equations

• ⋯ = ⋯

theorem FFL.FirstOrder.Arithmetic.mod_paMinus_of_ISigma {V : Type u_1} [ORingStructure V] {s : ℕ} [V↓[ℒₒᵣ] ⊧* 𝗜𝚺s] : V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻

instance FFL.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrISigmaOfPeano {V : Type u_1} [ORingStructure V] {s : ℕ} [V↓[ℒₒᵣ] ⊧* 𝗣𝗔] : V↓[ℒₒᵣ] ⊧* 𝗜𝚺s

theorem FFL.FirstOrder.Arithmetic.models_succInd (φ : ArithmeticSemiformula ℕ 1) : ℕ↓[ℒₒᵣ] ⊧ Semiformula.univCl (succInd φ)

instance FFL.FirstOrder.Arithmetic.models_ISigma (Γ : Polarity) (s : ℕ) : ℕ↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ s

instance FFL.FirstOrder.Arithmetic.models_ISigmaZero : ℕ↓[ℒₒᵣ] ⊧* 𝗜𝚺₀

instance FFL.FirstOrder.Arithmetic.models_ISigmaOne : ℕ↓[ℒₒᵣ] ⊧* 𝗜𝚺₁

instance FFL.FirstOrder.Arithmetic.models_Peano : ℕ↓[ℒₒᵣ] ⊧* 𝗣𝗔

instance FFL.FirstOrder.Arithmetic.sigmaOneSound_ISigmaOne : 𝗜𝚺₁.SoundOnHierarchy 𝚺 1

instance FFL.FirstOrder.Arithmetic.sigmaOneSound_Peano : 𝗣𝗔.SoundOnHierarchy 𝚺 1

instance FFL.FirstOrder.Arithmetic.instConsistentSentenceORingArithmeticTheoryInductionOnHierarchy {Γ : Polarity} {s : ℕ} : Entailment.Consistent (𝗜𝗡𝗗 Γ s)

instance FFL.FirstOrder.Arithmetic.instConsistentSentenceORingArithmeticTheoryPeano : Entailment.Consistent 𝗣𝗔

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoFirstOrderTrueArith : 𝗣𝗔 ⪯ 𝗧𝗔

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryR0OfPeanoMinus (T : ArithmeticTheory) [𝗣𝗔⁻ ⪯ T] : 𝗥₀ ⪯ T

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusOfISigmaOfNatNat (T : ArithmeticTheory) [𝗜𝚺₀ ⪯ T] : 𝗣𝗔⁻ ⪯ T

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusOfISigmaOfNatNat_1 (T : ArithmeticTheory) [𝗜𝚺₁ ⪯ T] : 𝗣𝗔⁻ ⪯ T

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusOfPeano (T : ArithmeticTheory) [𝗣𝗔 ⪯ T] : 𝗣𝗔⁻ ⪯ T