Fix on a provability predicate Prov for a suitable theory T (there’s a lot of choices to make here, starting of course with a choice of Gödel coding). Then any Gödel sentence in the sense of a fixed point for Prov is provably equivalent in T to the consistency sentence not-Prov(0=1). So these Gödel sentences are all equivalent. That’s all familiar.
Now Rosserize the provability predicate in the usual way, and consider Rosser sentences, meaning fixed points for this doctored predicate. The question was recently asked on math.stackexchange: are these Rosser sentences also provably equivalent with each other?
I knew there was a relevant paper by D. Guaspari and R. Solovay, ‘Rosser Sentences’, Annals of Math. Logic vol 16 (1979), pp. 81-99. And their key relevant result about Rosser sentences is this. There are some ‘standard’ provability predicates whose Rosser sentences are all equivalent, and there are other ‘standard’ provability predicates whose Rosser sentences are not all equivalent. (Being standard is a matter of satsifying two of the usual derivability conditions.)
The proofs of these results need quite a bit of apparatus: and the authors remark that the situation with respect to the “usual” provability predicate constructed in the normal way without fancy tweaking “seems to be very difficult” and is [or rather was at that time of publication, 1979] unsettled. But is the question still unsettled?
Well, I note that in Buss’s Handbook of Proof Theory (1998), p. 496, it is still reported as an open question whether there is a reasonable notion of “usual” provability predicate for which it can be settled whether or not all Rosser sentences for such a predicate are equivalent. It is interesting that the problem should be this intractable. I just don’t know whether there is any more recent work which sheds further light. Any offers?
I keep returning to this interesting problem. Last summer I discussed it briefly with Volodya Shavrukov who agreed it is still open. He has also written on the subject in On Rosser’s Provability Predicate, Math. Log. Quart., Vol. 37, pp 317-330.
My current view is the following: The proof predicates constructed by Guaspari and Solovay coincide with “the usual” proof predicate on the natural numbers. Since Rosser sentences lack standard proofs, they really claim something about the order of their non-standard proofs and refutations. It seems to me that this ordering can depend on e.g. the Gödel numbering of symbols, the encoding of finite sequences and the choice of proof system. Smorynski points out in Self-reference and modal logic (Springer, 1985) that the question of Rosser sentences’ equivalence is the first concerning Pr that requires more than the derivability conditions plus Löb’s theorem for a settlement. This suggest that the question might not be about “the usual” proof predicate, but rather about something else.
It has also been shown that the set of Rosser sentences is a complete \Sigma_1 set, a result that does not depend on the choice of proof predicate. The full text can be found at http://hdl.handle.net/2077/25513
Many thanks for this!
A 2006 acacademic thesis claimed that the problem was still open.
https://gupea.ub.gu.se/bitstream/2077/25475/1/gupea_2077_25475_1.pdf
In a related matter, a 2008 paper by Christopher von Bülow claimed that the hypotheses in the 1979 paper needed a bit of reinforcement.
Apologies if these were already well known.
Thanks for this!