On Solovay's Theorem and a Proof of Arithmetical Completeness of a New Predicate Modal Logic

This thesis investigates a first-order extension of GL called ML3. We briefly discuss the latters properties and some of its toolbox: some metatheorems, the conservation theorem, and its semantic completeness (with respect to finite reverse wellfounded Kripke models). Applying the Solovay technique to those models the thesis establishes its main result, namely, that ML3 is arithmetically complete. As expanded below, ML3 is a first-order modal logic that along with its built-in ability to simulate general classical first-order provability having simulate the metamathematical classical is also arithmetically complete in the Solovay sense. We also carefully reconstruct the proof of Solovays Lemmata in our Appendixes, including a complete mathematically rigorous construction of his graph-walking function h.