Rosser可証性述語と第2不完全性定理
前提
$ Tは無矛盾な$ \sf PAの再帰的拡大とする.
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})
$ \mathrm{Con}^\mathrm{Ro}_T \equiv \lnot\mathrm{Pr}^\mathrm{Ro}_T(\ulcorner \overline{0} = \overline{1} \urcorner)
$ T \vdash \mathrm{Con}^\mathrm{Ro}_T
証明Prop1.bと$ \mathsf{PA} \vdash \lnot(\overline{0} = \overline{1})より.
参考文献