2023/09/01 by Das, Anupam, van der Giessen, Iris, Marin, Sonia · 2 citations
#F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2309.00532
We derive an intuitionistic version of Gödel-Löb modal logic (\sfGL) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, \sfℓ IGL, by restricting a non-wellfounded labelled system for \sfGL to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that \sfGL's usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of \sfGL are typically defined over only the box (and not the diamond), our presentation includes both modalities. Our main result is that \sfℓ 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 \sfIGL. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of \sfIGL.