Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics
DOI:
https://doi.org/10.12775/LLP.2020.018Keywords
non-normal logics, deontic logics, sequent calculi, structural proof theory, interpolation, decidabilityAbstract
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.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
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 813
Number of citations: 0
