  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}$.
