theorem LO.FirstOrder.Arith.nat_modelsWithParam_iff_models_substs {k : ℕ} {v : Fin k → ℕ} {φ : Semisentence ℒₒᵣ k} : ℕ ⊧/v φ ↔ ℕ ⊧ₘ₀ φ ⇜ fun (i : Fin k) => ↑(Semiterm.Operator.numeral ℒₒᵣ (v i))

theorem LO.FirstOrder.Arith.modelsWithParam_iff_models_substs (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} {v : Fin k → ℕ} {φ : Semisentence ℒₒᵣ k} : (V ⊧/fun (x : Fin k) => ↑(v x)) φ ↔ V ⊧ₘ₀ φ ⇜ fun (i : Fin k) => ↑(Semiterm.Operator.numeral ℒₒᵣ (v i))

theorem LO.FirstOrder.Arith.shigmaZero_absolute (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (φ : 𝚺₀.Semisentence k) (v : Fin k → ℕ) : ℕ ⊧/v (HierarchySymbol.Semiformula.val φ) ↔ (V ⊧/fun (x : Fin k) => ↑(v x)) (HierarchySymbol.Semiformula.val φ)

theorem LO.FirstOrder.Arith.Defined.shigmaZero_absolute (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} {R : (Fin k → ℕ) → Prop} {R' : (Fin k → V) → Prop} {φ : 𝚺₀.Semisentence k} (hR : HierarchySymbol.Defined R φ) (hR' : HierarchySymbol.Defined R' φ) (v : Fin k → ℕ) : R v ↔ R' fun (i : Fin k) => ↑(v i)

theorem LO.FirstOrder.Arith.DefinedFunction.shigmaZero_absolute_func (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₀.Semisentence (k + 1)} (hf : HierarchySymbol.DefinedFunction f φ) (hf' : HierarchySymbol.DefinedFunction f' φ) (v : Fin k → ℕ) : ↑(f v) = f' fun (i : Fin k) => ↑(v i)

theorem LO.FirstOrder.Arith.sigmaOne_upward_absolute (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (φ : 𝚺₁.Semisentence k) (v : Fin k → ℕ) : ℕ ⊧/v (HierarchySymbol.Semiformula.val φ) → (V ⊧/fun (x : Fin k) => ↑(v x)) (HierarchySymbol.Semiformula.val φ)

theorem LO.FirstOrder.Arith.piOne_downward_absolute (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (φ : 𝚷₁.Semisentence k) (v : Fin k → ℕ) : (V ⊧/fun (x : Fin k) => ↑(v x)) (HierarchySymbol.Semiformula.val φ) → ℕ ⊧/v (HierarchySymbol.Semiformula.val φ)

theorem LO.FirstOrder.Arith.deltaOne_absolute (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} (φ : 𝚫₁.Semisentence k) (properNat : HierarchySymbol.Semiformula.ProperOn ℕ φ) (proper : HierarchySymbol.Semiformula.ProperOn V φ) (v : Fin k → ℕ) : ℕ ⊧/v (HierarchySymbol.Semiformula.val φ) ↔ (V ⊧/fun (x : Fin k) => ↑(v x)) (HierarchySymbol.Semiformula.val φ)

theorem LO.FirstOrder.Arith.Defined.shigmaOne_absolute (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} {R : (Fin k → ℕ) → Prop} {R' : (Fin k → V) → Prop} {φ : 𝚫₁.Semisentence k} (hR : HierarchySymbol.Defined R φ) (hR' : HierarchySymbol.Defined R' φ) (v : Fin k → ℕ) : R v ↔ R' fun (i : Fin k) => ↑(v i)

theorem LO.FirstOrder.Arith.DefinedFunction.shigmaOne_absolute_func (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₁.Semisentence (k + 1)} (hf : HierarchySymbol.DefinedFunction f φ) (hf' : HierarchySymbol.DefinedFunction f' φ) (v : Fin k → ℕ) : ↑(f v) = f' fun (i : Fin k) => ↑(v i)

theorem LO.FirstOrder.Arith.models_iff_of_Sigma0 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {n : ℕ} {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 0 σ) {e : Fin n → ℕ} : (V ⊧/fun (x : Fin n) => ↑(e x)) σ ↔ ℕ ⊧/e σ

theorem LO.FirstOrder.Arith.models_iff_of_Delta1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {n : ℕ} {σ : 𝚫₁.Semisentence n} (hσ : HierarchySymbol.Semiformula.ProperOn ℕ σ) (hσV : HierarchySymbol.Semiformula.ProperOn V σ) {e : Fin n → ℕ} : (V ⊧/fun (x : Fin n) => ↑(e x)) (HierarchySymbol.Semiformula.val σ) ↔ ℕ ⊧/e (HierarchySymbol.Semiformula.val σ)

noncomputable instance LO.FirstOrder.Arith.instSubtheorySyntacticFormulaORingTheoryCobhamR0_arithmetization {T : Theory ℒₒᵣ} [𝐏𝐀⁻ ≼ T] : 𝐑₀ ≼ T

Equations

• LO.FirstOrder.Arith.instSubtheorySyntacticFormulaORingTheoryCobhamR0_arithmetization = inferInstance.comp inferInstance

theorem LO.FirstOrder.Arith.sigma_one_completeness_iff_param {T : Theory ℒₒᵣ} [𝐏𝐀⁻ ≼ T] [Sigma1Sound T] {n : ℕ} {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 1 σ) {e : Fin n → ℕ} : ℕ ⊧/e σ ↔ T ⊢!. σ ⇜ fun (x : Fin n) => ↑(Semiterm.Operator.numeral ℒₒᵣ (e x))

theorem LO.FirstOrder.Arith.models_iff_provable_of_Sigma0_param {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {T : Theory ℒₒᵣ} [𝐏𝐀⁻ ≼ T] [Sigma1Sound T] {n : ℕ} [V ⊧ₘ* T] {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 0 σ) {e : Fin n → ℕ} : (V ⊧/fun (x : Fin n) => ↑(e x)) σ ↔ T ⊢!. σ ⇜ fun (x : Fin n) => ↑(Semiterm.Operator.numeral ℒₒᵣ (e x))

theorem LO.FirstOrder.Arith.models_iff_provable_of_Delta1_param {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {T : Theory ℒₒᵣ} [𝐏𝐀⁻ ≼ T] [Sigma1Sound T] {n : ℕ} [V ⊧ₘ* T] {σ : 𝚫₁.Semisentence n} (hσ : HierarchySymbol.Semiformula.ProperOn ℕ σ) (hσV : HierarchySymbol.Semiformula.ProperOn V σ) {e : Fin n → ℕ} : (V ⊧/fun (x : Fin n) => ↑(e x)) (HierarchySymbol.Semiformula.val σ) ↔ T ⊢!. HierarchySymbol.Semiformula.val σ ⇜ fun (x : Fin n) => ↑(Semiterm.Operator.numeral ℒₒᵣ (e x))