Rosser可証性述語と第2不完全性定理
前提
$ Tは無矛盾な$ \sf PAの再帰的拡大とする．
$ \mathrm{Pr}^\mathrm{Ro}_TはRosser証明可能性述語とする．
詳しくはGödel-Rosserの第1不完全性定理参照．
Prop 1: Rosser証明可能性述語の性質
a. $ T \vdash \varphi \implies T \vdash \mathrm{Pr}^\mathrm{Ro}_T({\ulcorner \varphi \urcorner})
b. $ T \vdash \lnot \varphi \implies T \vdash \lnot\mathrm{Pr}^\mathrm{Ro}_T({\ulcorner \varphi \urcorner})
Def: Rosser証明可能性述語における無矛盾性（Löb無矛盾性）を表す文
$ \mathrm{Con}^\mathrm{Ro}_T \equiv \lnot\mathrm{Pr}^\mathrm{Ro}_T(\ulcorner \overline{0} = \overline{1} \urcorner)
Rosser証明可能性述語によるLöb無矛盾文
Cor 1: Kreiselの注意
$ T \vdash \mathrm{Con}^\mathrm{Ro}_T
証明Prop1.bと$ \mathsf{PA} \vdash \lnot(\overline{0} = \overline{1})より．
すなわち，$ Tの無矛盾性を表す文のとり方によっては，Gödelの第2不完全性定理が成り立たない．
無矛盾性を表す文のとり方について
参考文献
Rosser可証性述語について(外部記事)