Arithmetic with a local reflection principle for Rosser provability formulas (Q908911)

The main theorem: There exists a \(\Sigma^ 0_ 1\)-formula Th(x) which is equivalent in Peano arithmetic PA to the standard Gödel \(\Sigma^ 0_ 1\)-formula Pr(x) of provability such that the theory \(PA+Rfn(Th^ R)\) coincides with \(PA+Rfn\) or equivalently that \(PA+Rfn(Th^ R)\vdash con(PA)\). Here \(Th^ R(x)=_{def}Th(x)\prec Th({\dot \neg}x)=_{def}\) ``x is Th-provable before \({\dot \neg}x''\) is the Rosser provability formula for Th, Rfn is the local reflection principle Pr(\(\ulcorner \phi \urcorner)\to \phi\) for arithmetical sentences \(\phi\), and \(Rfn(Th^ R)\) is the analogous principle \(Th^ R(\ulcorner \phi \urcorner)\to \phi\). The proof is based on (arithmetical and Kripke-style) completeness results of \textit{D. Guaspari} and \textit{R. M. Solovay} [Ann. Math. Logic 16, 81-99 (1979; Zbl 0426.03062)] and \textit{F. Voorbraak} [``A simplification of the completeness proof for Guaspari and Solovay's R'', Logic Group Preprint Series No.8, Dept. Philos., Univ. Utrecht (1986)] for a provability propositional logic with modal operators \(\square A\), \(\square A\preccurlyeq \square B\) and \(\square A\prec \square B\) interpreted respectively as Th-provability (of a translation) of A and as Th-provability of A nonstrictly or strictly before that of B. In fact it rests on the construction of a Kripke model and therefore of an arithmetical interpretation for the modal formula \(\square [(\square p\prec \square \neg p\to p)\wedge (\square q\prec \square \neg q\to q)\to \neg \square \perp]\) where conjuncts correspond to \(Rfn(Th^ R)\) and \(\neg \square \perp\) corresponds to con(PA). However this is impossible for the formula \(\square [(\square p\prec \square \neg p\to p)\to \neg \square \perp]\). There are some misprints in the paper. In particular the definition of A-correctness of Kripke R-models is unclear.