= Rosser provability predicate
{c}
{title2=$R_T(x)=\exists y(\operatorname{Prf}_T(x,y)\wedge\forall z\leq y\,\neg\operatorname{Prf}_T(\dot\neg x,z))$}
A Rosser provability predicate adds a bounded proof-order test to an <arithmetical provability predicate>: a proof of the sentence must occur before every proof of its <negation>. For a consistent theory it has the same standard extension as ordinary provability. Internally its behavior can differ: <arithmetic> proves $\neg R_T(\ulcorner\bot\urcorner)$ by splitting proof codes before and after a fixed proof of $\neg\bot$. This does not establish the usual consistency statement for ordinary provability.
Back to article page
