A note on some extension results (Q1814182)

In an earlier paper of the authors [Arch. Math. Logic 27, 115-133 (1988; Zbl 0688.03041)] extensions of Guaspari-Solovay provability logic [\textit{D. Guaspari} and \textit{R. Solovay}, Ann. Math. Logic 16, 81-99 (1979; Zbl 0426.03062)] by ``Rosser fixed points'' were considered. Guaspari-Solovay logic has the connectives \(\square\), \(\preccurlyeq\), \(\prec\); \(\square\) expresses provability is an arithmetical theory, \(\square A\preccurlyeq\square B\) (resp. \(\square A\prec\square B\)) reflects the fact that \(A\) has a proof which is not longer (resp. shorter) than any proof of \(B\). The authors' cited paper considered the Guaspari-Solovay system \(R^ -\), its extension \(R\) by the rule \(\square A/A\); \(RFP^{(- )}\) is an extension of \(R^{(-)}\) with propositional constants (``fixed points'') \(c_ 0\), \(c_ 1,\ldots\) satisfying axioms \(c_ n\equiv(A_ nc_ n\preccurlyeq B_ nc_ n)\) \((\langle A_ np,B_ np\rangle\) is a \(PR\)-sequence enumerating all pairs of formulas). It was proved that \(RFP\) is conservative over \(R\) and over \(RFP_ n\) (subsystem of \(RFP\) using only \(c_ 0,\ldots,c_ n\)), but the proof was not entirely modal and involved arithmetical interpretation. In the new paper, a weaker conservativity result is proved by applying Kripke models. It is required that formulas \(A_ n\), \(B_ n\) occurring in the axioms \(c_ n\equiv(A_ nc_ n\preccurlyeq B_ nc_ n)\) should not contain \(\preccurlyeq\), \(\prec\). The corresponding systems are again denoted by \(RFP_ n^{(-)}\), \(RFP^{(-)}\) (which makes some confusion with the previous paper). The main results are: \(RFP^{(-)}\) is conservative over \(R^{(-)}\) and over \(RFP_ n^{(-)}\); \(RFP^{(- )}_{n+1}\) is conservative over \(RFP_ n^{(-)}\).