Sequent Calculi for Multi-modal Logic with Interaction

Gratzl, Norbert (2013): Sequent Calculi for Multi-modal Logic with Interaction. In: Grossi, Davide; Roy, Olivier and Huang, Huaxin (eds.) : Logic, Rationality, and Interaction. Lecture Notes in Computer Science, Vol. 8196. Berlin, Heidelberg: Springer Berlin Heidelberg. pp. 124-134

Abstract

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.

• Item Type: Book Section
• Faculties: Philosophy, Philosophy of Science and Religious Science > Munich Center for Mathematical Philosophy (MCMP); Philosophy, Philosophy of Science and Religious Science > Munich Center for Mathematical Philosophy (MCMP) > Logic
• Subjects: 100 Philosophy and Psychology > 160 Logic
• ISBN: 978-3-642-40947-9
• ISSN: 0302-9743
• Place of Publication: Berlin, Heidelberg
• Language: English