Rosser証明可能性述語
性質
証明可能性述語
だが,
導出可能性条件
D1,D2,D3のうち
D1は満たす.
D2かD3のどちらかは少なくとも満たさない
両方満たしていたら
Rosser証明可能性述語
で
Gödelの第2不完全性定理
が成り立つはずだが
実際には成り立たない.
Kreiselの注意
.
Rosser可証性述語と第2不完全性定理
参照.
Thm:
D. Guaspari, Robert M. Solovay, "Rosser sentences"
D2とD3の両方が成立しない
$ T
の
Rosser証明可能性述語
が存在する.
Thm:
T. Arai; "Derivability conditions on Rosser's provability predicates"
D2が成立する
$ T
の
Rosser証明可能性述語
,及び,D3が成立する
$ T
の
Rosser証明可能性述語
が存在する.
注意
$ T
の
Rosser証明可能性述語
の否定
$ \lnot\mathrm{Pr}^R_T(x)
を
Gödelの不動点補題
に適用して存在が保証される文
$ \rho
を
Rosser文
という.
$ T \vdash \rho \leftrightarrow \lnot\mathrm{Pr}^R_T(\overline{\ulcorner \rho \urcorner})
Rosser文
は
$ T
が無矛盾なら証明も反証も出来ない.
Gödel-Rosserの第1不完全性定理
.
参考文献
D. Guaspari, Robert M. Solovay, "Rosser sentences"
T. Arai; "Derivability conditions on Rosser's provability predicates"
Rosser可証性述語について(外部記事)