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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.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 LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.toNumVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {n k : ℕ} (w : Fin n → V) : SemitermVec V ℒₒᵣ n k

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.toNumVec w = (fun (x : V) => LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.typedNumeral x)⨟ w

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.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 LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.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 LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.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 LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.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 LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.provable_internalize {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] {σ : ArithmeticSentence} : Provable T ⌜σ⌝ → Provable T ⌜provabilityPred T σ⌝