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

Eugenio Orlandelli

DOI: http://dx.doi.org/10.12775/LLP.2020.018

Abstract


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.

Keywords


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

Full Text:

PDF

References


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: http://dx.doi.org/10.1007/3-540-63385-5_35

Bilková, M., “Uniform interpolation and propositional quantifiers in modal logics”, Studia Logica 85 (2007): 1–31. DOI: http://dx.doi.org/10.1007/s11225-007-9021-5

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: http://dx.doi.org/10.1080/11663081.2014.966625

Chellas, B.F., Modal Logic: An Introduction, Cambridge: CUP, 1980. DOI: http://dx.doi.org/10.1017/CBO9780511621192

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: http://dx.doi.org/10.1007/978-3-662-59533-6_7

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. http://www.aiml.net/volumes/volume12/Dalmonte-Olivetti-Negri.pdf

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: http://dx.doi.org/10.1007/978-3-030-36755-8_3

Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Dordrecht: Reidel, 1983. DOI: http://dx.doi.org/10.1007/978-94-017-2794-5

Forrester, J.W., “Gentle murder, or the adverbial samaritan”, Journal of Philosophy 81 (1984): 193-197. DOI: http://dx.doi.org/10.2307/2026120

Gabbay, D. M., and L. Maksimova, Interpolation and Definability: Modal and Intuitionistic Logics, Oxford: Clarendon, 2005. DOI: http://dx.doi.org/10.1093/acprof:oso/9780198511748.001.0001

Gilbert, D., and P. Maffezioli, “Modular sequent calculi for classical modal logics”, Studia Logica 103 (2015): 175–217. DOI: http://dx.doi.org/10.1007/s11225-014-9556-1

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: http://dx.doi.org/10.1007/978-3-319-48758-8_18

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. http://www.collegepublications.co.uk/downloads/handbooks00001.pdf

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

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: http://dx.doi.org/10.2168/LMCS-5(2:2)2009

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. http://www.collegepublications.co.uk/downloads/handbooks00001.pdf

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

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: http://dx.doi.org/10.1007/3-540-61377-3_46

Indrzejczak, A., “Sequent calculi for monotonic modal logics”, Bullettin of the Section of Logic 34 (2005): 151–164. http://www.filozof.uni.lodz.pl/bulletin/pdf/34_3_4.pdf

Indrzejczak, A., “Admissiblity of cut in congruent modal logics”, Logic and Logical Philosophy 21 (2011): 189–203. DOI: http://dx.doi.org/10.12775/LLP.2011.010

Lavendhomme, R., and L. Lucas, “Sequent calculi and decision procedures for weak modal systems”, Studia Logica 65 (2000): 121–145. DOI: http://dx.doi.org/10.1023/A:1026753129680

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: http://dx.doi.org/10.1145/3288757

Ma, M., and J. Chen, “Sequent calculi for global modal consequence relations”, Studia Logica 107 (2019): 613–637. DOI: http://dx.doi.org/10.1007/s11225-018-9806-8

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: http://dx.doi.org/10.2969/jmsj/01340357

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. http://www.collegepublications.co.uk/downloads/ifcolog00013.pdf

Negri, S., and R. Hakli, “Does the deduction theorem fail for modal logic?”, Synthese 184 (2012): 849-867. DOI: http://dx.doi.org/10.1007/s11229-011-9905-9

Negri, S., and E. Orlandelli, “Proof theory for quantified monotone modal logics”, Logic Journal of the IGPL 27 (2019): 478–506. DOI: http://dx.doi.org/10.1093/jigpal/jzz015

Negri, S., and J. von Plato, Structural Proof Theory, Cambridge: CUP, 2001. DOI: http://dx.doi.org/10.1017/CBO9780511527340

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: http://dx.doi.org/10.1007/978-3-319-08615-6_11

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: http://dx.doi.org/10.1007/978-3-030-01713-2_11

Pacuit, E., Neighbourhood Semantics for Modal Logic, Berlin: Springer, 2017. DOI: http://dx.doi.org/10.1007/978-3-319-67149-9

Pattinson, D., “The logic of exact covers: completeness and uniform interpolation”, pages 418–427 in LICS 2013, IEEE Computer Society, 2013. DOI: http://dx.doi.org/10.1109/LICS.2013.48

Pattinson, D., and L. Schröder, “Cut elimination in coalgebraic logics”, Information and Computation 208 (2010): 1447–1468. DOI: http://dx.doi.org/10.1016/j.ic.2009.11.008

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: http://dx.doi.org/10.2307/2275175

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

van der Torre, L., Reasoning about Obligations, Amsterdam: Tinbergen Institute Research Series, 1997. https://icr.uni.lu/leonvandertorre/papers/thesis.pdf

Troelstra, A.S., and H. Schwichtenberg, Basic Proof Theory, Cambridge: CUP, 2000 2 . DOI: http://dx.doi.org/10.1017/CBO9781139168717

Valentini, S., “The sequent calculus for the modal logic D”, Bollettino dell’Unione Matematica Italiana 7 (1993): 455–460. https://www.math.unipd.it/~silvio/papers/ModalLogic/DModalLogic.pdf

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: http://dx.doi.org/10.1109/LICS.1989.39179

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: http://dx.doi.org/10.1109/LICS.1989.39179








ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism