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可証性述語について(外部記事)