Terminating sequent calculi for two intuitionistic modal logics
Rosalie Iemhoff · Journal of Logic and Computation · 2018
This paper presents sequent calculi in which proof search is terminating for two intuitionistic modal logics, the intuitionistic versions of the classical modal logics K and KD without a diamond operator. The calculi are extensions of the terminating sequent calculus |${\textsf{G4ip}}$| for intuitionistic propositional logic that was discovered independently by Dyckhoff and Hudelmaier around 1990. It is shown by proof-theoretic means that these terminating calculi are equivalent to the cutfree extensions of |${\textsf{G3ip}}$| that form some of the standard calculi for intuitionistic modal logics.