Documentation

Foundation.FirstOrder.Arithmetic.Q.Basic

Robinson's theory $\mathsf{Q}$ #

source
inductive LO.FirstOrder.Arithmetic.RobinsonQ :
ArithmeticTheory
Instances For
    source
    def LO.FirstOrder.Arithmetic.Β«term𝗀» :
    Lean.ParserDescr
    Equations
    Instances For
      source
      @[simp]
      instance LO.FirstOrder.Arithmetic.RobinsonQ.instModelsSetStrucORingSentenceStrNat :
      ℕ↓[β„’β‚’α΅£] ⊧* 𝗀
      source
      instance LO.FirstOrder.Arithmetic.RobinsonQ.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiom :
      π—˜π—€ β„’β‚’α΅£ βͺ― 𝗀
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.succ_ne_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] (a : M) :
      a + 1 β‰  0
      source
      theorem LO.FirstOrder.Arithmetic.succ_inj {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {a b : M} :
      a + 1 = b + 1 β†’ a = b
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.add_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {a : M} :
      a + 0 = a
      source
      theorem LO.FirstOrder.Arithmetic.add_succ {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] (a b : M) :
      a + (b + 1) = a + b + 1
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.mul_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] (a : M) :
      a * 0 = 0
      source
      theorem LO.FirstOrder.Arithmetic.mul_succ {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] (a b : M) :
      a * (b + 1) = a * b + a
      source
      theorem LO.FirstOrder.Arithmetic.zero_or_succ {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] (a : M) :
      a = 0 ∨ βˆƒ (b : M), a = b + 1
      source
      theorem LO.FirstOrder.Arithmetic.exists_succ_of_ne_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {a : M} (ha : a β‰  0) :
      βˆƒ (b : M), a = b + 1
      source
      theorem LO.FirstOrder.Arithmetic.exists_succ_of_ne_zero' {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {a : M} (ha : a β‰  0) :
      βˆƒ (b : M), b + 1 = a
      source
      theorem LO.FirstOrder.Arithmetic.lt_def {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {a b : M} :
      a < b ↔ βˆƒ (c : M), a + (c + 1) = b
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.one_ne_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] :
      1 β‰  0
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.one_add_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] :
      1 + 0 = 1
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.zero_add_one {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] :
      0 + 1 = 1
      source
      theorem LO.FirstOrder.Arithmetic.succ_inj_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {a : M} :
      a + 1 = 1 β†’ a = 0
      source
      theorem LO.FirstOrder.Arithmetic.eq_zero_of_eq_add_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {a b : M} (h : a + b = 0) :
      a = 0 ∧ b = 0
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.one_mul_one {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] :
      1 * 1 = 1
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.zero_mul_one {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] :
      0 * 1 = 0
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.not_le_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {a : M} :
      Β¬a < 0
      source
      theorem LO.FirstOrder.Arithmetic.lt_of_not_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {a b : M} (ha : b β‰  0) :
      a < a + b
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.iff_le_one_eq_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {a : M} :
      a < 1 ↔ a = 0
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.numeral_zero_add {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] (n : β„•) :
      0 + ORingStructure.numeral n = ORingStructure.numeral n
      source
      theorem LO.FirstOrder.Arithmetic.numeral_add_one {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] (n : β„•) :
      ORingStructure.numeral n + 1 = ORingStructure.numeral (n + 1)
      source
      theorem LO.FirstOrder.Arithmetic.numeral_add {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_zero_mul {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {n : β„•} :
      0 * ORingStructure.numeral n = 0
      source
      theorem LO.FirstOrder.Arithmetic.numeral_mul_one {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {n : β„•} :
      ORingStructure.numeral n * 1 = ORingStructure.numeral n
      source
      theorem LO.FirstOrder.Arithmetic.numeral_mul {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {n m : β„•} :
      ORingStructure.numeral n * ORingStructure.numeral m = ORingStructure.numeral (n * m)
      source
      theorem LO.FirstOrder.Arithmetic.exists_numeral_of_ne_zero {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {n : β„•} (h : n β‰  0) :
      βˆƒ (m : β„•), ORingStructure.numeral n = ORingStructure.numeral (m + 1)
      source
      theorem LO.FirstOrder.Arithmetic.numeral_zero_succ_ne {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {n : β„•} :
      ORingStructure.numeral 0 β‰  ORingStructure.numeral (n + 1)
      source
      theorem LO.FirstOrder.Arithmetic.numeral_succ_inj {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {n m : β„•} (h : ORingStructure.numeral (n + 1) = ORingStructure.numeral (m + 1)) :
      ORingStructure.numeral n = ORingStructure.numeral m
      source
      theorem LO.FirstOrder.Arithmetic.numeral_ne_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.numeral_lt_of_lt {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {n m : β„•} (h : n < m) :
      ORingStructure.numeral n < ORingStructure.numeral m
      source
      theorem LO.FirstOrder.Arithmetic.numeral_lt_add {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {n m : β„•} (hm : m β‰  0) :
      ORingStructure.numeral n < ORingStructure.numeral n + ORingStructure.numeral m
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.numeral_lt_succ {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {n : β„•} :
      ORingStructure.numeral n < ORingStructure.numeral n + ORingStructure.numeral 1
      source
      theorem LO.FirstOrder.Arithmetic.iff_lt_numeral_exists_numeral {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] {n : β„•} {x : M} :
      x < ORingStructure.numeral n ↔ βˆƒ m < n, x = ORingStructure.numeral m
      source
      instance LO.FirstOrder.Arithmetic.R0.instModelsSetStrucORingSentenceStr {M : Type u_1} [ORingStructure M] [M↓[β„’β‚’α΅£] ⊧* 𝗀] :
      M↓[β„’β‚’α΅£] ⊧* π—₯β‚€
      source
      instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryR0RobinsonQ :
      π—₯β‚€ βͺ― 𝗀
      source
      instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryR0RobinsonQ :
      π—₯β‚€ βͺ± 𝗀