Abstract:
We present a simplified proof of Japaridze's arithmetical completeness theorem for the well-known polymodal provability logic $\mathbf{GLP}$. The simplification is achieved by employing a fragment $\mathbf J$ of $\mathbf{GLP}$ that enjoys a more convenient Kripke-style semantics than the logic considered in the papers by Ignatiev and Boolos. In particular, this allows us to simplify the arithmetical fixed point construction and to bring it closer to the standard construction due to Solovay.