A Terminating Sequent Calculus for Intuitionistic Strong Löb Logic with the Subformula Property

Intuitionistic Strong Löb logic \(\textsf{iSL}\) is an intuitionistic modal logic with a provability interpretation. We introduce \(\textsf{GbuSL}_{\Box } \) , a terminating sequent calculus for \(\textsf{iSL}\) with the subformula property. \(\textsf{GbuSL}_{\Box } \) modifies the sequent calculus \(\textsf{G3iSL}_{\Box } \) for \(\textsf{iSL}\) based on \(\textsf{G3i} \) , by annotating the sequents to distinguish rule applications into an unblocked phase, where any rule can be backward applied, and a blocked phase where only right rules can be used. We prove that, if proof search for a sequent \(\sigma \) in \(\textsf{GbuSL}_{\Box } \) fails, then a Kripke countermodel for \(\sigma \) can be constructed.