A Many-Sorted Variant of Japaridze's Polymodal Provability Logic

Abstract

We consider a many-sorted variant of Japaridze's polymodal provability logic $\mathsf{GLP}$. In this variant, which is denoted ${\mathsf{GLP}}^{\ast }$, propositional variables are assigned sorts $\alpha \le \omega$, where variables of finite sort $n<\omega$ are interpreted as ${\Pi }_{n+1}$-sentences of the arithmetical hierarchy, while those of sort $\omega$ range over arbitrary ones. We prove that ${\mathsf{GLP}}^{\ast }$ is arithmetically complete with respect to this interpretation. Moreover, we relate ${\mathsf{GLP}}^{\ast }$ to its one-sorted counterpart $\mathsf{GLP}$ and prove that the former inherits some well-known properties of the latter, like Craig interpolation and PSpace decidability. We also study a positive variant of ${\mathsf{GLP}}^{\ast }$ which allows for an even richer arithmetical interpretation---variables are permitted to range over theories rather than single sentences. This interpretation in turn allows the introduction of a modality that corresponds to the full uniform reflection principle. We show that our positive variant of ${\mathsf{GLP}}^{\ast }$ is arithmetically complete.

{A version of this article has been published in the Logic Journal of the IGPL, 26(5): 505--538 (2018)