Monadic Intuitionistic and Modal Logics Admitting Provability Interpretations
Guram Bezhanishvili, Kristina Brantley, Julia Ilin

TL;DR
This paper extends provability interpretations from classical intuitionistic and modal logics to their monadic extensions, establishing embeddings and arithmetical interpretations through added formulas and translations.
Contribution
It introduces monadic extensions of IPC, Grz, and GL, and proves embeddings and arithmetical interpretations for these extended systems.
Findings
Monadic extensions admit similar embeddings as their base logics.
Adding Casari's formula enables embeddings of monadic IPC into monadic Grz.
Solovay's theorem extends to monadic GL, allowing arithmetical interpretations.
Abstract
The G\"odel translation provides an embedding of the intuitionistic logic into the modal logic , which then embeds into the modal logic via the splitting translation. Combined with Solovay's theorem that is the modal logic of the provability predicate of Peano Arithmetic , both and admit arithmetical interpretations. When attempting to 'lift' these results to the monadic extensions , , and of these logics, the same techniques no longer work. Following a conjecture made by Esakia, we add an appropriate version of Casari's formula to these monadic extensions (denoted by a '+'), obtaining that the G\"odel translation embeds into and the splitting translation embeds into . As…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Advanced Algebra and Logic
