= Rosser predicates in inconsistent theories depend on proof order
{c}
{title2=$R_T(\ulcorner A\urcorner)=\exists p\,[\operatorname{Proof}_T(A,p)\wedge\forall q\le p\,\neg\operatorname{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.
Back to article page
