We derive an intuitionistic version of G\"odel-L\"ob modal logic ($\sf{ GL}$) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, $\sf{ \ell IGL}$, by restricting a non-wellfounded labelled system for $\sf{ GL}$ to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that $\sf{ GL}$'s usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of $\sf{ GL}$ are typically defined over only the box (and not the diamond), our presentation includes both modalities. Our main result is that $\sf{ \ell IGL}$ 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 $\sf{ IGL}$. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of $\sf{ IGL}$.
Categories: cs.LO math.LO