Documentation

Foundation.FirstOrder.Arithmetic.R0.Basic

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

source
inductive LO.FirstOrder.Arithmetic.R0 :
ArithmeticTheory
Instances For
    source
    def LO.FirstOrder.Arithmetic.Β«termπ—₯β‚€Β» :
    Lean.ParserDescr
    Equations
    Instances For
      source
      instance LO.FirstOrder.Arithmetic.R0.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiom :
      π—˜π—€ β„’β‚’α΅£ βͺ― π—₯β‚€
      source
      instance LO.FirstOrder.Arithmetic.R0.instModelsSetStrucORingSentenceStrNat :
      ℕ↓[β„’β‚’α΅£] ⊧* π—₯β‚€
      source
      theorem LO.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 LO.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 LO.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
      theorem LO.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
      @[simp]
      theorem LO.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 LO.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 LO.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 LO.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 LO.FirstOrder.Arithmetic.R0.model_complete {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* π—₯β‚€] {Οƒ : ArithmeticSentence} (hΟƒ : Hierarchy 𝚺 1 Οƒ) :
      ℕ↓[β„’β‚’α΅£] ⊧ Οƒ β†’ M↓[β„’β‚’α΅£] ⊧ Οƒ
      source
      theorem LO.FirstOrder.Arithmetic.nat_extention_sigmaOne (M : Type u_1) [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* π—₯β‚€] {Οƒ : ArithmeticSentence} (hΟƒ : Hierarchy 𝚺 1 Οƒ) :
      ℕ↓[β„’β‚’α΅£] ⊧ Οƒ β†’ M↓[β„’β‚’α΅£] ⊧ Οƒ
      source
      theorem LO.FirstOrder.Arithmetic.nat_extention_piOne (M : Type u_1) [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* π—₯β‚€] {Οƒ : ArithmeticSentence} (hΟƒ : Hierarchy 𝚷 1 Οƒ) :
      M↓[β„’β‚’α΅£] ⊧ Οƒ β†’ ℕ↓[β„’β‚’α΅£] ⊧ Οƒ
      source
      theorem LO.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 LO.FirstOrder.Arithmetic.consistent :
      Entailment.Consistent π—₯β‚€
      source
      theorem LO.FirstOrder.Arithmetic.sigma_one_completeness {T : ArithmeticTheory} [π—₯β‚€ βͺ― T] {Οƒ : ArithmeticSentence} (hΟƒ : Hierarchy 𝚺 1 Οƒ) :
      ℕ↓[β„’β‚’α΅£] ⊧ Οƒ β†’ T ⊒ Οƒ
      source
      theorem LO.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 LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne :
      Type
      Equations
      Instances For
        source
        @[implicit_reducible]
        instance LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.instNatCast :
        NatCast OmegaAddOne
        Equations
        source
        @[implicit_reducible]
        instance LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.instOfNat (n : β„•) :
        OfNat OmegaAddOne n
        Equations
        source
        @[implicit_reducible]
        instance LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.instTop :
        Top OmegaAddOne
        Equations
        source
        @[implicit_reducible]
        instance LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.instORingStructure :
        ORingStructure OmegaAddOne
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.coe_zero :
        ↑0 = 0
        source
        @[simp]
        theorem LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.coe_one :
        ↑1 = 1
        source
        @[simp]
        theorem LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.coe_add (a b : β„•) :
        ↑(a + b) = ↑a + ↑b
        source
        @[simp]
        theorem LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.coe_mul (a b : β„•) :
        ↑(a * b) = ↑a * ↑b
        source
        @[simp]
        theorem LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.lt_coe_iff (n m : β„•) :
        ↑n < ↑m ↔ n < m
        source
        @[simp]
        theorem LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.not_top_lt (n : β„•) :
        ¬⊀ < ↑n
        source
        @[simp]
        theorem LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.lt_top (n : β„•) :
        ↑n < ⊀
        source
        @[simp]
        theorem LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.top_add_zero :
        ⊀ + 0 = 0
        source
        theorem LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.exists_add_zero_ne_self :
        βˆƒ (x : OmegaAddOne), x + 0 β‰  x
        source
        @[simp]
        theorem LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.numeral_eq (n : β„•) :
        ORingStructure.numeral n = ↑n
        source
        @[simp]
        theorem LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.coe_inj_iff (n m : β„•) :
        ↑n = ↑m ↔ n = m
        source
        def LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.cases' {P : OmegaAddOne β†’ Sort u_1} (nat : (n : β„•) β†’ P ↑n) (top : P ⊀) (x : OmegaAddOne) :
        P x
        Equations
        Instances For
          source
          instance LO.FirstOrder.Arithmetic.R0.Countermodel.OmegaAddOne.instModelsSetStrucORingSentenceStr :
          OmegaAddOne↓[β„’β‚’α΅£] ⊧* π—₯β‚€
          source
          theorem LO.FirstOrder.Arithmetic.R0.unprovable_addZero :
          π—₯β‚€ ⊬ (β€œβˆ€ΒΉ (!!(Semiterm.bvar 0) + 0) = !!(Semiterm.bvar 0)”)