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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Avron, A.: Hypersequents, logical consequence and intermediate logics for concurrency. Annals of Mathematics and Artifical Intelligence 4, 225–248 (1991)
Avron, A.: The methods of hypersequents in the proof theory of propositional and non-classical logics. In: Hodges, W., Hyland, M. (eds.) Logic: from Foundations to Applications. Proc. Logic Colloquium, pp. 1–32. Oxford University Press (1993)
Baltag, A., Smets, S.: Conditioanl doxastic models: A qualitative approach to dynamic belief revision. In: Electornic Notes in Theoretical Computer Science, vol. 165, pp. 5–21. Springer (2006)
Brünnler, K., Lange, M.: Cut-free sequent systems for temporal logic. Journal of Logic and Algebraic Programming 76(2), 216–225 (2008)
Governatori, G., Rotolo, A.: Labelled modal sequents. In: TABLEAUX 2000. Position Papers and Tutorials, pp. 3–21 (2000)
Gratzl, N.: A note on hypersequent first order s5 (submitted)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic (Foundations of Computing). MIT Press (2000)
Hill, B., Poggiolesi, F.: A contraction-free and cut-free sequent calculus for propositional dynamic logic. Studia Logica 94(1), 47–72 (2010)
Lavendhomme, R., Lucas, T.: Sequent calculi and decision procedures for weak modal systems. Studia Logica, 121–145 (2000)
McNamara, P.: Deontic logic. In: E. N. Zalta, editor, Standford Encyclopedia of Philosophy. Spring edn. (2006), http://plato.stanford.edu/archives/spr2006/entries/logic-deontic/
Negri, S.: Proof analysis in modal logic. Journal of Philosophical Logic 34(5), 507–544 (2005)
Poggiolesi, F.: Gentzen Calculi for Modal Propositional Logic. Springer (2011)
Poggiolesi, F.: From single agent to multi-agent via hypersequents. Logica Universalis, 1–20 (2012)
Poggiolesi, F.: A cut-free simple sequent calculus for modal logic s5. Review of Symbolic Logic 1(1), 3–15 (2008)
Restall, G.: Proofnets for s5: sequents and circuits for modal logic. In: Logic Colloquium, vol. 28, pp. 151–172 (2005)
Roy, O., Anglberger, A.J.J., Gratzl, N.: The logic of obligation as weakest permission. In: Ågotnes, T., Broersen, J., Elgesem, D. (eds.) DEON 2012. LNCS, vol. 7393, pp. 139–150. Springer, Heidelberg (2012)
Roy, O., Anglberger, A., Gratzl, N.: The logic of best action from a deontic perspective. In: Baltag, A., Smets, S. (eds.) Johan F.A.K. van Benthem on Logical and Informational Dynamics (2013)
Sun, X.: Conditional ought, a game theoretical perspective. In: van Ditmarsch, H., Lang, J., Ju, S. (eds.) LORI 2011. LNCS, vol. 6953, pp. 356–369. Springer, Heidelberg (2011)
Van Benthem, J., Gerbrandy, J., Hoshi, T., Pacuit, E.: Merging frameworks for interaction. Journal of Philosophical Logic 38(5), 491–526 (2009)
van Benthem, J., Grossi, D., Liu, F.: Deontics = betterness + priority. In: Governatori, G., Sartor, G. (eds.) DEON 2010. LNCS (LNAI), vol. 6181, pp. 50–65. Springer, Heidelberg (2010)
Wansing, H.: Displaying modal logic. Kluwer Academic Publishers (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gratzl, N. (2013). Sequent Calculi for Multi-modal Logic with Interaction. In: Grossi, D., Roy, O., Huang, H. (eds) Logic, Rationality, and Interaction. LORI 2013. Lecture Notes in Computer Science, vol 8196. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40948-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-40948-6_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40947-9
Online ISBN: 978-3-642-40948-6
eBook Packages: Computer ScienceComputer Science (R0)