 This theorem says essentially that the modal logic GL captures everything that Peano Arithmetic can truthfully say in modal terms about its own provability predicate. The direction from left to right, arithmetical soundness of GL, is discussed above. Solovay set out to prove the other, much more difficult, direction by contraposition. His proof is based on intricate self-referential techniques, and only a small glimpse can be given here.