 Rosser proof-order dependence

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].