Rosser predicates in inconsistent theories depend on proof order
ID: rosser-predicates-in-inconsistent-theories-depend-on-proof-order
If a first-order theory proves both and , the external truth of its Rosser provability predicate for depends on which side has the earlier formal proof code. A reserved least code for a formal proof of makes the Rosser assertion false. Reserving the least code for a formal proof of makes it true. These are legitimate effective renumberings of the same formal proofs. Inconsistent first-order theories therefore require an explicit proof-order convention.
New to topics? Read the docs here!