• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Article

A many-sorted variant of Japaridze's polymodal provability logic

Logic Journal of the IGPL. 2018. Vol. 26. No. 5. P. 505-538.
Berger G., Beklemishev L. D., Tompits H.

We consider a many-sorted variant of Japaridze’s polymodal provability logic (⁠GLP⁠). In this variant, which is denoted GLP∗⁠, propositional variables are assigned sorts n≤ω⁠, where variables of finite sort n<ω are interpreted as Π_{n+1}-sentences of the arithmetical hierarchy, while those of sort ω range over arbitrary ones. We prove that GLP∗is arithmetically complete with respect to this interpretation. Moreover, we relate GLP∗ to its one-sorted counterpart GLP and prove that the former inherits some well-known properties of the latter, like Craig interpolation and polynomial space (PSPACE) decidability. We also study a positive variant of GLP∗ that 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 GLP∗ is arithmetically complete.