A simplification of the completeness proofs for Guaspari and Solovay's R (Q923070)

The author gives alternative completeness proofs for Guaspari and Solovay's modal logic R which characterizes the formal properties of provability predicate and witness comparison of PA. The Kripke model completeness is proved by using tail models instead of finite Kripke models, from which there follows the arithmetical completeness by literally embedding Kripke models in PA. The arithmetical completeness proved in this paper is slightly different from Guaspari and Solovay's and forms a solution to Smorynski's problem of obtaining a completeness result with respect to a variety of orderings.