DeutschClear Cookie - decide language by browser settings
Gratzl, Norbert (2013): Sequent Calculi for Multi-modal Logic with Interaction. In: Grossi, Davide; Roy, Olivier; Huang, Huaxin (eds.) : Logic, Rationality, and Interaction. Lecture Notes in Computer Science, Vol. 8196. Berlin, Heidelberg: Springer Berlin Heidelberg. pp. 124-134
Full text not available from 'Open Access LMU'.


This paper studies Gentzen-style sequent calculi for multi-modal logics with interaction between the modalities. We prove cut elimination and some of its usual corollaries for two such logics: Standard Deontic Logic with the Ought-implies-Can principle, and a non-normal deontic logic where obligation, permissions and abilities interact in a complex way. The key insight of these results is to make rules sensitive to the shape of the formulas on either sides of the sequents. This way one can devise rules in a much more modular fashion. This feature of Hilbert-style systems is notoriously lost when one moves to sequent calculi. By partly restoring modularity the method proposed here can potentially provide a unified approach to the proof theory of multi-modal systems.