A simplification of the completeness proofs for Guaspari and Solovav's R
Frans P. J. M. Voorbraak · Utrecht University Repository (Utrecht University) · 1986
Alternative proofs for Guaspari and Solovay's completeness the- orems 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 wit- ness comparison. (The primary example of sentences involving witness com- parison 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 pos- sible 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 obtain- ing a completeness result with respect to a variety of orderings.