A simplification of the completeness proofs for Guaspari and Solovay's ${\rm R}$.
Frans P. J. M. Voorbraak · Notre Dame Journal of Formal Logic · 1989
Alternative proofs for Guaspari and Solovay's completeness theorems for R are presented.R is an extension of the provability logic L and was developed in order to study the formal properties of the provability predicate of PA occurring in sentences that may contain connectives for witness comparison.(The primary example of sentences involving witness comparison is the Rosser sentence.)In this article the proof of the Kripke model completeness theorems employs tail models, as introduced by Visser, instead of the more usual finite Kripke models.The use of tail models makes it possible to derive arithmetical completeness from Kripke model completeness by literally embedding Kripke models into PA.Our arithmetical completeness theorem differs slightly from the one proved by Guaspari and Solovay, and it also forms a solution to the problem (advanced by Smoryήski) of obtaining a completeness result with respect to a variety of orderings.