Countermodels from Sequent Calculi in Multi-Modal Logics

A novel countermodel-producing decision procedure that applies to several multi-modal logics, both intuitionistic and classical, is presented. Based on backwards search in labeled sequent calculi, the procedure employs a novel termination condition and countermodel construction. Using the procedure, it is argued that multi-modal variants of several classical and intuitionistic logics including K, T, K4, S4 and their combinations with D are decidable and have the finite model property. At least in the intuitionistic multi-modal case, the decidability results are new. It is further shown that the countermodels produced by the procedure, starting from a set of hypotheses and no goals, characterize the atomic formulas provable from the hypotheses.