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

DOI10.1093/JIGPAL/JZY012MaRDI QIDQ5095650zbMATH OpenOpenAlexWikidataFDO

Authors Gerald Berger, Hans Tompits, Lev D. Beklemishev

Publication date 10 August 2022

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1601.02857

zbMATH Keywords

formal arithmeticmodal logicprovability logicsmathematical logicarithmetical completeness

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

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

Recommendations

• On provability logics with linearly ordered modalities
• A simplified proof of arithmetical completeness theorem for provability logic GLP
• The analytical completeness of Dzhaparidze's polymodal logics
• Kripke semantics for provability logic GLP
• Positive provability logic for uniform reflection principles

Cited in

(2)

• Many-sorted equivalence of shiny and strongly polite theories
• On provability logics with linearly ordered modalities

This page was built for publication: A many-sorted variant of Japaridze's polymodal provability logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5095650)