Supporting results for pointwise provable equality.

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryR0 {T : ArithmeticTheory} [𝐏𝐀⁻ ≼ T] : 𝐑₀ ≼ T

theorem PointwiseComposition.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.models_iff_provable_of_Sigma0_param {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {T : ArithmeticTheory} [𝐏𝐀⁻ ≼ T] [T.SoundOnHierarchy Σ 1] {n : ℕ} {σ : ArithmeticSemisentence n} (hσ : Hierarchy Σ 0 σ) {e : Fin n → ℕ} : (Semiformula.Evalb (Nat.cast ∘ e)) σ ↔ T ⊢ σ ↜ fun (x : Fin n) => ↑(Semiterm.Operator.numeral ℒₒᵣ (e x))

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.models_iff_provable_of_Delta1_param {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {T : ArithmeticTheory} [𝐏𝐀⁻ ≼ T] [T.SoundOnHierarchy Σ 1] {n : ℕ} {σ : ∆₁.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))