On the proof of Solovay's theorem (Q1176096)

In the original proof of arithmetical completeness for the modal logic \(L\) by Solovay the key lemma is established by employing the formalized recursion theorem. In this paper it is shown that the use of the recursion theorem can be replaced by the diagonalization lemma for arithmetic: the authors give the analogous key lemma by means of self- referential sentences and prove it mainly by modal properties of the arithmetic. As a consequence, arithmetical completeness is extended to a large class of fragments of PA such as any \(\Sigma_ 1\)-sound RE- extension of \(I\Delta_ 0=\text{EXP}\). The proof is developed in the framework of the so-called Rosser logic \(R\) of Guaspari and Solovay dealing with witness comparisons, whose arithmetical completeness is also proved in the same way.