Proof Theory for Intuitionistic Strong Löb Logic

Abstract

This paper introduces two sequent calculi for intuitionistic strong Löb logic iSL□: a terminating sequent calculus G4iSL□ based on the terminating sequent calculus G4ip for intuitionistic propositional logic IPC and an extension G3iSL□ of the standard cut-free sequent calculus G3ip without structural rules for IPC. One of the main results is a syntactic proof of the cut-elimination theorem for G3iSL□. In addition, equivalences between the sequent calculi and Hilbert systems for iSL□ are established. It is known from the literature that iSL□ is complete with respect to the class of intuitionistic modal Kripke models in which the modal relation is transitive, conversely well-founded and a subset of the intuitionistic relation. Here a constructive proof of this fact is obtained by using a countermodel construction based on a variant of G4iSL□. The paper thus contains two proofs of cut-elimination, a semantic and a syntactic proof.