Rosser provability predicate ($R_T(x)=\exists y({\mathrm{Prf}}_T(x,y)\wedge \forall z\le y\neg {\mathrm{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(┌\perp ┐)$ by splitting proof codes before and after a fixed proof of $\neg \perp$. This does not establish the usual consistency statement for ordinary provability.

The internal derivability conditions of a Rosser provability predicate depend on the proof numbering, even when the ordinary provability predicate is unchanged up to provable equivalence. Joining proofs of $A$ and $A\to B$ can increase their codes beyond the two bounds in the Rosser hypotheses, leaving the absence of earlier proofs of $\neg B$ unestablished. Internal modus ponens rule therefore needs a separate argument for the chosen numbering. Proof predicates can be constructed with different combinations of closure and introspection properties. ^[ref]. ^[ref].

If a first-order theory proves both $A$ and $\neg A$, the external truth of its Rosser provability predicate for $A$ depends on which side has the earlier formal proof code. A reserved least code for a formal proof of $\neg A$ makes the Rosser assertion false. Reserving the least code for a formal proof of $A$ makes it true. These are legitimate effective renumberings of the same formal proofs. Inconsistent first-order theories therefore require an explicit proof-order convention.