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

We consider a many-sorted variant of Japaridze’s polymodal provability logic $\mathsf{G}\mathsf{L}\mathsf{P}$. In this variant, which is denoted ${\mathsf{G}\mathsf{L}\mathsf{P}}^{\ast }$, propositional variables are assigned sorts $\alpha \le \omega$, where variables of finite sort $n<\omega$ are interpreted as ${\mathrm{\Pi }}_{n+1}$-sentences of the arithmetical hierarchy, while those of sort $\omega$ range over arbitrary ones. We prove that ${\mathsf{G}\mathsf{L}\mathsf{P}}^{\ast }$ is arithmetically complete with respect to this interpretation. Moreover, we relate ${\mathsf{G}\mathsf{L}\mathsf{P}}^{\ast }$ to its one-sorted counterpart $\mathsf{G}\mathsf{L}\mathsf{P}$ 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{G}\mathsf{L}\mathsf{P}}^{\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{G}\mathsf{L}\mathsf{P}}^{\ast }$ is arithmetically complete.