Documentation

Arithmetization.Definability.Absoluteness

theorem LO.FirstOrder.Arith.Defined.shigmaZero_absolute (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {R : (Fin k)Prop} {R' : (Fin kV)Prop} {p : 𝚺₀.Semisentence k} (hR : LO.FirstOrder.Arith.HierarchySymbol.Defined R p) (hR' : LO.FirstOrder.Arith.HierarchySymbol.Defined R' p) (v : Fin k) :
R v R' fun (i : Fin k) => (v i)
theorem LO.FirstOrder.Arith.DefinedFunction.shigmaZero_absolute_func (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {f : (Fin k)} {f' : (Fin kV)V} {p : 𝚺₀.Semisentence (k + 1)} (hf : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f p) (hf' : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f' p) (v : Fin k) :
(f v) = f' fun (i : Fin k) => (v i)
theorem LO.FirstOrder.Arith.Defined.shigmaOne_absolute (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {R : (Fin k)Prop} {R' : (Fin kV)Prop} {p : 𝚫₁.Semisentence k} (hR : LO.FirstOrder.Arith.HierarchySymbol.Defined R p) (hR' : LO.FirstOrder.Arith.HierarchySymbol.Defined R' p) (v : Fin k) :
R v R' fun (i : Fin k) => (v i)
theorem LO.FirstOrder.Arith.DefinedFunction.shigmaOne_absolute_func (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {f : (Fin k)} {f' : (Fin kV)V} {p : 𝚺₁.Semisentence (k + 1)} (hf : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f p) (hf' : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f' p) (v : Fin k) :
(f v) = f' fun (i : Fin k) => (v i)
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} :
(V ⊧/fun (x : Fin n) => (e x)) σ ⊧/e σ
Equations
  • LO.FirstOrder.Arith.instSubtheorySyntacticFormulaORingTheoryCobhamR0_arithmetization = inferInstance.comp inferInstance