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)によって構成されるHilbert-Bernays無矛盾文$ \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無矛盾文からHilbert-Bernays無矛盾文になることに注意．