An open problem about Rosser sentences?
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?