Documentation

LeanPool.PointwiseComposition.Foundation.FirstOrder.Arithmetic.R0.Basic

Supporting results for pointwise provable equality.

Cobham's theory $\mathsf{R_0}$ #

source
inductive PointwiseComposition.FFL.FirstOrder.Arithmetic.R0 :
ArithmeticTheory

Data and laws for 𝐑₀ in 𝐑₀.

Instances For
    source
    def PointwiseComposition.FFL.FirstOrder.Arithmetic.Β«term𝐑₀» :
    Lean.ParserDescr

    The Β«term𝐑₀» construction in FFL.FirstOrder.Arithmetic.

    Equations
    Instances For
      source
      instance PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiom :
      𝐄𝐐 β„’β‚’α΅£ β‰Ό 𝐑₀
      source
      instance PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.instModelsSetStrucORingSentenceStrNat :
      ℕ↓[β„’β‚’α΅£] ⊧* 𝐑₀
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_add_numeral {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] (n m : β„•) :
      ORingStructure.numeral n + ORingStructure.numeral m = ORingStructure.numeral (n + m)
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_mul_numeral {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] (n m : β„•) :
      ORingStructure.numeral n * ORingStructure.numeral m = ORingStructure.numeral (n * m)
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_numeral_iff {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] {x : M} {n : β„•} :
      x < ORingStructure.numeral n ↔ βˆƒ (i : Fin n), x = ORingStructure.numeral ↑i
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.not_numeral_lt_self {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] (n : β„•) :
      Β¬ORingStructure.numeral n < ORingStructure.numeral n
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_ne_numeral_of_ne {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] {n m : β„•} (h : n β‰  m) :
      ORingStructure.numeral n β‰  ORingStructure.numeral m
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_inj_iff {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] {n m : β„•} :
      ORingStructure.numeral n = ORingStructure.numeral m ↔ n = m
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_lt_numeral_iff {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] {n m : β„•} :
      ORingStructure.numeral n < ORingStructure.numeral m ↔ n < m
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.val_numeral {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] {n : β„•} {ΞΎ : Type u_2} (bv : Fin n β†’ β„•) (fv : ΞΎ β†’ β„•) (t : ArithmeticSemiterm ΞΎ n) :
      Semiterm.val (ORingStructure.numeral ∘ bv) (ORingStructure.numeral ∘ fv) t = ORingStructure.numeral (Semiterm.val bv fv t)
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.bold_sigma_one_completeness {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] {ΞΎ : Type u_2} {n : β„•} {Ο† : ArithmeticSemiformula ΞΎ n} (hp : Hierarchy Ξ£ 1 Ο†) {bv : Fin n β†’ β„•} {fv : ΞΎ β†’ β„•} :
      (Semiformula.Eval bv fv) Ο† β†’ (Semiformula.Eval (ORingStructure.numeral ∘ bv) (ORingStructure.numeral ∘ fv)) Ο†
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.model_complete {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] {Οƒ : ArithmeticSentence} (hΟƒ : Hierarchy Ξ£ 1 Οƒ) :
      ℕ↓[β„’β‚’α΅£] ⊧ Οƒ β†’ M↓[β„’β‚’α΅£] ⊧ Οƒ
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nat_extention_sigmaOne (M : Type u_1) [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] {Οƒ : ArithmeticSentence} (hΟƒ : Hierarchy Ξ£ 1 Οƒ) :
      ℕ↓[β„’β‚’α΅£] ⊧ Οƒ β†’ M↓[β„’β‚’α΅£] ⊧ Οƒ
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nat_extention_piOne (M : Type u_1) [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] {Οƒ : ArithmeticSentence} (hΟƒ : Hierarchy Ξ  1 Οƒ) :
      M↓[β„’β‚’α΅£] ⊧ Οƒ β†’ ℕ↓[β„’β‚’α΅£] ⊧ Οƒ
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.bold_sigma_one_completeness' {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝐑₀] {n : β„•} {Οƒ : ArithmeticSemisentence n} (hΟƒ : Hierarchy Ξ£ 1 Οƒ) {bv : Fin n β†’ β„•} :
      (Semiformula.Evalb bv) Οƒ β†’ (Semiformula.Evalb (ORingStructure.numeral ∘ bv)) Οƒ
      source
      instance PointwiseComposition.FFL.FirstOrder.Arithmetic.consistent :
      Entailment.Consistent 𝐑₀
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sigma_one_completeness {T : ArithmeticTheory} [𝐑₀ β‰Ό T] {Οƒ : ArithmeticSentence} (hΟƒ : Hierarchy Ξ£ 1 Οƒ) :
      ℕ↓[β„’β‚’α΅£] ⊧ Οƒ β†’ T ⊒ Οƒ
      source
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sigma_one_completeness_iff {T : ArithmeticTheory} [𝐑₀ β‰Ό T] [T.SoundOnHierarchy Ξ£ 1] {Οƒ : ArithmeticSentence} (hΟƒ : Hierarchy Ξ£ 1 Οƒ) :
      ℕ↓[β„’β‚’α΅£] ⊧ Οƒ ↔ T ⊒ Οƒ

      Unprovable theorems of $\mathsf{R}_0$ #

      $\omega + 1$ (the structure of order type $\omega + 1$) is a models of $\mathsf{R}_0$.

      Ο‰ + 1 models 𝐑₀

      source
      def PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne :
      Type

      The Omega Add One construction in FFL.FirstOrder.Arithmetic.R0.Countermodel.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.instNatCast :
        NatCast OmegaAddOne
        Equations
        source
        @[instance_reducible]
        instance PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.instOfNat (n : β„•) :
        OfNat OmegaAddOne n
        Equations
        source
        @[instance_reducible]
        instance PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.instTop :
        Top OmegaAddOne
        Equations
        source
        @[instance_reducible]
        instance PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.instORingStructure :
        ORingStructure OmegaAddOne
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.coe_zero :
        ↑0 = 0
        source
        @[simp]
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.coe_one :
        ↑1 = 1
        source
        @[simp]
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.coe_add (a b : β„•) :
        ↑(a + b) = ↑a + ↑b
        source
        @[simp]
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.coe_mul (a b : β„•) :
        ↑(a * b) = ↑a * ↑b
        source
        @[simp]
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.lt_coe_iff (n m : β„•) :
        ↑n < ↑m ↔ n < m
        source
        @[simp]
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.not_top_lt (n : β„•) :
        ¬⊀ < ↑n
        source
        @[simp]
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.lt_top (n : β„•) :
        ↑n < ⊀
        source
        @[simp]
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.top_add_zero :
        ⊀ + 0 = 0
        source
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.exists_add_zero_ne_self :
        βˆƒ (x : OmegaAddOne), x + 0 β‰  x
        source
        @[simp]
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.numeral_eq (n : β„•) :
        ORingStructure.numeral n = ↑n
        source
        @[simp]
        theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.coe_inj_iff (n m : β„•) :
        ↑n = ↑m ↔ n = m
        source
        def PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.cases' {P : OmegaAddOne β†’ Sort u_1} (nat : (n : β„•) β†’ P ↑n) (top : P ⊀) (x : OmegaAddOne) :
        P x

        The cases' construction in FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.

        Equations
        Instances For
          source
          instance PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.instModelsSetStrucORingSentenceStr :
          OmegaAddOne↓[β„’β‚’α΅£] ⊧* 𝐑₀
          source
          theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.R0.unprovable_addZero :
          𝐑₀ ⊬ (β€œβˆ€ΒΉ (!!(Semiterm.bvar 0) + 0) = !!(Semiterm.bvar 0)”)