Documentation

Foundation.FirstOrder.Arithmetic.Schemata

Induction schemata of Arithmetic #

source
def LO.FirstOrder.Arithmetic.succInd {L : Language} [L.ORing] {ΞΎ : Type u_3} (Ο† : Semiformula L ΞΎ 1) :
Formula L ΞΎ
Equations
Instances For
    source
    def LO.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.
    Instances For
      source
      def LO.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.
      Instances For
        source
        def LO.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.
        Instances For
          source
          @[reducible, inline]
          abbrev LO.FirstOrder.Arithmetic.IOpen :
          ArithmeticTheory
          Equations
          Instances For
            source
            def LO.FirstOrder.Arithmetic.Β«termπ—œπ—’π—½π—²π—»Β» :
            Lean.ParserDescr
            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev LO.FirstOrder.Arithmetic.InductionOnHierarchy (Ξ“ : Polarity) (k : β„•) :
              ArithmeticTheory
              Equations
              Instances For
                source
                def LO.FirstOrder.Arithmetic.Β«termπ—œπ—‘π——_Β» :
                Lean.ParserDescr
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[reducible, inline]
                  abbrev LO.FirstOrder.Arithmetic.ISigma (k : β„•) :
                  ArithmeticTheory
                  Equations
                  Instances For
                    source
                    def LO.FirstOrder.Arithmetic.Β«termπ—œπšΊ_Β» :
                    Lean.ParserDescr
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def LO.FirstOrder.Arithmetic.Β«termπ—œπšΊβ‚€Β» :
                      Lean.ParserDescr
                      Equations
                      Instances For
                        source
                        @[reducible, inline]
                        abbrev LO.FirstOrder.Arithmetic.IPi (k : β„•) :
                        ArithmeticTheory
                        Equations
                        Instances For
                          source
                          def LO.FirstOrder.Arithmetic.Β«termπ—œπš·_Β» :
                          Lean.ParserDescr
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def LO.FirstOrder.Arithmetic.Β«termπ—œπš·β‚€Β» :
                            Lean.ParserDescr
                            Equations
                            Instances For
                              source
                              def LO.FirstOrder.Arithmetic.Β«termπ—œπšΊβ‚Β» :
                              Lean.ParserDescr
                              Equations
                              Instances For
                                source
                                def LO.FirstOrder.Arithmetic.Β«termπ—œπš·β‚Β» :
                                Lean.ParserDescr
                                Equations
                                Instances For
                                  source
                                  @[reducible, inline]
                                  abbrev LO.FirstOrder.Arithmetic.Peano :
                                  ArithmeticTheory
                                  Equations
                                  Instances For
                                    source
                                    def LO.FirstOrder.Arithmetic.Β«term𝗣𝗔» :
                                    Lean.ParserDescr
                                    Equations
                                    Instances For
                                      source
                                      theorem LO.FirstOrder.Arithmetic.InductionScheme_subset {C C' : ArithmeticSemiformula β„• 1 β†’ Prop} (h : βˆ€ {Ο† : ArithmeticSemiformula β„• 1}, C Ο† β†’ C' Ο†) :
                                      InductionScheme β„’β‚’α΅£ C βŠ† InductionScheme β„’β‚’α΅£ C'
                                      source
                                      theorem LO.FirstOrder.Arithmetic.ISigma_subset_mono {s₁ sβ‚‚ : β„•} (h : s₁ ≀ sβ‚‚) :
                                      π—œπšΊs₁ βŠ† π—œπšΊsβ‚‚
                                      source
                                      theorem LO.FirstOrder.Arithmetic.ISigma_weakerThan_of_le {s₁ sβ‚‚ : β„•} (h : s₁ ≀ sβ‚‚) :
                                      π—œπšΊs₁ βͺ― π—œπšΊsβ‚‚
                                      source
                                      instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiomInductionOnHierarchy {Ξ“ : Polarity} {n : β„•} :
                                      π—˜π—€ β„’β‚’α΅£ βͺ― π—œπ—‘π—— Ξ“ n
                                      source
                                      instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiomIOpen :
                                      π—˜π—€ β„’β‚’α΅£ βͺ― π—œπ—’π—½π—²π—»
                                      source
                                      instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryIOpenInductionOnHierarchy {Ξ“ : Polarity} {n : β„•} :
                                      π—œπ—’π—½π—²π—» βͺ― π—œπ—‘π—— Ξ“ n
                                      source
                                      instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryISigmaOfNatNat :
                                      π—œπšΊβ‚€ βͺ― π—œπšΊβ‚
                                      source
                                      instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryISigmaPeano {i : β„•} :
                                      π—œπšΊi βͺ― 𝗣𝗔
                                      source
                                      theorem LO.FirstOrder.Arithmetic.mem_InductionScheme_of_mem {C : ArithmeticSemiformula β„• 1 β†’ Prop} {Ο† : ArithmeticSemiformula β„• 1} (hp : C Ο†) :
                                      Semiformula.univCl (succInd Ο†) ∈ InductionScheme β„’β‚’α΅£ C
                                      source
                                      theorem LO.FirstOrder.Arithmetic.mem_IOpen_of_qfree {Ο† : ArithmeticSemiformula β„• 1} (hp : Semiformula.Open Ο†) :
                                      Semiformula.univCl (succInd Ο†) ∈ InductionScheme β„’β‚’α΅£ Semiformula.Open
                                      source
                                      instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusIOpen :
                                      𝗣𝗔⁻ βͺ― π—œπ—’π—½π—²π—»
                                      source
                                      instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryIOpenISigmaOfNatNat :
                                      π—œπ—’π—½π—²π—» βͺ― π—œπšΊβ‚€
                                      source
                                      instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryISigmaOfNatNatPeano :
                                      π—œπšΊβ‚ βͺ― 𝗣𝗔
                                      source
                                      theorem LO.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
                                      source
                                      instance LO.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrInductionSchemeHierarchyNat {V : Type u_1} [ORingStructure V] (Ξ“ : Polarity) (m : β„•) [V↓[β„’β‚’α΅£] ⊧* π—œπ—‘π—— Ξ“ m] :
                                      V↓[β„’β‚’α΅£] ⊧* InductionScheme β„’β‚’α΅£ (Hierarchy Ξ“ m)
                                      source
                                      theorem LO.FirstOrder.Arithmetic.InductionOnHierarchy.succ_induction {V : Type u_1} [ORingStructure 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
                                      source
                                      theorem LO.FirstOrder.Arithmetic.InductionOnHierarchy.order_induction {V : Type u_1} [ORingStructure 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
                                      source
                                      instance LO.FirstOrder.Arithmetic.InductionOnHierarchy.models_InductionScheme_alt {V : Type u_1} [ORingStructure V] (Ξ“ : Polarity) (m : β„•) [V↓[β„’β‚’α΅£] ⊧* π—œπ—‘π—— Ξ“ m] :
                                      V↓[β„’β‚’α΅£] ⊧* InductionScheme β„’β‚’α΅£ (Hierarchy Ξ“.alt m)
                                      source
                                      instance LO.FirstOrder.Arithmetic.InductionOnHierarchy.models_alt {V : Type u_1} [ORingStructure V] (Ξ“ : Polarity) (m : β„•) [V↓[β„’β‚’α΅£] ⊧* π—œπ—‘π—— Ξ“ m] :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπ—‘π—— Ξ“.alt m
                                      source
                                      theorem LO.FirstOrder.Arithmetic.InductionOnHierarchy.least_number {V : Type u_1} [ORingStructure 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
                                      source
                                      theorem LO.FirstOrder.Arithmetic.InductionOnHierarchy.succ_induction_sigma {V : Type u_1} [ORingStructure 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
                                      source
                                      theorem LO.FirstOrder.Arithmetic.InductionOnHierarchy.order_induction_sigma {V : Type u_1} [ORingStructure 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
                                      source
                                      theorem LO.FirstOrder.Arithmetic.InductionOnHierarchy.least_number_sigma {V : Type u_1} [ORingStructure 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
                                      source
                                      instance LO.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrOfSigmaPolarity {V : Type u_1} [ORingStructure V] {m : β„•} {Ξ“ : Polarity} [V↓[β„’β‚’α΅£] ⊧* π—œπ—‘π—— 𝚺 m] :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπ—‘π—— Ξ“ m
                                      source
                                      instance LO.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrOfPiPolarity {V : Type u_1} [ORingStructure V] {m : β„•} {Ξ“ : Polarity} [V↓[β„’β‚’α΅£] ⊧* π—œπ—‘π—— 𝚷 m] :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπ—‘π—— Ξ“ m
                                      source
                                      theorem LO.FirstOrder.Arithmetic.InductionOnHierarchy.mod_ISigma_of_le {V : Type u_1} [ORingStructure V] {n₁ nβ‚‚ : β„•} (h : n₁ ≀ nβ‚‚) [V↓[β„’β‚’α΅£] ⊧* π—œπšΊnβ‚‚] :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπšΊn₁
                                      source
                                      instance LO.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrISigmaOfNatNat {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚€
                                      source
                                      instance LO.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrIPiOfISigma {V : Type u_1} [ORingStructure V] {n : β„•} [V↓[β„’β‚’α΅£] ⊧* π—œπšΊn] :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπš·n
                                      source
                                      instance LO.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrISigmaOfIPi {V : Type u_1} [ORingStructure V] {n : β„•} [V↓[β„’β‚’α΅£] ⊧* π—œπš·n] :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπšΊn
                                      source
                                      theorem LO.FirstOrder.Arithmetic.InductionOnHierarchy.models_ISigma_iff_models_IPi {V : Type u_1} [ORingStructure V] {n : β„•} :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπšΊn ↔ V↓[β„’β‚’α΅£] ⊧* π—œπš·n
                                      source
                                      instance LO.FirstOrder.Arithmetic.InductionOnHierarchy.instModelsSetStrucORingSentenceStrOfISigma {V : Type u_1} [ORingStructure V] {n : β„•} {Ξ“ : Polarity} [V↓[β„’β‚’α΅£] ⊧* π—œπšΊn] :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπ—‘π—— Ξ“ n
                                      source
                                      theorem LO.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
                                      source
                                      theorem LO.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
                                      source
                                      theorem LO.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
                                      source
                                      theorem LO.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
                                      source
                                      theorem LO.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
                                      source
                                      theorem LO.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
                                      source
                                      theorem LO.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
                                      source
                                      theorem LO.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
                                      source
                                      theorem LO.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
                                      source
                                      instance LO.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrPeanoMinusOfIOpen {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπ—’π—½π—²π—»] :
                                      V↓[β„’β‚’α΅£] ⊧* 𝗣𝗔⁻
                                      source
                                      instance LO.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrIOpenOfISigmaOfNatNat {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚€] :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπ—’π—½π—²π—»
                                      source
                                      instance LO.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrISigmaOfNatNat {V : Type u_1} [ORingStructure V] [V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚] :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚€
                                      source
                                      @[reducible, inline]
                                      abbrev LO.FirstOrder.Arithmetic.mod_ISigma_of_le {V : Type u_1} [ORingStructure V] {n₁ nβ‚‚ : β„•} (h : n₁ ≀ nβ‚‚) [V↓[β„’β‚’α΅£] ⊧* π—œπšΊnβ‚‚] :
                                      V↓[β„’β‚’α΅£] ⊧* π—œπšΊn₁
                                      Equations
                                      • β‹― = β‹―
                                      Instances For
                                        source
                                        theorem LO.FirstOrder.Arithmetic.models_succInd (Ο† : ArithmeticSemiformula β„• 1) :
                                        ℕ↓[β„’β‚’α΅£] ⊧ Semiformula.univCl (succInd Ο†)
                                        source
                                        instance LO.FirstOrder.Arithmetic.models_ISigma (Ξ“ : Polarity) (k : β„•) :
                                        ℕ↓[β„’β‚’α΅£] ⊧* π—œπ—‘π—— Ξ“ k
                                        source
                                        instance LO.FirstOrder.Arithmetic.models_ISigmaZero :
                                        ℕ↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚€
                                        source
                                        instance LO.FirstOrder.Arithmetic.models_ISigmaOne :
                                        ℕ↓[β„’β‚’α΅£] ⊧* π—œπšΊβ‚
                                        source
                                        instance LO.FirstOrder.Arithmetic.models_Peano :
                                        ℕ↓[β„’β‚’α΅£] ⊧* 𝗣𝗔
                                        source
                                        instance LO.FirstOrder.Arithmetic.instConsistentSentenceORingArithmeticTheoryInductionOnHierarchy {Ξ“ : Polarity} {k : β„•} :
                                        Entailment.Consistent (π—œπ—‘π—— Ξ“ k)
                                        source
                                        instance LO.FirstOrder.Arithmetic.instConsistentSentenceORingArithmeticTheoryPeano :
                                        Entailment.Consistent 𝗣𝗔
                                        source
                                        instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoFirstOrderTrueArith :
                                        𝗣𝗔 βͺ― 𝗧𝗔
                                        source
                                        instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryR0OfPeanoMinus (T : ArithmeticTheory) [𝗣𝗔⁻ βͺ― T] :
                                        π—₯β‚€ βͺ― T
                                        source
                                        instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusOfISigmaOfNatNat (T : ArithmeticTheory) [π—œπšΊβ‚€ βͺ― T] :
                                        𝗣𝗔⁻ βͺ― T
                                        source
                                        instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusOfISigmaOfNatNat_1 (T : ArithmeticTheory) [π—œπšΊβ‚ βͺ― T] :
                                        𝗣𝗔⁻ βͺ― T
                                        source
                                        instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryPeanoMinusOfPeano (T : ArithmeticTheory) [𝗣𝗔 βͺ― T] :
                                        𝗣𝗔⁻ βͺ― T