Abstract: We will begin with a cursory overview of modal logic, the meaning of soundness and completeness, and the traditional axiomatic extensions. The provability logic will be motivated by Lobs theorem, and we will explore the axiomatic extension known as GL, and discover the extent to which CL is able to encapsulate provability statements in Peano arithmetic, such that the Second Incompleteness Theorem. Time permitting, we will get into the details of Solovay’s proof of the completeness of GL with respect to Peano arithmetic. The presentation will be heavily motivated by The Unprovability of Consistency by George Boolos. Please note the unusual location.