What are the adequacy conditions for Rosser Provability? 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$?
 A: 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.
