2
$\begingroup$

Famously, Rosser introduced a provability predicate $\pi[A]$ that holds iff $\exists x(xP[A]\wedge\forall y(y\le x\to\lnot yP[\lnot A]))$.

Supposing $PA$ is consistent, what are the adequacy conditions for $\pi$ as compared with the Hilbert-Bernays-Löb derivability conditions for P?

In particular, do we have $\vdash_{PA}\pi[A]\Leftrightarrow\hspace{2pt}\vdash_{PA}A$?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

If we assume that PA is consistent, then the two provability predicates are equivalent, since Rosser provability implies regular provability; and conversely, if there is a proof of $A$ in PA, then by Con(PA) there will be no proof of $\neg A$ at all, let alone one with a shorter proof, and so $A$ is Rosser provable. Thus, PA+Con(PA) proves that $\pi[A]\iff P[A]$. The point is that the Rosser provability predicate becomes more interesting when the theory is inconsistent.

Your final query, however, is a bit different from this equivalence. Nevertheless, that biconditional happens also to be true (arguing in ZFC, say, but it suffices merely that PA is sufficiently sound). Namely, if PA proves $\pi[A]$, then $\pi[A]$ is true, and so there really is a proof of $A$. Conversely, if $A$ is provable in PA, then there will be a specific proof of $A$, and by Con(PA) there is no shorter proof of $\neg A$, and so PA will prove $\pi[A]$.

Perhaps the proof theorists will say exactly what one needs to undertake that argument.

Improve this answer
$\endgroup$
15
  • 1
    $\begingroup$ I guess what we need is that PA is $\Pi^0_1$-sound, since from $PA$ proving $\pi[A]$, we want to know that there really is a proof of $A$. $\endgroup$
    – Joel David Hamkins
    Commented Sep 22, 2015 at 17:45
  • 1
    $\begingroup$ If PA is $\Pi^0_1$-sound, then Con(PA) is true, since otherwise, it would prove everything, including false $\Pi^0_1$ sentences. $\endgroup$
    – Joel David Hamkins
    Commented Sep 22, 2015 at 18:26
  • 1
    $\begingroup$ But $\pi[A]$ is $\Sigma^0_1$, right? So why is it not $\Sigma^0_1$-soundness we need in order to conclude from $PA$ proving $\pi[A]$ that there really is a proof in $PA$ of $A$? $\endgroup$
    – Frode Alfson Bjørdal
    Commented Sep 22, 2015 at 18:46
  • 1
    $\begingroup$ Yes, you are right. It is $\Sigma^0_1$-soundness that I want. $\endgroup$
    – Joel David Hamkins
    Commented Sep 22, 2015 at 18:57
  • 1
    $\begingroup$ PA does prove all true existentials, yes. But the last remark is not quite right. It is correct that $\Sigma^0_1$-soundness implies consistency, since if the theory is inconsistent, then it proves everything, including false statements of that complexity; but this amount of soundness is not necessarily equivalent to consistency, since one can have a model of PA+Con(PA)+$\neg$Con(PA+Con(PA)), and in this model, PA is consistent, but not $\Sigma^0_1$-sound, because this model thinks that PA proves that Con(PA) implies 0=1, which is a $\Sigma^0_1$-assertion, but it isn't true in this model. $\endgroup$
    – Joel David Hamkins
    Commented Sep 22, 2015 at 19:43

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .