Sequent calculi for intuitionistic Gödel-Löb logic (Q1982008)

The paper investigates two sequent calculi for the modal logic iGL, which is the intuitionistic version of the Gödel-Löb logic (the classical provability logic). The first one, GL3i, is a common cut-free one-sided sequent calculus for intuitionistic logic augmented with the GL modal rule \[ \frac{\Box\Gamma,\Gamma,\Box A\Rightarrow A}{\Pi,\Box\Gamma\Rightarrow\Box A}; \] the second-one, GL4i, is based on the Dyckhoff-Hudelmaier terminating intuitionistic calculus. The paper proves in detail that cut is admissible in GL3i, using ideas by \textit{S. Valentini} [J. Philos. Logic 12, 471--476 (1983; Zbl 0535.03031)] and \textit{R. Goré} and \textit{R. Ramanayake} [Rev. Symb. Log. 5, No. 2, 212--238 (2012; Zbl 1254.03113)], and that GL4i is terminating. The authors go on to show the equivalence of GL3i and GL4i (which implies cut admissibility in GL4i, and that both calculi are sound and complete for the logic iGL), and the Craig interpolation property for iGL.