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

翻译：我们以辛普森风格，通过证明论技术导出了哥德尔-勒布模态逻辑（$\sf{GL}$）的直觉主义版本。通过将$\sf{GL}$的非良基带标签系统限制为右侧仅含单一公式，我们得到了一个带标签系统$\sf{\ell IGL}$。后者利用循环证明论技术获得，避开了$\sf{GL}$通常的框架条件（逆良基性）非一阶可定义这一障碍。尽管现有直觉主义版本的$\sf{GL}$通常仅定义在box模态（而非diamond模态）上，我们的表述同时包含了两种模态。我们的主要结果是：$\sf{\ell IGL}$与二元关系语义中的对应语义条件（即模态关系与直觉主义关系的复合是逆良基的）完全一致。我们将由此得到的逻辑称为$\sf{IGL}$。其中，可靠性方向的证明采用了标准方法，而完全性方向的证明更为复杂，需要通过对$\sf{IGL}$的若干中间刻画进行迂回论证。