Sequent calculi for intuitionistic Gödel-Löb logic

Iris van der Giessen, Rosalie Iemhoff

Research output: Contribution to journalArticlepeer-review

5 Downloads (Pure)


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.
Original languageEnglish
Pages (from-to)221-246
Number of pages26
JournalNotre Dame Journal of Formal Logic
Issue number2
Publication statusPublished - 9 Jun 2021
Externally publishedYes


  • cut-admissibility
  • Gödel–Löb logic
  • Intuitionistic logic
  • sequent calculi


Dive into the research topics of 'Sequent calculi for intuitionistic Gödel-Löb logic'. Together they form a unique fingerprint.

Cite this