Supporting results for pointwise provable equality.

Prenex normal form theorem over $\mathsf{I\Sigma_1}$

Every Hierarchy Σ 1 formula is 𝐈Σ₁-provably equivalent to a formula of the form ∃¹ θ with θ in Hierarchy Σ 0, and dually for Hierarchy Π 1 and ∀¹ θ.

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.ISigma1.hasPrenex {n : ℕ} {φ : ArithmeticSemisentence n} (h : Hierarchy Σ 1 φ) : ∃ (φ' : Prenex Σ 1 Empty n), 𝐈Σ₁ ⊢ ∀¹* (φ ⇔ₗ ↑φ')

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.ISigma1.exists_matrix_provable {n : ℕ} {φ : ArithmeticSemisentence n} (h : Hierarchy Σ 1 φ) : ∃ (θ : Σ₀.Semisentence (n + 1)), 𝐈Σ₁ ⊢ ∀¹* (φ ⇔ₗ ∃¹ ↑θ)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.ISigma1.exists_matrix_provable_pi {n : ℕ} {φ : ArithmeticSemisentence n} (h : Hierarchy Π 1 φ) : ∃ (θ : Σ₀.Semisentence (n + 1)), 𝐈Σ₁ ⊢ ∀¹* (φ ⇔ₗ ∀¹ ↑θ)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.ISigma1.exists_matrix_provable_of_sentence {σ : ArithmeticSentence} (h : Hierarchy Σ 1 σ) : ∃ (θ : Σ₀.Semisentence 1), 𝐈Σ₁ ⊢ σ ⇔ₗ ∃¹ ↑θ