Formalized $\Sigma_1$-Completeness #
def
LO.Arith.Formalized.toNumVec
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(e : Fin n → V)
:
(ℒₒᵣ.codeIn V).SemitermVec (↑n) 0
Equations
- LO.Arith.Formalized.toNumVec e = { val := ⌜fun (i : Fin n) => LO.Arith.Formalized.numeral (e i)⌝, prop := ⋯ }
Instances For
@[simp]
theorem
LO.Arith.Formalized.toNumVec_nil
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
LO.Arith.Formalized.toNumVec ![] = LO.Arith.Language.SemitermVec.nil (ℒₒᵣ.codeIn V) 0
@[simp]
theorem
LO.Arith.Formalized.toNumVec_nth
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(e : Fin n → V)
(i : Fin n)
:
(LO.Arith.Formalized.toNumVec e).nth ↑↑i ⋯ = LO.Arith.Formalized.typedNumeral 0 (e i)
@[simp]
theorem
LO.Arith.Formalized.toNumVec_val_nth
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{n : ℕ}
(e : Fin n → V)
(i : Fin n)
:
LO.Arith.nth (LO.Arith.Formalized.toNumVec e).val ↑↑i = LO.Arith.Formalized.numeral (e i)
@[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 n → V}
{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)]
noncomputable def
LO.Arith.Formalized.TProof.termEqComplete
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(T : ⌜ℒₒᵣ⌝.TTheory)
[LO.Arith.Formalized.R₀Theory T]
{n : ℕ}
(e : Fin n → V)
(t : LO.FirstOrder.Semiterm ℒₒᵣ Empty n)
:
T ⊢ ⌜LO.FirstOrder.Rew.embs t⌝^ᵗ/[LO.Arith.Formalized.toNumVec e].equals
(LO.Arith.Formalized.typedNumeral 0 (LO.FirstOrder.Semiterm.valbm V e t))
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
Instances For
theorem
LO.Arith.Formalized.TProof.termEq_complete!
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(T : ⌜ℒₒᵣ⌝.TTheory)
[LO.Arith.Formalized.R₀Theory T]
{n : ℕ}
(e : Fin n → V)
(t : LO.FirstOrder.Semiterm ℒₒᵣ Empty n)
:
T ⊢! ⌜LO.FirstOrder.Rew.embs t⌝^ᵗ/[LO.Arith.Formalized.toNumVec e].equals
(LO.Arith.Formalized.typedNumeral 0 (LO.FirstOrder.Semiterm.valbm V e t))
theorem
LO.Arith.Formalized.TProof.bold_sigma₁_complete
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(T : ⌜ℒₒᵣ⌝.TTheory)
[LO.Arith.Formalized.R₀Theory T]
{n : ℕ}
{p : LO.FirstOrder.Semisentence ℒₒᵣ n}
(hp : LO.FirstOrder.Arith.Hierarchy 𝚺 1 p)
{e : Fin n → V}
:
theorem
LO.Arith.Formalized.TProof.sigma₁_complete
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(T : ⌜ℒₒᵣ⌝.TTheory)
[LO.Arith.Formalized.R₀Theory T]
{σ : LO.FirstOrder.Sentence ℒₒᵣ}
(hσ : LO.FirstOrder.Arith.Hierarchy 𝚺 1 σ)
:
Hilbert–Bernays provability condition D3
theorem
LO.Arith.sigma₁_complete
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{T : LO.FirstOrder.Theory ℒₒᵣ}
[T.Delta1Definable]
{σ : LO.FirstOrder.Sentence ℒₒᵣ}
(hσ : LO.FirstOrder.Arith.Hierarchy 𝚺 1 σ)
: