10
$\begingroup$

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.

$\endgroup$
11
$\begingroup$

This is a non-trivial question!

There is 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. 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. I don't know whether there is any more recent work which sheds further light.

$\endgroup$
  • $\begingroup$ This paper claims that there's an oversight in the paper you cite, and that the premises have to be strengthened to fix the oversight. ​ (I have not reviewed their argument.) ​ ​ ​ ​ $\endgroup$ – user57159 Aug 5 '17 at 7:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.