theorem
LO.FirstOrder.Arith.nat_modelsWithParam_iff_models_substs
{k : ℕ}
{v : Fin k → ℕ}
{p : LO.FirstOrder.Semisentence ℒₒᵣ k}
:
ℕ ⊧/v p ↔ ℕ ⊧ₘ₀ (LO.FirstOrder.Rew.substs fun (i : Fin k) =>
LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ (v i))).hom
p
theorem
LO.FirstOrder.Arith.modelsWithParam_iff_models_substs
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{v : Fin k → ℕ}
{p : LO.FirstOrder.Semisentence ℒₒᵣ k}
:
(V ⊧/fun (x : Fin k) => ↑(v x)) p ↔ V ⊧ₘ₀ (LO.FirstOrder.Rew.substs fun (i : Fin k) =>
LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ (v i))).hom
p
theorem
LO.FirstOrder.Arith.shigmaZero_absolute
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(p : 𝚺₀.Semisentence k)
(v : Fin k → ℕ)
:
ℕ ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val p) ↔ (V ⊧/fun (x : Fin k) => ↑(v x)) (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val p)
theorem
LO.FirstOrder.Arith.Defined.shigmaZero_absolute
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{R : (Fin k → ℕ) → Prop}
{R' : (Fin k → V) → Prop}
{p : 𝚺₀.Semisentence k}
(hR : LO.FirstOrder.Arith.HierarchySymbol.Defined R p)
(hR' : LO.FirstOrder.Arith.HierarchySymbol.Defined R' p)
(v : Fin k → ℕ)
:
theorem
LO.FirstOrder.Arith.DefinedFunction.shigmaZero_absolute_func
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{f : (Fin k → ℕ) → ℕ}
{f' : (Fin k → V) → V}
{p : 𝚺₀.Semisentence (k + 1)}
(hf : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f p)
(hf' : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f' p)
(v : Fin k → ℕ)
:
theorem
LO.FirstOrder.Arith.sigmaOne_upward_absolute
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(p : 𝚺₁.Semisentence k)
(v : Fin k → ℕ)
:
ℕ ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val p) →
(V ⊧/fun (x : Fin k) => ↑(v x)) (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val p)
theorem
LO.FirstOrder.Arith.piOne_downward_absolute
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(p : 𝚷₁.Semisentence k)
(v : Fin k → ℕ)
:
(V ⊧/fun (x : Fin k) => ↑(v x)) (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val p) →
ℕ ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val p)
theorem
LO.FirstOrder.Arith.deltaOne_absolute
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(p : 𝚫₁.Semisentence k)
(properNat : LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn ℕ p)
(proper : LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn V p)
(v : Fin k → ℕ)
:
ℕ ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val p) ↔ (V ⊧/fun (x : Fin k) => ↑(v x)) (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val p)
theorem
LO.FirstOrder.Arith.Defined.shigmaOne_absolute
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{R : (Fin k → ℕ) → Prop}
{R' : (Fin k → V) → Prop}
{p : 𝚫₁.Semisentence k}
(hR : LO.FirstOrder.Arith.HierarchySymbol.Defined R p)
(hR' : LO.FirstOrder.Arith.HierarchySymbol.Defined R' p)
(v : Fin k → ℕ)
:
theorem
LO.FirstOrder.Arith.DefinedFunction.shigmaOne_absolute_func
(V : Type u_1)
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{f : (Fin k → ℕ) → ℕ}
{f' : (Fin k → V) → V}
{p : 𝚺₁.Semisentence (k + 1)}
(hf : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f p)
(hf' : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f' p)
(v : Fin k → ℕ)
:
theorem
LO.FirstOrder.Arith.models_iff_of_Sigma0
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{n : ℕ}
{σ : LO.FirstOrder.Semisentence ℒₒᵣ n}
(hσ : LO.FirstOrder.Arith.Hierarchy 𝚺 0 σ)
{e : Fin n → ℕ}
:
theorem
LO.FirstOrder.Arith.models_iff_of_Delta1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{n : ℕ}
{σ : 𝚫₁.Semisentence n}
(hσ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn ℕ σ)
(hσV : LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn V σ)
{e : Fin n → ℕ}
:
(V ⊧/fun (x : Fin n) => ↑(e x)) (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val σ) ↔ ℕ ⊧/e (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val σ)
noncomputable instance
LO.FirstOrder.Arith.instSubtheorySyntacticFormulaORingTheoryCobhamR0_arithmetization
{T : LO.FirstOrder.Theory ℒₒᵣ}
[𝐏𝐀⁻ ≼ T]
:
Equations
- LO.FirstOrder.Arith.instSubtheorySyntacticFormulaORingTheoryCobhamR0_arithmetization = inferInstance.comp inferInstance
theorem
LO.FirstOrder.Arith.sigma_one_completeness_iff_param
{T : LO.FirstOrder.Theory ℒₒᵣ}
[𝐏𝐀⁻ ≼ T]
[LO.FirstOrder.Arith.Sigma1Sound T]
{n : ℕ}
{σ : LO.FirstOrder.Semisentence ℒₒᵣ n}
(hσ : LO.FirstOrder.Arith.Hierarchy 𝚺 1 σ)
{e : Fin n → ℕ}
:
ℕ ⊧/e σ ↔ T ⊢!. (LO.FirstOrder.Rew.substs fun (x : Fin n) =>
LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ (e x))).hom
σ
theorem
LO.FirstOrder.Arith.models_iff_provable_of_Sigma0_param
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{T : LO.FirstOrder.Theory ℒₒᵣ}
[𝐏𝐀⁻ ≼ T]
[LO.FirstOrder.Arith.Sigma1Sound T]
{n : ℕ}
[V ⊧ₘ* T]
{σ : LO.FirstOrder.Semisentence ℒₒᵣ n}
(hσ : LO.FirstOrder.Arith.Hierarchy 𝚺 0 σ)
{e : Fin n → ℕ}
:
(V ⊧/fun (x : Fin n) => ↑(e x)) σ ↔ T ⊢!. (LO.FirstOrder.Rew.substs fun (x : Fin n) =>
LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ (e x))).hom
σ
theorem
LO.FirstOrder.Arith.models_iff_provable_of_Delta1_param
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{T : LO.FirstOrder.Theory ℒₒᵣ}
[𝐏𝐀⁻ ≼ T]
[LO.FirstOrder.Arith.Sigma1Sound T]
{n : ℕ}
[V ⊧ₘ* T]
{σ : 𝚫₁.Semisentence n}
(hσ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn ℕ σ)
(hσV : LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn V σ)
{e : Fin n → ℕ}
:
(V ⊧/fun (x : Fin n) => ↑(e x)) (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val σ) ↔ T ⊢!. (LO.FirstOrder.Rew.substs fun (x : Fin n) =>
LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ (e x))).hom
(LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val σ)