Rosser predicates in inconsistent theories depend on proof order ($R_T(┌A┐)=\exists p[{\mathrm{Proof}}_T(A,p)\wedge \forall q\le p\neg {\mathrm{Proof}}_T(\neg A,q)]$)

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.