 From the time GL was formulated, researchers wondered whether it was adequate for formal theories like Peano Arithmetic (PA): does GL prove everything about the notion of provability that can be expressed in a propositional modal language and can be proved in Peano Arithmetic, or should more principles be added to GL? To make this notion of adequacy more precise, we define a realization (sometimes called translation or interpretation) to be a function f that assigns to each propositional atom of modal logic a sentence of arithmetic, where