= Rosser proof-order dependence
{c}
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. https://sartemov.ws.gc.cuny.edu/files/2012/10/Artemov-Beklemishev.-Provability-logic.pdf[Provability Logic, printed page 87, Rosser provability and proof-numbering dependence]{ref}. https://arxiv.org/abs/1902.06863[Rosser provability and the second incompleteness theorem, constructions of differing derivability conditions]{ref}.
Back to article page
