Monadic Intuitionistic and Modal Logics Admitting Provability Interpretations

Abstract

The G\"odel translation provides an embedding of the intuitionistic logic $\mathsf{IPC}$ into the modal logic $\mathsf{Grz}$, which then embeds into the modal logic $\mathsf{GL}$ via the splitting translation. Combined with Solovay's theorem that $\mathsf{GL}$ is the modal logic of the provability predicate of Peano Arithmetic $\mathsf{PA}$, both $\mathsf{IPC}$ and $\mathsf{Grz}$ admit arithmetical interpretations. When attempting to 'lift' these results to the monadic extensions $\mathsf{MIPC}$, $\mathsf{MGrz}$, and $\mathsf{MGL}$ 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 $\mathsf{M^{+}IPC}$ into $\mathsf{M^{+}Grz}$ and the splitting translation embeds $\mathsf{M^{+}Grz}$ into $\mathsf{MGL}$. As proven by Japaridze, Solovay's result extends to the monadic system $\mathsf{MGL}$, which leads us to an arithmetical interpretation of both $\mathsf{M^{+}IPC}$ and $\mathsf{M^{+}Grz}$.