Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics

We derive an intuitionistic version of Gödel-Löb modal logic ($\mathsf{G}\mathsf{L}$) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, $\mathsf{\ell }\mathsf{I}\mathsf{G}\mathsf{L}$, by restricting a non-wellfounded labelled system for $\mathsf{G}\mathsf{L}$ to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that $\mathsf{G}\mathsf{L}$'s usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of $\mathsf{G}\mathsf{L}$ are typically defined over only the box (and not the diamond), our presentation includes both modalities. Our main result is that $\mathsf{\ell }\mathsf{I}\mathsf{G}\mathsf{L}$ coincides with a corresponding semantic condition in birelational semantics: the composition of the modal relation and the intuitionistic relation is conversely well-founded. We call the resulting logic $\mathsf{I}\mathsf{G}\mathsf{L}$. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of $\mathsf{I}\mathsf{G}\mathsf{L}$.