On statement of Löb theorem

[iehality]

Löb の定理

Foundation/Foundation/FirstOrder/Incompleteness/Löb.lean

Line 16 in 342c5b3

theorem löb_theorem : T ⊢ (T.standardProvability σ) ➝ σ → T ⊢ σ := ProvabilityAbstraction.löb_theorm (𝔅 := T.standardProvability)

やその周辺について，LO.FirstOrder.Theory.standardProvability は ProvabilityAbstraction の結果を利用するためのラッパーなので，具体的な結果についてはできるだけ LO.FirstOrder.Theory.provable を使うべきだと思う．