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

Intuitionistic Strong Lob logic iSL is an intuitionistic modal logic with a provability interpretation. We introduce GbuSL(square), a terminating sequent calculus for iSL with the subformula property. GbuSL(square) modifies the sequent calculus G3iSL(square) for iSL based on 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 s in GbuSL(square) fails, then a Kripke countermodel for s can be constructed.