Supporting results for pointwise provable equality.

Hilbert-Bernays-Löb derivability condition $\mathbf{D3}$ and formalized $\Sigma_1$-completeness

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.eq_comm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {T : ArithmeticTheory} [Theory.Δ₁ T] [𝐏𝐀⁻ ≼ T] {t₁ t₂ : Term V ℒₒᵣ} : Theory.internalize V T ⊢ Semiterm.equals t₁ t₂ → Theory.internalize V T ⊢ Semiterm.equals t₂ t₁

@[reducible, inline]

noncomputable abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.toNumVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n k : ℕ} (w : Fin n → V) : SemitermVec V ℒₒᵣ n k

The to Num Vec construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.term_complete {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐏𝐀⁻ ≼ T] {n : ℕ} (t : ClosedSemiterm ℒₒᵣ n) (w : Fin n → V) : Theory.internalize V T ⊢ (Semiterm.subst (toNumVec w) ⌜t⌝).equals (typedNumeral (Semiterm.valb w t))

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.bold_sigma_one_complete {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐏𝐀⁻ ≼ T] {n : ℕ} {φ : ArithmeticSemisentence n} (hp : Hierarchy Σ 1 φ) {w : Fin n → V} : (Semiformula.Evalb w) φ → Theory.internalize V T ⊢ Semiformula.subst (toNumVec w) ⌜φ⌝

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.sigma_one_provable_of_models {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐏𝐀⁻ ≼ T] {σ : ArithmeticSentence} (hσ : Hierarchy Σ 1 σ) : V↓[ℒₒᵣ] ⊧ σ → Theory.internalize V T ⊢ ⌜σ⌝

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.sigma_one_complete {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐏𝐀⁻ ≼ T] {σ : ArithmeticSentence} (hσ : Hierarchy Σ 1 σ) : V↓[ℒₒᵣ] ⊧ σ → Provable T ⌜σ⌝

Hilbert–Bernays provability condition D3

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.provable_internalize {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝐏𝐀⁻ ≼ T] {σ : ArithmeticSentence} : Provable T ⌜σ⌝ → Provable T ⌜provabilityPred T σ⌝