A many-sorted variant of Japaridze's polymodal provability logicстатья
Информация о цитировании статьи получена из
Web of Science,
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 24 января 2020 г.
Аннотация: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 α≤ω, 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.