MONADIC INTUITIONISTIC AND MODAL LOGICS ADMITTING PROVABILITY INTERPRETATIONS

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