Intuitionistic G\"odel-L\"ob logic, \`a la Simpson: labelled systems and birelational semantics

TL;DR

This paper develops an intuitionistic G"odel-L"ob modal logic using proof-theoretic and birelational semantics techniques, including labelled systems and cyclic proof theory, to handle non-first-order definable frame conditions.

Contribution

It introduces a new labelled system for intuitionistic G"odel-L"ob logic that incorporates both modalities and establishes its semantic equivalence via birelational semantics.

Findings

The labelled system  IGL coincides with birelational semantics where the composition of relations is conversely well-founded.

The logic  IGL is sound and complete with respect to the birelational semantics.

The approach handles non-first-order definable frame conditions using cyclic proof techniques.

Abstract

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