直觉主义 Gödel-Löb 逻辑，à la Simpson：带标签系统与双关系语义
Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics
AI总结：
本文通过证明论技术提出直觉主义 Gödel-Löb 逻辑 IGL，包含盒与菱形模态，并证明其带标签系统与双关系语义中逆良基复合条件等价，主要贡献在于完备性证明需经多个中间刻画。
摘要：
我们通过证明论技术，以 Simpson 风格推导出 Gödel-Löb 模态逻辑（$\sf{GL}$）的直觉主义版本。通过将 $\sf{GL}$ 的非良基带标签系统限制为右侧仅有一个公式，我们恢复了一个带标签系统 $\sf{\ell IGL}$。后者是利用循环证明论技术获得的，绕过了 $\sf{GL}$ 通常的框架条件（逆良基性）不是一阶可定义这一障碍。虽然现有的直觉主义版本 $\sf{GL}$ 通常仅定义在盒模态（而非菱形模态）上，但我们的表述包含两种模态。我们的主要结果是 $\sf{\ell IGL}$ 与双关系语义中的相应语义条件一致：模态关系与直觉主义关系的复合是逆良基的。我们将所得逻辑称为 $\sf{IGL}$。虽然可靠性方向使用标准思想证明，但完备性方向更为复杂，需要通过 $\sf{IGL}$ 的若干中间刻画进行迂回。
英文摘要：
We derive an intuitionistic version of Gödel-Löb 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}$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
