Formalized $\Sigma_1$-Completeness

noncomputable def LO.Arith.Formalized.toNumVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (e : Fin n → V) : (ℒₒᵣ.codeIn V).SemitermVec (↑n) 0

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.Formalized.toNumVec e = { val := ⌜fun (i : Fin n) => LO.Arith.Formalized.numeral (e i)⌝, prop := ⋯ }

@[simp]

theorem LO.Arith.Formalized.toNumVec_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : toNumVec ![] = Language.SemitermVec.nil (ℒₒᵣ.codeIn V) 0

@[simp]

theorem LO.Arith.Formalized.toNumVec_nth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} (e : Fin n → V) (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 ⊧ₘ* 𝐈Sg1] {n : ℕ} (e : Fin n → V) (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 ⊧ₘ* 𝐈Sg1] {n : ℕ} (i : Fin n) : ↑↑i < ↑n

TODO: move

@[simp]

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

@[simp]

theorem LO.Arith.Formalized.cast_substs_numVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : ℕ} {e : Fin n → V} {x : V} (φ : FirstOrder.Semisentence ℒₒᵣ (n + 1)) : (⌜(FirstOrder.Rewriting.app FirstOrder.Rew.embs) φ⌝.cast ⋯)^/[(toNumVec e).q.substs (typedNumeral 0 x).sing] = ⌜(FirstOrder.Rewriting.app FirstOrder.Rew.embs) φ⌝^/[toNumVec (x :> e)]

noncomputable def LO.Arith.Formalized.TProof.termEqComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n : ℕ} (e : Fin n → V) (t : FirstOrder.Semiterm ℒₒᵣ Empty n) : T ⊢ ⌜FirstOrder.Rew.embs t⌝^ᵗ/[toNumVec e].equals (typedNumeral 0 (FirstOrder.Semiterm.valbm V e t))

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.Arith.Formalized.TProof.termEqComplete T e (LO.FirstOrder.Semiterm.bvar z) = ⋯.mpr (LO.Arith.Formalized.TProof.eqRefl T (LO.Arith.Formalized.typedNumeral 0 (e z)))
• LO.Arith.Formalized.TProof.termEqComplete T e (LO.FirstOrder.Semiterm.fvar x_1) = x_1.elim

theorem LO.Arith.Formalized.TProof.termEq_complete! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n : ℕ} (e : Fin n → V) (t : FirstOrder.Semiterm ℒₒᵣ Empty n) : T ⊢! ⌜FirstOrder.Rew.embs t⌝^ᵗ/[toNumVec e].equals (typedNumeral 0 (FirstOrder.Semiterm.valbm V e t))

theorem LO.Arith.Formalized.TProof.bold_sigma₁_complete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n : ℕ} {φ : FirstOrder.Semisentence ℒₒᵣ n} (hp : FirstOrder.Arith.Hierarchy Sg 1 φ) {e : Fin n → V} : V ⊧/e φ → T ⊢! ⌜(FirstOrder.Rewriting.app FirstOrder.Rew.embs) φ⌝^/[toNumVec e]

theorem LO.Arith.Formalized.TProof.sigma₁_complete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {σ : FirstOrder.Sentence ℒₒᵣ} (hσ : FirstOrder.Arith.Hierarchy Sg 1 σ) : V ⊧ₘ₀ σ → T ⊢! ⌜σ⌝

Hilbert–Bernays provability condition D3

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