Documentation

Foundation.FirstOrder.Arith.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 𝚺 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 𝚺 1 Οƒ) :
β„• βŠ§β‚˜β‚€ Οƒ β†’ M βŠ§β‚˜β‚€ Οƒ
source
theorem LO.FirstOrder.Arith.sigma_one_completeness {T : Theory β„’β‚’α΅£} [𝐑₀ β‰Ό T] {Οƒ : Sentence β„’β‚’α΅£} (hΟƒ : Hierarchy 𝚺 1 Οƒ) :
β„• βŠ§β‚˜β‚€ Οƒ β†’ T ⊒! ↑σ
source
theorem LO.FirstOrder.Arith.sigma_one_completeness_iff {T : Theory β„’β‚’α΅£} [𝐑₀ β‰Ό T] [ss : Sigma1Sound T] {Οƒ : Sentence β„’β‚’α΅£} (hΟƒ : Hierarchy 𝚺 1 Οƒ) :
β„• βŠ§β‚˜β‚€ Οƒ ↔ T ⊒! ↑σ