Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics

Eugenio Orlandelli



G3-style sequent calculi for the logics in the cube of non-normal modal logics and for their deontic extensions are studied. For each calculus we prove that weakening and contraction are height-preserving admissible, and we give a syntactic proof of the admissibility of cut. This implies that the subformula property holds and that derivability can be decided by a terminating proof search whose complexity is in Pspace. These calculi are shown to be equivalent to the axiomatic ones and, therefore, they are sound and complete with respect to neighbourhood semantics. Finally, a Maehara-style proof of Craig’s interpolation theorem for most of the logics considered is given.


non-normal logics; deontic logics; sequent calculi; structural proof theory; interpolation; decidability

Full Text:



Basin, D., S. Matthews and L. Viganò, “A new method for bounding the complexity of modal logics”, pages 89–102 in G. Gottlob et al. (eds.), Computational Logic and Proof Theory (KGC 1997), Berlin: Springer, 1997. DOI:

Bilková, M., “Uniform interpolation and propositional quantifiers in modal logics”, Studia Logica 85 (2007): 1–31. DOI:

Calardo, E., A. Rotolo, “Variants of multi-relational semantics for propositional non-normal modal logics”, Journal of Applied Non-Classical Logics 24 (2014): 293–320. DOI:

Chellas, B.F., Modal Logic: An Introduction, Cambridge: CUP, 1980. DOI:

Chen, J., G. Greco, A. Palmigiano and A. Tzimoulis, “Non normal logics: semantic analysis and proof theory”, pages 99–118 in R. Iemhoff et al. (eds.), Logic, Language, Information, and Computation (WOLLIC 2019), Berlin: Springer, 2019. DOI:

Dalmonte, T., N. Olivetti and S. Negri, “Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi”, pages 159–178 in G. Bezanishvili et al. (eds.), Advances in Modal Logic 12, London: College Publications, 2018.

Dalmonte, T., B. Lellmann, N. Olivetti and E. Pimentel, “Countermodel construction via optimal hypersequent calculi for non-normal modal logics”, pages 27–46 in S. Artemov and A. Nerode (eds.), Logical Foundations of Computer Science 2020, Berlin: Springer, 2020. DOI:

Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Dordrecht: Reidel, 1983. DOI:

Forrester, J.W., “Gentle murder, or the adverbial samaritan”, Journal of Philosophy 81 (1984): 193-197. DOI:

Gabbay, D. M., and L. Maksimova, Interpolation and Definability: Modal and Intuitionistic Logics, Oxford: Clarendon, 2005. DOI:

Gilbert, D., and P. Maffezioli, “Modular sequent calculi for classical modal logics”, Studia Logica 103 (2015): 175–217. DOI:

Girlando, M., B. Lellmann, N. Olivetti and G. L. Pozzato, “Standard sequent calculi for Lewis’ logics of counterfactuals”, pages 272–287 in L. Michael and A. Kakas (ed.), JELIA 2016, Cham: Springer, 2016. DOI:

Goble, L., “Prima facie norms, normative conflicts, and dilemmas”, pages 241–351 in D. Gabbay et al. (eds.), Handbook of Deontic Logic and Normative Systems, London: College Publications, 2013.

Halldén, S., “On the semantic non-completeness of certain Lewis calculi”, Journal of Symbolic Logic 16 (1951): 127–129. DOI:

Hansen H.H., C. Kupke and E. Pacuit, “Neighborhood structures: bisimilarity and basic model theory”, Logical Methods in Computer Science 5 (2009): 1–38. DOI:

Hilpinen, R., and P. McNamara, “Deontic logic: a historical survey and introduction”, pages 3–136 in D.M. Gabbay et al. (eds.), Handbook of Deontic Logic and Normative Systems, London: College Publications, 2013.

Hudelmaier, J., “An O(n log n)-space decision procedure for intuitionistic propositional logic”, Journal of Logic and Computation 3 (1993): 63–76. DOI:

Hudelmaier, J., “Improved decision procedures for the modal logics K, T and S4”, pages 320–334 in H. Kleine Büning, Computer Science Logic (CSL 1995), Berlin: Springer, 1995. DOI:

Indrzejczak, A., “Sequent calculi for monotonic modal logics”, Bullettin of the Section of Logic 34 (2005): 151–164.

Indrzejczak, A., “Admissiblity of cut in congruent modal logics”, Logic and Logical Philosophy 21 (2011): 189–203. DOI:

Lavendhomme, R., and L. Lucas, “Sequent calculi and decision procedures for weak modal systems”, Studia Logica 65 (2000): 121–145. DOI:

Lellmann, B., and E. Pimentel, “Modularization of sequent calculi for normal and non-normal modalities”, ACM Transactions on Computational Logic, 20, (2019): 1–46. DOI:

Ma, M., and J. Chen, “Sequent calculi for global modal consequence relations”, Studia Logica 107 (2019): 613–637. DOI:

Maehara, S., “On the interpolation theorem of Craig” (Japanese), Sugaku 12 (1960): 235–237.

Maehara, S., and G. Takeuti, “A formal system of first-order predicate calculus with infinitely long expressions”, Journal of the Mathematical Society of Japan 13 (1961): 357–370. DOI:

Negri, S., “Proof theory for non-normal modal logics: the neighbourhood formalism and basic results”, IfCoLog Journal of Logics and their Applications 4 (2017): 1241–1286.

Negri, S., and R. Hakli, “Does the deduction theorem fail for modal logic?”, Synthese 184 (2012): 849-867. DOI:

Negri, S., and E. Orlandelli, “Proof theory for quantified monotone modal logics”, Logic Journal of the IGPL 27 (2019): 478–506. DOI:

Negri, S., and J. von Plato, Structural Proof Theory, Cambridge: CUP, 2001. DOI:

Negri, S., and J. von Plato, Proof Analysis, Cambridge: CUP, 2011. 10.1017/CBO9781139003513

Orlandelli, E., “Proof analysis in deontic logics”, pages 139–148 in F. Cariani et al. (eds.), Deontic Logic and Normative Systems (DEON 2014), Berlin: Springer, 2015. DOI:

Orlandelli, E., and G. Corsi, “Decidable term-modal logics”, pages 147–162 in F. Belardinelli and E. Argente (eds.), EUMAS 2017/AT 2017, Berlin: Springer, 2018. DOI:

Pacuit, E., Neighbourhood Semantics for Modal Logic, Berlin: Springer, 2017. DOI:

Pattinson, D., “The logic of exact covers: completeness and uniform interpolation”, pages 418–427 in LICS 2013, IEEE Computer Society, 2013. DOI:

Pattinson, D., and L. Schröder, “Cut elimination in coalgebraic logics”, Information and Computation 208 (2010): 1447–1468. DOI:

Pitts, A. J., “On an interpretation of second order quantification in first order intuitionistic propositional logic”, Journal of Symbolic Logic 57 (1992): 33–52. DOI:

Schröder, L., and D. Pattinson, “PSPACE bounds for rank-1 modal logics”, ACM Transactions in Computational Logics 10 (2009): 1–33. DOI:

van der Torre, L., Reasoning about Obligations, Amsterdam: Tinbergen Institute Research Series, 1997.

Troelstra, A.S., and H. Schwichtenberg, Basic Proof Theory, Cambridge: CUP, 2000 2 . DOI:

Valentini, S., “The sequent calculus for the modal logic D”, Bollettino dell’Unione Matematica Italiana 7 (1993): 455–460.

Vardi, M.Y., “On the complexity of epistemic reasoning”, pages 243–252 in Proceedings of the Fourth Annual Symposium on Logic in Computer Science, IEEE Press, 1989. DOI:

Vardi, M.Y., “On the complexity of epistemic reasoning”, pages 243–252 in Proceedings of the Fourth Annual Symposium on Logic in Computer Science, IEEE Press, 1989. DOI:

ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism