Sign up ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

[Improved version!!]

Suppose $\mathsf{Prov}_R$ is a Rosserized proof predicate for PA (or some other suitable theory). To fix ideas, suppose

$$\mathsf{Prov}_R(\overline{\ulcorner\varphi\urcorner}) = \mathsf{\exists x(Prf(x, \overline{\ulcorner\varphi\urcorner}) \land (\forall y \leq x)\neg Prf(y, \overline{\ulcorner\bot\urcorner}))}$$

where $\mathsf{Prf}$ represents the relation that $m$ has to $n$ when $m$ numbers a proof of the sentence numbered $n$. We can construct a $\Delta_0$ wff $\mathsf{Prf}$, making $\mathsf{Prov}_R$ $\Sigma_1$.

Then, as is familiar,

PA $\vdash \neg\mathsf{Prov}_R(\overline{\ulcorner\bot\urcorner})$

So the HBL derivability conditions can't all hold for $\mathsf{Prov}_R$.

The first condition still holds. And it is reasonably easy to see why the second condition might fail (suppose that ordered by Gödel numbers the proof of $A$ and $A \to C$ precede the first proof of $\bot$ which precedes the first proof of $C$). But we also know that using Jereslow's trick we can get a version of the unprovability of consistency without appeal to the second condition, so the third condition should be the crucial failure.

Well the usual proof of the third condition runs by showing PA $\vdash \psi \to \mathsf{Prov}(\overline{\ulcorner\psi\urcorner})$ for any $\Sigma_1$ $\psi$, and then remarking that $\mathsf{Prov}(\overline{\ulcorner\varphi\urcorner})$ is itself $\Sigma_1$. But this line of argument is presumably going to be blocked at the first stage when we turn to the Rosserized predicate $\mathsf{Prov}_R$: i.e. we won't have PA $\vdash \psi \to \mathsf{Prov}_R(\overline{\ulcorner\psi\urcorner})$ for every $\Sigma_1$ $\psi$. [And it is plausible this should fail, I guess.]

So we know the third condition fails. But -- and here at last is the questions:

Is there a simple counterexample to PA $\vdash \psi \to \mathsf{Prov}_R(\overline{\ulcorner\psi\urcorner})$ for $\Sigma_1$ $\psi$,

and if that counterexample doesn't already involve $\mathsf{Prov}_R$,

Are there known constructions of suitable wffs $\theta$ such that we have a nice illustration of a case where PA $\nvdash \mathsf{Prov}_R(\overline{\ulcorner\theta\urcorner}) \to \mathsf{Prov}_R(\overline{\ulcorner\mathsf{Prov}_R(\overline{\ulcorner\theta\urcorner})\urcorner})$

either for the given Rosserized predicate, or some cousin?

share|cite|improve this question
My question relates to the answer below - why do you claim that $\mathsf{Prov}_R$ is not $\Sigma_1$? – Mad Hatter Apr 8 '13 at 6:25

1 Answer 1

Isn't Prf(x,y) a $\Delta_0$ relation? And so doesn't that make Rosserized provability predicates $\Sigma_1$?

share|cite|improve this answer
Oops, no excuses, I was having bad senior moment: yes of course you can, as a best case, construct a suitable $\Sigma_0$ wff for Prf. I've rephrased the question! (Thanks!) – Peter Smith Apr 8 '13 at 7:26
Actually, even $$PA \vdash Prov_R (A \rightarrow B) \rightarrow (Prov_R (A) \rightarrow Prov_R (B))$$ isn't obvious. – Cecil Apr 8 '13 at 18:48
What is Jereslow's trick? I can't find a reference. – Cecil Apr 8 '13 at 18:51
Yes, as I said, the second condition can fail. As for Jereslow's trick see e.g. my Gödel book, §33.5 in the second edition, based on Jeroslow, R. G., 1973, Redundancies in the Hilbert-Bernays derivability conditions for Gödel’s second incompleteness theorem. Journal of Symbolic Logic, 38: 359–367. – Peter Smith Apr 8 '13 at 20:49
Thanks for the reference. Sorry, I am dense, why do we have $$ PA \vdash \neg \mbox{Prov} _R (\bot)?$$ – Cecil Apr 9 '13 at 11:17

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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