Jeroslowの第2不完全性定理
References
R. G. Jeroslow; "Redundancies in the Hilbert–Bernays Derivability Conditions for Gödel's Second Incompleteness Theorem"
T. Kurahashi; "第2不完全性定理について"
Thm
$ \bf D1, \Sigma_1Cを満たす証明可能性述語$ \mathrm{Pr}_T(x)によって構成される形式化された無矛盾律$ \mathrm{Con}^\mathrm{HB}_{\mathrm{Pr}_T} \equiv \forall_x\lbrack \mathrm{Fml}(x) \land (\mathrm{Pr}_T(x) \to \lnot\mathrm{Pr}_T(\dot{\lnot}x)) \rbrackについて，$ T \nvdash \mathrm{Con}^\mathrm{HB}_{\mathrm{Pr}_T}
remark:
Löbの第2不完全性定理で$ \bf D3を$ \bf \Sigma_1Cに強めると$ \bf D2が不要になる．
ただし，無矛盾性を表す文はLöb無矛盾文から形式化された無矛盾律になることに注意．