Documentation

Foundation.FirstOrder.Arith.Induction

Induction schemata of Arithmetic #

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
      Equations
      Instances For
        Equations
        Instances For
          @[reducible, inline]
          Equations
          Instances For
            Equations
            Instances For
              Equations
              Instances For
                @[reducible, inline]
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    Instances For
                      Equations
                      Instances For
                        Equations
                        Instances For
                          Equations
                          Instances For
                            theorem LO.ISigma_subset_mono {s₁ sβ‚‚ : β„•} (h : s₁ ≀ sβ‚‚) :
                            theorem LO.ISigma_weakerThan_of_le {s₁ sβ‚‚ : β„•} (h : s₁ ≀ sβ‚‚) :
                            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
                            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
                            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) :
                            βˆƒ (y : V), P y ∧ βˆ€ z < y, Β¬P z
                            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) :
                            βˆƒ (y : V), P y ∧ βˆ€ z < y, Β¬P z
                            theorem LO.InductionOnHierarchy.mod_ISigma_of_le {V : Type u_1} [ORingStruc V] {n₁ nβ‚‚ : β„•} (h : n₁ ≀ nβ‚‚) [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) :
                            βˆƒ (y : V), P y ∧ βˆ€ z < y, Β¬P z
                            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
                            def LO.mod_ISigma_of_le {V : Type u_1} [ORingStruc V] {n₁ nβ‚‚ : β„•} (h : n₁ ≀ nβ‚‚) [V βŠ§β‚˜* 𝐈𝚺nβ‚‚] :
                            Equations
                            • β‹― = β‹―
                            Instances For