theorem FFL.FirstOrder.Arithmetic.nat_modelsWithParam_iff_models_substs {k : ℕ} {v : Fin k → ℕ} {φ : ArithmeticSemisentence k} : (Semiformula.Evalb v) φ ↔ ℕ↓[ℒₒᵣ] ⊧ φ ⇜ fun (i : Fin k) => ↑(Semiterm.Operator.numeral ℒₒᵣ (v i))

theorem FFL.FirstOrder.Arithmetic.modelsWithParam_iff_models_substs (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} {v : Fin k → ℕ} {φ : ArithmeticSemisentence k} : (Semiformula.Evalb (Nat.cast ∘ v)) φ ↔ V↓[ℒₒᵣ] ⊧ φ ⇜ fun (i : Fin k) => ↑(Semiterm.Operator.numeral ℒₒᵣ (v i))

theorem FFL.FirstOrder.Arithmetic.shigmaZero_absolute (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (φ : 𝚺₀.Semisentence k) (v : Fin k → ℕ) : (Semiformula.Evalb v) ↑φ ↔ (Semiformula.Evalb (Nat.cast ∘ v)) ↑φ

theorem FFL.FirstOrder.Arithmetic.Defined.shigmaZero_absolute (V : Type u_1) [ORingStructure 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' (Nat.cast ∘ v)

theorem FFL.FirstOrder.Arithmetic.DefinedFunction.shigmaZero_absolute_func (V : Type u_1) [ORingStructure 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' (Nat.cast ∘ v)

theorem FFL.FirstOrder.Arithmetic.sigmaOne_upward_absolute (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (φ : 𝚺₁.Semisentence k) (v : Fin k → ℕ) : (Semiformula.Evalb v) ↑φ → (Semiformula.Evalb (Nat.cast ∘ v)) ↑φ

theorem FFL.FirstOrder.Arithmetic.piOne_downward_absolute (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (φ : 𝚷₁.Semisentence k) (v : Fin k → ℕ) : (Semiformula.Evalb (Nat.cast ∘ v)) ↑φ → (Semiformula.Evalb v) ↑φ

theorem FFL.FirstOrder.Arithmetic.deltaOne_absolute (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k : ℕ} (φ : 𝚫₁.Semisentence k) (properNat : HierarchySymbol.Semiformula.ProperOn ℕ φ) (proper : HierarchySymbol.Semiformula.ProperOn V φ) (v : Fin k → ℕ) : (Semiformula.Evalb v) ↑φ ↔ (Semiformula.Evalb (Nat.cast ∘ v)) ↑φ

theorem FFL.FirstOrder.Arithmetic.Defined.shigmaOne_absolute (V : Type u_1) [ORingStructure 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' (Nat.cast ∘ v)

theorem FFL.FirstOrder.Arithmetic.DefinedFunction.shigmaOne_absolute_func (V : Type u_1) [ORingStructure 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' (Nat.cast ∘ v)

theorem FFL.FirstOrder.Arithmetic.models_iff_of_Sigma0 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {n : ℕ} {σ : ArithmeticSemisentence n} (hσ : Hierarchy 𝚺 0 σ) {e : Fin n → ℕ} : (Semiformula.Evalb (Nat.cast ∘ e)) σ ↔ (Semiformula.Evalb e) σ

theorem FFL.FirstOrder.Arithmetic.models_iff_of_Delta1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {n : ℕ} {σ : 𝚫₁.Semisentence n} (hσ : HierarchySymbol.Semiformula.ProperOn ℕ σ) (hσV : HierarchySymbol.Semiformula.ProperOn V σ) {e : Fin n → ℕ} : (Semiformula.Evalb (Nat.cast ∘ e)) ↑σ ↔ (Semiformula.Evalb e) ↑σ

instance FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryR0 {T : ArithmeticTheory} [𝗣𝗔⁻ ⪯ T] : 𝗥₀ ⪯ T

theorem FFL.FirstOrder.Arithmetic.sigma_one_completeness_iff_param {T : ArithmeticTheory} [𝗣𝗔⁻ ⪯ T] [T.SoundOnHierarchy 𝚺 1] {n : ℕ} {σ : ArithmeticSemisentence n} (hσ : Hierarchy 𝚺 1 σ) {e : Fin n → ℕ} : (Semiformula.Evalb e) σ ↔ T ⊢ σ ⇜ fun (x : Fin n) => ↑(Semiterm.Operator.numeral ℒₒᵣ (e x))

theorem FFL.FirstOrder.Arithmetic.models_iff_provable_of_Sigma0_param {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {T : ArithmeticTheory} [𝗣𝗔⁻ ⪯ T] [T.SoundOnHierarchy 𝚺 1] {n : ℕ} [V↓[ℒₒᵣ] ⊧* T] {σ : ArithmeticSemisentence n} (hσ : Hierarchy 𝚺 0 σ) {e : Fin n → ℕ} : (Semiformula.Evalb (Nat.cast ∘ e)) σ ↔ T ⊢ σ ⇜ fun (x : Fin n) => ↑(Semiterm.Operator.numeral ℒₒᵣ (e x))

theorem FFL.FirstOrder.Arithmetic.models_iff_provable_of_Delta1_param {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {T : ArithmeticTheory} [𝗣𝗔⁻ ⪯ T] [T.SoundOnHierarchy 𝚺 1] {n : ℕ} [V↓[ℒₒᵣ] ⊧* T] {σ : 𝚫₁.Semisentence n} (hσ : HierarchySymbol.Semiformula.ProperOn ℕ σ) (hσV : HierarchySymbol.Semiformula.ProperOn V σ) {e : Fin n → ℕ} : (Semiformula.Evalb (Nat.cast ∘ e)) ↑σ ↔ T ⊢ ↑σ ⇜ fun (x : Fin n) => ↑(Semiterm.Operator.numeral ℒₒᵣ (e x))