We derive an intuitionistic version of Gödel-Löb modal logic (GL) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, ℓIGL, by restricting a non-wellfounded labelled system for GL to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that GL’s usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of GL are typically defined over only the box (and not the diamond), our presentation includes both modalities. Our main result is that ℓ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 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 IGL.
@InProceedings{das_et_al:LIPIcs.CSL.2024.22, author = {Das, Anupam and van der Giessen, Iris and Marin, Sonia}, title = {{Intuitionistic G\"{o}del-L\"{o}b Logic, \`{a} la Simpson: Labelled Systems and Birelational Semantics}}, booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)}, pages = {22:1--22:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-310-2}, ISSN = {1868-8969}, year = {2024}, volume = {288}, editor = {Murano, Aniello and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.22}, URN = {urn:nbn:de:0030-drops-196654}, doi = {10.4230/LIPIcs.CSL.2024.22}, annote = {Keywords: provability logic, proof theory, intuitionistic modal logic, cyclic proofs, non-wellfounded proofs, proof search, cut-elimination, labelled sequents} }
Feedback for Dagstuhl Publishing