Derivability conditions on Rosser's provability predicates (Q2641298)

As the author states, this is a complement to a paper by \textit{D. Guaspari} and \textit{R. M. Solovay} [Ann. Math. Logic 16, 81-99 (1979; Zbl 0426.03062)]: the author considers Rosser sentences in the milieu of PRA \((=\) open induction with parameters for primitive recursive functions), while Guaspari and Solvay did so in Peano arithmetic. For a provability predicate \(P(a):=\exists y\theta (y,a)\), the associated Rosser predicate R(a) is defined to be \(\exists y(\theta (y,a)\&\forall z\leq y\neg \theta (z,\neg a))\). [Here and below, Gödel numbering and the like are suppressed.] Given a provability predicate P(a) that satisfies (*) \(\vdash \forall formula x,y[P(x\to y)\to P(x)\to P(y)]\) (`\(\vdash '\) for `PRA\(\vdash ')\), and two other reasonable conditions, the author constructs other predicates \(P_ 1\) and \(P_ 2\) that are equivalent to P, i.e. \(\vdash \forall formula P(x)\leftrightarrow P_ 1(x)\leftrightarrow P_ 2(x)\), and such that their Rosser versions \(R_ 1\) and \(R_ 2\) have the following properties: (*) holds for \(R_ 1\) in place of P, and for \(R_ 2\) (**) \(\vdash \forall formula x[R_ 2(x)\to R_ 2(R_ 2(x))]\). (Of course, neither \(R_ 1\) nor \(R_ 2\) can satisfy both (*) and (**).) The author's construction of these predicates is intricate, but straightforward. Unlike Guaspari and Solovay, he does not go into modality considerations.