Documentation

Incompleteness.Arith.D3

Formalized Σ1-Completeness #

def LO.Arith.Formalized.toNumVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : } (e : Fin nV) :
(ℒₒᵣ.codeIn V).SemitermVec (↑n) 0
Equations
@[simp]
theorem LO.Arith.Formalized.toNumVec_nth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : } (e : Fin nV) (i : Fin n) :
(toNumVec e).nth i = typedNumeral 0 (e i)
@[simp]
theorem LO.Arith.Formalized.toNumVec_val_nth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : } (e : Fin nV) (i : Fin n) :
nth (toNumVec e).val i = numeral (e i)
@[simp]
theorem LO.Arith.Formalized.coe_coe_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : } (i : Fin n) :
i < n

TODO: move

@[simp]
theorem LO.Arith.Formalized.len_semitermvec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k n : V} {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (v : L.SemitermVec k n) :
len v.val = k

Hilbert–Bernays provability condition D3

theorem LO.Arith.sigma₁_complete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {T : FirstOrder.Theory ℒₒᵣ} [T.Delta1Definable] {σ : FirstOrder.Sentence ℒₒᵣ} (hσ : FirstOrder.Arith.Hierarchy 𝚺 1 σ) :
V ⊧ₘ₀ σT.Provableₐ σ