Sequent calculi for intuitionistic gödel-löb logic

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.