Sequent Calculi for Intuitionistic Gödel–Löb Logic

This paper provides a study of sequent calculi for intuitionistic Godel–Lob logic (iGL), which is the intuitionistic version of the classical modal logic GL, known as Godel–Lob 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 Godel–Lob logic.