Rosser and Mostowski sentences (Q1263586)

The authors provide a modal framework for the study of Rosser and Mostowski sentences of Peano Arithmetic. The properties of the operator called witness comparison, with which Rosser sentences can be discussed, have been analysed in a modal system by \textit{D. Guaspari} and \textit{R. M. Solovay} [Ann. Math. Logic 16, 81-99 (1979; Zbl 0426.03062)]. In the system, however, it has been shown that there are no fixed points for Rosser formulae. Several extensions of the system, therefore, are defined in this paper by adding new constants to fill the role of the fixed points so that not only Rosser sentences but also Mostowski sentences are discussed uniformly in a more complete modal setting. The main result is a lemma called intersection lemma, from which immediately follow the formalized Rosser theorem, the Friedman-Goldfarb-Harrington's principle, and so on. The arithmetical completeness and semantical completeness by Kripke models for the systems are also proved.