A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised

Ian Shillito, Iris van der Giessen, Rajeev Goré +1

We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic $\mathsf{iSL}$, an intuit…