Documentation

LeanPool.Incompleteness.Foundation.FirstOrder.Arith.CobhamR0

CobhamR0 #

source
theorem LO.Arith.numeral_add_numeral {M : Type u_1} [ORingStruc M] [M βŠ§β‚˜* 𝐑₀] (n m : β„•) :
ORingStruc.numeral n + ORingStruc.numeral m = ORingStruc.numeral (n + m)
source
theorem LO.Arith.numeral_mul_numeral {M : Type u_1} [ORingStruc M] [M βŠ§β‚˜* 𝐑₀] (n m : β„•) :
ORingStruc.numeral n * ORingStruc.numeral m = ORingStruc.numeral (n * m)
source
theorem LO.Arith.numeral_ne_numeral_of_ne {M : Type u_1} [ORingStruc M] [M βŠ§β‚˜* 𝐑₀] {n m : β„•} (h : n β‰  m) :
ORingStruc.numeral n β‰  ORingStruc.numeral m
source
theorem LO.Arith.lt_numeral_iff {M : Type u_1} [ORingStruc M] [M βŠ§β‚˜* 𝐑₀] {x : M} {n : β„•} :
x < ORingStruc.numeral n ↔ βˆƒ (i : Fin n), x = ORingStruc.numeral ↑i
source
@[simp]
theorem LO.Arith.numeral_inj_iff {M : Type u_1} [ORingStruc M] [M βŠ§β‚˜* 𝐑₀] {n m : β„•} :
ORingStruc.numeral n = ORingStruc.numeral m ↔ n = m
source
@[simp]
theorem LO.Arith.numeral_lt_numeral_iff {M : Type u_1} [ORingStruc M] [M βŠ§β‚˜* 𝐑₀] {n m : β„•} :
ORingStruc.numeral n < ORingStruc.numeral m ↔ n < m
source
theorem LO.Arith.val_numeral {M : Type u_1} [ORingStruc M] [M βŠ§β‚˜* 𝐑₀] {ΞΎ : Type u_2} {n : β„•} (t : FirstOrder.Semiterm β„’β‚’α΅£ ΞΎ n) (v : Fin n β†’ β„•) (f : ΞΎ β†’ β„•) :
FirstOrder.Semiterm.valm M (fun (x : Fin n) => ORingStruc.numeral (v x)) (fun (x : ΞΎ) => ORingStruc.numeral (f x)) t = ORingStruc.numeral (FirstOrder.Semiterm.valm β„• v f t)
source
theorem LO.Arith.bold_sigma_one_completeness {M : Type u_1} [ORingStruc M] [M βŠ§β‚˜* 𝐑₀] {ΞΎ : Type u_2} {n : β„•} {Ο† : FirstOrder.Semiformula β„’β‚’α΅£ ΞΎ n} (hp : FirstOrder.Arith.Hierarchy Sg 1 Ο†) {e : Fin n β†’ β„•} {f : ΞΎ β†’ β„•} :
(FirstOrder.Semiformula.Evalm β„• e f) Ο† β†’ (FirstOrder.Semiformula.Evalm M (fun (x : Fin n) => ORingStruc.numeral (e x)) fun (x : ΞΎ) => ORingStruc.numeral (f x)) Ο†
source
theorem LO.Arith.sigma_one_completeness {M : Type u_1} [ORingStruc M] [M βŠ§β‚˜* 𝐑₀] {Οƒ : FirstOrder.Sentence β„’β‚’α΅£} (hΟƒ : FirstOrder.Arith.Hierarchy Sg 1 Οƒ) :
β„• βŠ§β‚˜β‚€ Οƒ β†’ M βŠ§β‚˜β‚€ Οƒ
source
theorem LO.FirstOrder.Arith.sigma_one_completeness {T : Theory β„’β‚’α΅£} [𝐑₀ wkn T] {Οƒ : Sentence β„’β‚’α΅£} (hΟƒ : Hierarchy Sg 1 Οƒ) :
β„• βŠ§β‚˜β‚€ Οƒ β†’ T ⊒! ↑σ
source
theorem LO.FirstOrder.Arith.sigma_one_completeness_iff {T : Theory β„’β‚’α΅£} [𝐑₀ wkn T] [ss : Sigma1Sound T] {Οƒ : Sentence β„’β‚’α΅£} (hΟƒ : Hierarchy Sg 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.Arith.Countermodel.OmegaAddOne :
Type

Imported declaration from the Incompleteness formalization.

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

    Imported declaration from the Incompleteness formalization.

    Equations
    Instances For
      source
      instance LO.FirstOrder.Arith.Countermodel.OmegaAddOne.instModelsTheoryCobhamR0 :
      OmegaAddOne βŠ§β‚˜* 𝐑₀
      source
      theorem LO.FirstOrder.Arith.Rβ‚€_unprovable_add_zero :
      𝐑₀ ⊬ (β€œ(!!(Semiterm.fvar 0) + !!↑0) = !!(Semiterm.fvar 0)”)