Sequent Calculi for Intuitionistic Gödel-Löb Logic
Publication date
2021-05
Authors
van der Giessen, Iris
Iemhoff, Rosalie
Editors
Advisors
Supervisors
Document Type
Article
Metadata
Show full item recordCollections
License
taverne
Abstract
This paper provides a study of sequent calculi for intuitionistic Gödel-Löb logic (iGL), which is the intuitionistic version of the classical modal logic GL, known as Gödel-Löb logic. We present two different sequent calculi, one of which we prove to be the terminating version of the other. We study those systems from a proof-theoretic point of view. One of our main results is a syntactic proof for the cut-admissibility result for those systems. Finally, we apply this to prove Craig interpolation for intuitionistic Gödel-Löb logic.
Keywords
Cut-admissibility, Gödel-Löb logic, Intuitionistic logic, Sequent calculi, Taverne, Logic
Citation
van der Giessen, I & Iemhoff, R 2021, 'Sequent Calculi for Intuitionistic Gödel-Löb Logic', Notre Dame Journal of Formal Logic, vol. 62, no. 2, pp. 221-246. https://doi.org/10.1215/00294527-2021-0011