Supporting results for pointwise provable equality.

Induction and least number schemata of Arithmetic

References

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

Axiom formulas

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

The succ Ind construction in FFL.FirstOrder.Arithmetic.

Equations

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

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

The order Ind construction in FFL.FirstOrder.Arithmetic.

Equations

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

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

The least Number construction in FFL.FirstOrder.Arithmetic.

Equations

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

Induction schemata

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

The Induction Scheme construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.IOpen : ArithmeticTheory

The 𝐈𝐎𝐩𝐞𝐧 construction in 𝐈𝐎𝐩𝐞𝐧.

Equations

• 𝐈𝐎𝐩𝐞𝐧 = 𝐏𝐀⁻ ∪ PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionScheme ℒₒᵣ PointwiseComposition.FFL.FirstOrder.Semiformula.Open

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈𝐎𝐩𝐞𝐧» : Lean.ParserDescr

The «term𝐈𝐎𝐩𝐞𝐧» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈𝐎𝐩𝐞𝐧» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈𝐎𝐩𝐞𝐧» 1024 (Lean.ParserDescr.symbol "𝐈𝐎𝐩𝐞𝐧")

@[reducible, inline]

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

The Induction On Hierarchy construction in FFL.FirstOrder.Arithmetic.

Equations

• 𝐈𝐍𝐃 Γ s = 𝐏𝐀⁻ ∪ PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionScheme ℒₒᵣ (PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy Γ s)

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈𝐍𝐃_» : Lean.ParserDescr

The «term𝐈𝐍𝐃 » construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[reducible, inline]

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

The ISigma construction in FFL.FirstOrder.Arithmetic.

Equations

• 𝐈Σs = 𝐈𝐍𝐃 Σ s

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Σ_» : Lean.ParserDescr

The «term𝐈Σ » construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Σ₀» : Lean.ParserDescr

The «term𝐈Σ₀» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Σ₀» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Σ₀» 1024 (Lean.ParserDescr.symbol "𝐈Σ₀")

@[reducible, inline]

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

The IPi construction in FFL.FirstOrder.Arithmetic.

Equations

• 𝐈Πs = 𝐈𝐍𝐃 Π s

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Π_» : Lean.ParserDescr

The «term𝐈Π » construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Π₀» : Lean.ParserDescr

The «term𝐈Π₀» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Π₀» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Π₀» 1024 (Lean.ParserDescr.symbol "𝐈Π₀")

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Σ₁» : Lean.ParserDescr

The «term𝐈Σ₁» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Σ₁» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Σ₁» 1024 (Lean.ParserDescr.symbol "𝐈Σ₁")

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Π₁» : Lean.ParserDescr

The «term𝐈Π₁» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Π₁» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐈Π₁» 1024 (Lean.ParserDescr.symbol "𝐈Π₁")

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.Peano : ArithmeticTheory

The 𝐏𝐀 construction in 𝐏𝐀.

Equations

• 𝐏𝐀 = 𝐏𝐀⁻ ∪ PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionScheme ℒₒᵣ Set.univ

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐏𝐀» : Lean.ParserDescr

The «term𝐏𝐀» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐏𝐀» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐏𝐀» 1024 (Lean.ParserDescr.symbol "𝐏𝐀")

Least number schemata

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

The Least Number Scheme construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[reducible, inline]

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

The Least Number On Hierarchy construction in FFL.FirstOrder.Arithmetic.

Equations

• 𝐋 Γ s = 𝐏𝐀⁻ ∪ PointwiseComposition.FFL.FirstOrder.Arithmetic.LeastNumberScheme (PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy Γ s)

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

The «term𝐋 » construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[reducible, inline]

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

The LSigma construction in FFL.FirstOrder.Arithmetic.

Equations

• 𝐋Σs = 𝐋 Σ s

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐋Σ_» : Lean.ParserDescr

The «term𝐋Σ » construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[reducible, inline]

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

The LPi construction in FFL.FirstOrder.Arithmetic.

Equations

• 𝐋Πs = 𝐋 Π s

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐋Π_» : Lean.ParserDescr

The «term𝐋Π » construction in FFL.FirstOrder.Arithmetic.

Equations

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

Induction scheme lemmas

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

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

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.ISigma_subset_mono {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : 𝐈Σs₁ ⊆ 𝐈Σs₂

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.ISigma_weakerThan_of_le {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : 𝐈Σs₁ ≼ 𝐈Σs₂

theorem PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.LeastNumberScheme_subset {C C' : ArithmeticSemiformula ℕ 1 → Prop} (h : ∀ {φ : ArithmeticSemiformula ℕ 1}, C φ → C' φ) : LeastNumberScheme C ⊆ LeastNumberScheme C'

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

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.LeastNumberOnHierarchy_weakerThan_of_le {Γ : Polarity} {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : 𝐋 Γ s₁ ≼ 𝐋 Γ s₂

Relations between the theories

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiomInductionOnHierarchy {Γ : Polarity} {s : ℕ} : 𝐄𝐐 ℒₒᵣ ≼ 𝐈𝐍𝐃 Γ s

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiomIOpen : 𝐄𝐐 ℒₒᵣ ≼ 𝐈𝐎𝐩𝐞𝐧

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryIOpenInductionOnHierarchy {Γ : Polarity} {s : ℕ} : 𝐈𝐎𝐩𝐞𝐧 ≼ 𝐈𝐍𝐃 Γ s

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryISigmaOfNatNat : 𝐈Σ₀ ≼ 𝐈Σ₁

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryISigmaPeano {s : ℕ} : 𝐈Σs ≼ 𝐏𝐀

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusIOpen : 𝐏𝐀⁻ ≼ 𝐈𝐎𝐩𝐞𝐧

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryIOpenISigmaOfNatNat : 𝐈𝐎𝐩𝐞𝐧 ≼ 𝐈Σ₀

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryISigmaOfNatNatPeano : 𝐈Σ₁ ≼ 𝐏𝐀

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiomPeano : 𝐄𝐐 ℒₒᵣ ≼ 𝐏𝐀

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusLeastNumberOnHierarchy (Γ : Polarity) (s : ℕ) : 𝐏𝐀⁻ ≼ 𝐋 Γ s

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiomLeastNumberOnHierarchy (Γ : Polarity) (s : ℕ) : 𝐄𝐐 ℒₒᵣ ≼ 𝐋 Γ s

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.eq_weakerThan_of_ISigma {T : ArithmeticTheory} {s : ℕ} [𝐈Σs ≼ T] : 𝐄𝐐 ℒₒᵣ ≼ T

theorem PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrInductionSchemeHierarchyNat {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝐈𝐍𝐃 Γ s] : V↓[ℒₒᵣ] ⊧* InductionScheme ℒₒᵣ (Hierarchy Γ s)

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionOnHierarchy.models_InductionScheme_alt {V : Type u_1} [ORingStructure V] (Γ : Polarity) (s : ℕ) [V↓[ℒₒᵣ] ⊧* 𝐈𝐍𝐃 Γ s] : V↓[ℒₒᵣ] ⊧* InductionScheme ℒₒᵣ (Hierarchy Γ.alt s)

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrOfSigmaPolarity {V : Type u_1} [ORingStructure V] {s : ℕ} {Γ : Polarity} [V↓[ℒₒᵣ] ⊧* 𝐈𝐍𝐃 Σ s] : V↓[ℒₒᵣ] ⊧* 𝐈𝐍𝐃 Γ s

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrOfPiPolarity {V : Type u_1} [ORingStructure V] {s : ℕ} {Γ : Polarity} [V↓[ℒₒᵣ] ⊧* 𝐈𝐍𝐃 Π s] : V↓[ℒₒᵣ] ⊧* 𝐈𝐍𝐃 Γ s

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

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrIPiOfISigma {V : Type u_1} [ORingStructure V] {s : ℕ} [V↓[ℒₒᵣ] ⊧* 𝐈Σs] : V↓[ℒₒᵣ] ⊧* 𝐈Πs

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrISigmaOfIPi {V : Type u_1} [ORingStructure V] {s : ℕ} [V↓[ℒₒᵣ] ⊧* 𝐈Πs] : V↓[ℒₒᵣ] ⊧* 𝐈Σs

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionOnHierarchy.models_ISigma_iff_models_IPi {V : Type u_1} [ORingStructure V] {s : ℕ} : V↓[ℒₒᵣ] ⊧* 𝐈Σs ↔ V↓[ℒₒᵣ] ⊧* 𝐈Πs

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrOfISigma {V : Type u_1} [ORingStructure V] {s : ℕ} {Γ : Polarity} [V↓[ℒₒᵣ] ⊧* 𝐈Σs] : V↓[ℒₒᵣ] ⊧* 𝐈𝐍𝐃 Γ s

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrPeanoMinusOfIOpen {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrIOpenOfISigmaOfNatNat {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₀] : V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧

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

@[reducible, inline]

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

The mod ISigma of le construction in FFL.FirstOrder.Arithmetic.

Equations

• ⋯ = ⋯

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_paMinus_of_ISigma {V : Type u_1} [ORingStructure V] {s : ℕ} [V↓[ℒₒᵣ] ⊧* 𝐈Σs] : V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrISigmaOfPeano {V : Type u_1} [ORingStructure V] {s : ℕ} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀] : V↓[ℒₒᵣ] ⊧* 𝐈Σs

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.models_ISigma (Γ : Polarity) (s : ℕ) : ℕ↓[ℒₒᵣ] ⊧* 𝐈𝐍𝐃 Γ s

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.models_ISigmaZero : ℕ↓[ℒₒᵣ] ⊧* 𝐈Σ₀

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.models_ISigmaOne : ℕ↓[ℒₒᵣ] ⊧* 𝐈Σ₁

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.models_Peano : ℕ↓[ℒₒᵣ] ⊧* 𝐏𝐀

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.sigmaOneSound_ISigmaOne : 𝐈Σ₁.SoundOnHierarchy Σ 1

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.sigmaOneSound_Peano : 𝐏𝐀.SoundOnHierarchy Σ 1

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instConsistentSentenceORingArithmeticTheoryInductionOnHierarchy {Γ : Polarity} {s : ℕ} : Entailment.Consistent (𝐈𝐍𝐃 Γ s)

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instConsistentSentenceORingArithmeticTheoryPeano : Entailment.Consistent 𝐏𝐀

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoFirstOrderTrueArith : 𝐏𝐀 ≼ 𝐓𝐀

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryR0OfPeanoMinus (T : ArithmeticTheory) [𝐏𝐀⁻ ≼ T] : 𝐑₀ ≼ T

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusOfISigmaOfNatNat (T : ArithmeticTheory) [𝐈Σ₀ ≼ T] : 𝐏𝐀⁻ ≼ T

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusOfISigmaOfNatNat_1 (T : ArithmeticTheory) [𝐈Σ₁ ≼ T] : 𝐏𝐀⁻ ≼ T

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusOfPeano (T : ArithmeticTheory) [𝐏𝐀 ≼ T] : 𝐏𝐀⁻ ≼ T