Documentation

Incompleteness.Arith.D3

Formalized $\Sigma_1$-Completeness #

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

    TODO: move

    @[simp]
    theorem LO.Arith.Formalized.len_semitermvec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : V} {n : V} {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (v : L.SemitermVec k n) :
    LO.Arith.len v.val = k
    @[simp]
    theorem LO.Arith.Formalized.cast_substs_numVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : } {e : Fin nV} {x : V} (p : LO.FirstOrder.Semisentence ℒₒᵣ (n + 1)) :
    (LO.FirstOrder.Rew.embs.hom p.cast )^/[(LO.Arith.Formalized.toNumVec e).q.substs (LO.Arith.Formalized.typedNumeral 0 x).sing] = LO.FirstOrder.Rew.embs.hom p^/[LO.Arith.Formalized.toNumVec (x :> e)]