Skip to main content
4 of 5
added 1 character in body

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$?