# Is there more than one Rosser sentence?

Let $T$ be a recursively axiomatized consistent extension of PA (if you're so inclined you can replace PA everywhere with Robinson's Q). Let $\mathrm{bws}_T(p,\varphi)$ be the proof predicate, expressing that $p$ is a proof in $T$ of $\varphi$ and $\mathrm{bwb}_T(\varphi)$ the provability predicate, expressing that there exists such a proof $p$.

A Gödel sentence for $T$ is a sentence $\sigma$ such that $$PA\vdash \sigma\iff\lnot\mathrm{bwb}_T(\sigma)$$ A Rosser sentence for $T$ is a sentence $\tau$ such that $$PA\vdash \tau\iff (\forall p\colon \mathrm{bws}_T(p,\tau)\implies \exists q\leq p\colon \mathrm{bws}_T(q,\lnot\tau))$$

It can be shown that any Gödel sentence for $T$ is provably equivalent over $T$ to Con($T$) (Andreas Blass sketched a proof of this in an answer to a previous question of mine). Therefore there is, up to $T$-provable equivalence, a single Gödel sentence for $T$.

Does a similar conclusion hold for Rosser sentences? Or are there two nonequivalent Rosser sentences for some theory $T$?

Joel David Hamkins shows in this MO answer that the sentences obtained from Gödel's fixed point lemma (which gives the existence of Gödel and Rosser sentences) are not unique in general. In a comment to the same answer Sridhar Ramesh gives an argument based on Löb's theorem, showing that fixed points are unique if the template, whose fixed points we are looking for, preserves provable equivalence. But this doesn't seem to be the case for the Rosser template; the precise bound $q\leq p$ prevents us from simply stitching proofs together.