Documentation

Foundation.FirstOrder.Arith.CobhamR0

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