標準的な証明可能性述語
導出可能性条件
(あるいはもっと具体的に
Hilber-Bernays-Löbの導出可能性条件
$ \bf D1,D2,D3
)を満たす
証明可能性述語
のこと.
標準的な証明可能性述語
を構成できる
第1不完全性定理
が成り立つ体系では
Gödelの第2不完全性定理
が成立する.
証明はこの可証性述語が
Löb無矛盾文
と体系内で同値であることを示して
第1不完全性定理
から系として導かれる.