Hilbert-Bernays-Löb derivability condition $\mathbf{D1}$ and soundness of internal provability.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.derivable_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : Finset (Proposition L)} (d : Derivation2 T Γ) : Derivable T ⌜Γ⌝

theorem LO.FirstOrder.Arithmetic.Bootstrapping.internalize_provability {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} : T ⊢ φ → Provable T ⌜φ⌝

Hilbert–Bernays provability condition D1

theorem LO.FirstOrder.Arithmetic.Bootstrapping.internal_provable_of_outer_provable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} : T ⊢ φ → Theory.internalize V T ⊢ ⌜φ⌝

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Provable.complete {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} : Theory.internalize ℕ T ⊢ ⌜φ⌝ ↔ T ⊢ φ

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.provable_iff_provable {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} : Provable T ⌜φ⌝ ↔ T ⊢ φ