Induction schemata of Arithmetic #
def
LO.FirstOrder.succInd
{L : Language}
[L.ORing]
{ΞΎ : Type u_3}
(Ο : Semiformula L ΞΎ 1)
:
Formula L ΞΎ
Equations
Instances For
def
LO.FirstOrder.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.
Instances For
def
LO.FirstOrder.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.
Instances For
def
LO.InductionScheme
(L : FirstOrder.Language)
[L.ORing]
(Ξ : FirstOrder.Semiformula L β 1 β Prop)
:
Equations
- LO.InductionScheme L Ξ = {Ο : LO.FirstOrder.SyntacticFormula L | β (Ο : LO.FirstOrder.Semiformula L β 1), Ξ Ο β§ Ο = LO.FirstOrder.succInd Ο}
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Β«termπOpenΒ» = Lean.ParserDescr.node `LO.Β«termπOpenΒ» 1024 (Lean.ParserDescr.symbol "πOpen")
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.Β«termπππ_Β» = Lean.ParserDescr.node `LO.Β«termπππ_Β» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "πππ ") (Lean.ParserDescr.cat `term 1024))
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.Β«termππΊ_Β» = Lean.ParserDescr.node `LO.Β«termππΊ_Β» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ππΊ") (Lean.ParserDescr.cat `term 1024))
Instances For
Equations
- LO.Β«termππΊβΒ» = Lean.ParserDescr.node `LO.Β«termππΊβΒ» 1024 (Lean.ParserDescr.symbol "ππΊβ")
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.Β«termππ·_Β» = Lean.ParserDescr.node `LO.Β«termππ·_Β» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ππ·") (Lean.ParserDescr.cat `term 1024))
Instances For
Equations
- LO.Β«termππ·βΒ» = Lean.ParserDescr.node `LO.Β«termππ·βΒ» 1024 (Lean.ParserDescr.symbol "ππ·β")
Instances For
Equations
- LO.Β«termππΊβΒ» = Lean.ParserDescr.node `LO.Β«termππΊβΒ» 1024 (Lean.ParserDescr.symbol "ππΊβ")
Instances For
Equations
- LO.Β«termππ·βΒ» = Lean.ParserDescr.node `LO.Β«termππ·βΒ» 1024 (Lean.ParserDescr.symbol "ππ·β")
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.Β«termππΒ» = Lean.ParserDescr.node `LO.Β«termππΒ» 1024 (Lean.ParserDescr.symbol "ππ")
Instances For
theorem
LO.InductionScheme_subset
{C C' : FirstOrder.Semiformula ββα΅£ β 1 β Prop}
(h : β {Ο : FirstOrder.Semiformula ββα΅£ β 1}, C Ο β C' Ο)
:
instance
LO.instWeakerThanSyntacticFormulaORingArithmeticTheoryPeanoMinusInductionOnHierarchy
{Ξ : Polarity}
{n : β}
:
instance
LO.instWeakerThanSyntacticFormulaORingTheoryArithmeticTheoryEqAxiomInductionOnHierarchy
{Ξ : Polarity}
{n : β}
:
instance
LO.instWeakerThanSyntacticFormulaORingArithmeticTheoryIOpenInductionOnHierarchy
{Ξ : Polarity}
{n : β}
:
theorem
LO.mem_InductionScheme_of_mem
{C : FirstOrder.Semiformula ββα΅£ β 1 β Prop}
{Ο : FirstOrder.Semiformula ββα΅£ β 1}
(hp : C Ο)
:
theorem
LO.InductionScheme.succ_induction
{V : Type u_1}
[ORingStruc V]
{C : FirstOrder.Semiformula ββα΅£ β 1 β Prop}
[V β§β* InductionScheme ββα΅£ 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
instance
LO.InductionOnHierarchy.instModelsTheoryInductionSchemeORingHierarchyNat
{V : Type u_1}
[ORingStruc V]
(Ξ : Polarity)
(m : β)
[V β§β* πππ Ξ m]
:
theorem
LO.InductionOnHierarchy.succ_induction
{V : Type u_1}
[ORingStruc V]
(Ξ : Polarity)
(m : β)
[V β§β* πππ Ξ 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.InductionOnHierarchy.order_induction
{V : Type u_1}
[ORingStruc V]
(Ξ : Polarity)
(m : β)
[V β§β* πππ Ξ m]
{P : V β Prop}
(hP : { Ξ := Ξ.coe, rank := m }-Predicate P)
(ind : β (x : V), (β y < x, P y) β P x)
(x : V)
:
P x
instance
LO.InductionOnHierarchy.models_InductionScheme_alt
{V : Type u_1}
[ORingStruc V]
(Ξ : Polarity)
(m : β)
[V β§β* πππ Ξ m]
:
instance
LO.InductionOnHierarchy.models_alt
{V : Type u_1}
[ORingStruc V]
(Ξ : Polarity)
(m : β)
[V β§β* πππ Ξ m]
:
theorem
LO.InductionOnHierarchy.least_number
{V : Type u_1}
[ORingStruc V]
(Ξ : Polarity)
(m : β)
[V β§β* πππ Ξ m]
{P : V β Prop}
(hP : { Ξ := Ξ.coe, rank := m }-Predicate P)
{x : V}
(h : P x)
:
theorem
LO.InductionOnHierarchy.succ_induction_sigma
{V : Type u_1}
[ORingStruc V]
(Ξ : SigmaPiDelta)
(m : β)
[V β§β* πππ πΊ 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.InductionOnHierarchy.order_induction_sigma
{V : Type u_1}
[ORingStruc V]
(Ξ : SigmaPiDelta)
(m : β)
[V β§β* πππ πΊ m]
{P : V β Prop}
(hP : { Ξ := Ξ, rank := m }-Predicate P)
(ind : β (x : V), (β y < x, P y) β P x)
(x : V)
:
P x
theorem
LO.InductionOnHierarchy.least_number_sigma
{V : Type u_1}
[ORingStruc V]
(Ξ : SigmaPiDelta)
(m : β)
[V β§β* πππ πΊ m]
{P : V β Prop}
(hP : { Ξ := Ξ, rank := m }-Predicate P)
{x : V}
(h : P x)
:
instance
LO.InductionOnHierarchy.instModelsTheoryOfSigmaPolarity
{V : Type u_1}
[ORingStruc V]
{m : β}
{Ξ : Polarity}
[V β§β* πππ πΊ m]
:
instance
LO.InductionOnHierarchy.instModelsTheoryOfPiPolarity
{V : Type u_1}
[ORingStruc V]
{m : β}
{Ξ : Polarity}
[V β§β* πππ π· m]
:
theorem
LO.InductionOnHierarchy.mod_ISigma_of_le
{V : Type u_1}
[ORingStruc V]
{nβ nβ : β}
(h : nβ β€ nβ)
[V β§β* ππΊnβ]
:
instance
LO.InductionOnHierarchy.instModelsTheoryISigmaOfNatNat
{V : Type u_1}
[ORingStruc V]
[V β§β* ππΊβ]
:
instance
LO.InductionOnHierarchy.instModelsTheoryIPiOfISigma
{V : Type u_1}
[ORingStruc V]
{n : β}
[V β§β* ππΊn]
:
instance
LO.InductionOnHierarchy.instModelsTheoryISigmaOfIPi
{V : Type u_1}
[ORingStruc V]
{n : β}
[V β§β* ππ·n]
:
theorem
LO.InductionOnHierarchy.models_ISigma_iff_models_IPi
{V : Type u_1}
[ORingStruc V]
{n : β}
:
instance
LO.InductionOnHierarchy.instModelsTheoryOfISigma
{V : Type u_1}
[ORingStruc V]
{n : β}
{Ξ : Polarity}
[V β§β* ππΊn]
:
theorem
LO.ISigma0.succ_induction
{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.ISigma1.sigma1_succ_induction
{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.ISigma1.pi1_succ_induction
{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.ISigma0.order_induction
{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.ISigma1.sigma1_order_induction
{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.ISigma1.pi1_order_induction
{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.ISigma0.least_number
{V : Type u_1}
[ORingStruc V]
[V β§β* ππΊβ]
{P : V β Prop}
(hP : πΊβ-Predicate P)
{x : V}
(h : P x)
:
theorem
LO.ISigma1.succ_induction
{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.ISigma1.order_induction
{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
instance
LO.instModelsTheoryIOpenOfISigmaOfNatNat
{V : Type u_1}
[ORingStruc V]
[V β§β* ππΊβ]
:
instance
LO.instConsistentSyntacticFormulaORingArithmeticTheoryInductionOnHierarchy
{Ξ : Polarity}
{k : β}
: