Supporting results for pointwise provable equality.

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

theorem PointwiseComposition.FFL.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 : LK2.Derivation T Γ) : Derivable T ⌜Γ⌝

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.Provable.complete {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Sentence L} : Theory.internalize ℕ T ⊢ ⌜φ⌝ ↔ T ⊢ φ

@[simp]

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