Löb's Theorem

theorem LO.FirstOrder.Arithmetic.löb_theorem {T : ArithmeticTheory} [Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] {σ : ArithmeticSentence} : T ⊢ Bootstrapping.provabilityPred T σ 🡒 σ → T ⊢ σ

theorem LO.FirstOrder.Arithmetic.formalized_löb_theorem {T : ArithmeticTheory} [Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] {σ : ArithmeticSentence} : 𝗜𝚺₁ ⊢ Bootstrapping.provabilityPred T (Bootstrapping.provabilityPred T σ 🡒 σ) 🡒 Bootstrapping.provabilityPred T σ