Jeroslow文
References
R. G. Jeroslow; "Redundancies in the Hilbert–Bernays Derivability Conditions for Gödel's Second Incompleteness Theorem"で考案されたもの
新井敏康『数学基礎論』増補版のp137.Q22に用例がある
Def:
Gödelの不動点補題より構成される次の文$ JをJeroslow文という．
$ \mathsf{PA} \vdash J \leftrightarrow \mathrm{Pr}_T(\ulcorner \lnot J \urcorner)
Thm: Jeroslowの第2不完全性定理
$ \Sigma_1で$ \bf D1,\Sigma_1C/導出可能性条件D1,形式化されたΣ₁完全性定理を満たす$ \mathrm{Pr}_T(x)によってJeroslow文$ Jを構成したとき，
$ T \nvdash \lnot J
$ T \vdash J \to (\mathrm{Pr}_T(\ulcorner J \urcorner) \land \mathrm{Pr}_T(\ulcorner \lnot J \urcorner))