Nested Sequent Calculi for Some Modal Logics with Non-Standard Modalities

Yaroslav Petrukhin

doi:10.12775/LLP.2025.009

Authors

Yaroslav Petrukhin Center for Philosophy of Nature, University of Lódź https://orcid.org/0000-0002-7731-1339

DOI:

https://doi.org/10.12775/LLP.2025.009

Keywords

nested sequent calculus, cut elimination, 4-valued modal logics, contingency logic, essence logic, accident logic, paraconsistent logic, paracomplete logic

Abstract

This paper introduces nested sequent calculi for modal logics that include non-standard modalities as primitive operators in their languages. By non-standard modalities, we mean non-contingency, contingency, essence, accident, impossibility, and unnecessity. We consider basic normal modal logic K and its serial, reflexive, transitive, and symmetric extensions. Our research begins by using Poggiolesi’s nested sequent calculi as a foundation. These calculi are specifically designed for logics that are formulated in a language that includes the necessity operator. Next, we proceed to modify their rules to accommodate non-standard modalities. We then establish the soundness and completeness of the resulting calculi. As a consequence, we get that the nested sequent calculus for K is cut-free. Subsequently, we provide a constructive cut admissibility proof for K. Finally, we discuss the issues pertaining to the cut admissibility for the extensions of K and their relationships with the so-called special structural rules as well as the potential for considering other forms of non-standard modalities.

References

Avron, A., and O. Lahav, “A simple cut-free system for a paraconsistent logic equivalent to S5”, pages 29–42 in G. Bezhanishvili, G. D’Agostino, G. Metcalfe and T. Studer (eds.), Advances in Modal Logic, vol. 12, College Publications, 2018.

Béziau, J. Y., “The paraconsistent logic Z. A possible solution to Jaśkowski’s problem”, Logic and Logical Philosophy 15, 2 (2006): 99–111. DOI: https://doi.org/10.12775/LLP.2006.006

Boolos, G., The Logic of Provability, Cambridge University Press, 1993. DOI: https://doi.org/10.1017/CBO9780511625183

Brünnler, K., “Deep sequent systems for modal logic”, pages 107–119 in G. Governatori, I. Hodkinson, and Y. Venema (eds.), Advances in Modal Logic, vol. 6, College Publications, London, 2006. DOI: https://doi.org/10.1007/s00153-009-0137-3

Brünnler, K., and L. Straßburger, “Modular sequent systems for modal logic”, pages 152–166 in M. Giese and A. Waaler (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX’09, LNCS 5607, 2009. DOI: https://doi.org/10.1007/978-3-642-02716-1_12

Coniglio, M. E., and L. Prieto-Sanabria, “Modal logic S4 as a paraconsistent logic with a topological semantics”, in C. Caleiro, F. Dionisio, P. Gouveia, P. Mateus and J. Rasga (eds.), Logic and Computation: Essays in Honour of Amilcar Sernadas, College Publications, 2017.

Dodó, A., and J. Marcos, “Negative modalities, consistency and determinedness”, Electronic Notes in Theoretical Computer Science, 300 (2014): 21–45. DOI: https://doi.org/10.1016/j.entcs.2013.12.010

Fan, J., Y. Wang and H. van Ditmarsch, “Almost necessary”, pages 178–196 in G. Bezhanishvili, G. D’Agostino, G. Metcalfe and T. Studer (eds.), Advances in Modal Logic, vol. 10, College Publications, 2014.

Fan, J., Y. Wang, and H. Ditmarsch, “Contingency and knowing whether”, The Review of Symbolic Logic 8, 1 (2015): 75–107. DOI: https://doi.org/10.1017/S1755020314000343

Fan, J., “Logics of essence and accident”, https://arxiv.org/abs/1506.01872, accessed on 21.04.2025 (2015).

Fan, J., “Bimodal logics with contingency and accident”, Journal of Philosophical Logic 48, 2 (2019): 425–445. DOI: https://doi.org/10.1007/s10992-018-9470-5

Fan, J., “Bimodal logic with contingency and accident: bisimulation and axiomatizations”, Logica Universalis 15, 2 (2021): 123–147. DOI: https://doi.org/10.1007/s11787-021-00270-9

Fitting, M. “Prefixed tableaus and nested sequents”, Annals of Pure and Applied Logic 163, 3 (2012): 291–313. DOI: https://doi.org/10.1016/j.apal.2011.09.004

Gilbert, D. R. and G. Venturi, “A note on logics of essence and accident”, Logic Journal of the IGPL 28, 5 (2020): 881–891. DOI: https://doi.org/10.1093/jigpal/jzy065

Humberstone, L., “The logic of noncontingency”, Notre Dame Journal of Formal Logic 36, 2 (1995): 214–229. DOI: https://doi.org/10.1305/ndjfl/1040248455

Jaskowski, S., “A propositional calculus for inconsistent deductive systems”, Logic and Logical Philosophy, 7 (1999): 35–56. English translation of paper by 1948. DOI: https://doi.org/10.12775/LLP.1999.003

Kashima, R., “Cut-free sequent calculi for some tense logics”, Studia Logica, 53 (1994): 119–135. DOI: https://doi.org/10.1007/BF01053026

Kuhn, S., “Minimal non-contingency logic”, Notre Dame Journal of Formal Logic 36, 2 (1995): 230–234. DOI: https://doi.org/10.1305/ndjfl/1040248456

Lahav, O., J. Marcos and Y.Zohar, “Sequent systems for negative modalities”, Logica Universalis 11, 3 (2017): 345–382. DOI: https://doi.org/10.1007/s11787-017-0175-2

Liu, F., J. Seligman and P. Girard, “Logical dynamics of belief change in the community”, Synthese 191, 11 (2014): 2403–2431. DOI: https://doi.org/10.1007/s11229-014-0432-3

Lyon, T. S., and E. Orlandelli, “Nested sequents for quantified modal logics”, pages 449–467 in R. Ramanayake and J. Urban(eds.), Automated Reasoning with Analytic Tableaux and Related Methods, 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Springer. DOI: https://doi.org/10.1007/978-3-031-43513-3_24

Marcos, J., “Nearly every normal modal logic is paranormal”, Logique et Analyse, 48, 189–192 (2005): 279–300.

Marcos, J., “Logics of essence and accident”, Bulletin of the Section of Logic, 34, 1 (2005): 43–56.

Marin, S., and L. Straßburger, “Label-free modular systems for classical and intuitionistic modal logics”, pages 387–406 in R. Goré, B. Kooi and A. Kurucz (eds.), Advances in Modal Logic, vol. 10, College Publications, 2014.

Mruczek-Nasieniewska, K., and M. Nasieniewski, “Syntactical and semantical characterization of a class of paraconsistent logics”, Bulletin of the Section of Logic, 34, 4 (2005): 229–248.

Montgomery, H., and R. Routley, “Contingency and noncontingency bases for normal modal logics”, Logique et Analyse, 9 (1966): 318–328.

Montgomery, H., and R. Routley, “Noncontingency axioms for S4 and S5”, Logique et Analyse, 11 (1968): 422–424.

Montgomery, H., and R. Routley, “Modalities in a sequence of normal noncontingency modal systems”, Logique et Analyse, 12 (1969): 225–227.

Negri, S., and J. von Plato, “Meaning in use”, pages 239–257 in H. Wansing (ed.), Dag Prawitz on Proofs and Meaning, Outstanding Contributions to Logic, vol. 7, Springer, Cham, 2015. DOI: https://doi.org/10.1007/978-3-319-11041-7_10

[30] Omori, H., and T. Waragai, T., “On Béziau’s logic Z”, Logic and Logical Philosophy, 17, 4 (2008): 305–320. DOI: https://doi.org/10.12775/LLP.2008.017

Pan, T., and C. Yang, C., “A logic for weak essence and srtong accident”, Logique et Analyse, 60 (2017): 179–190. DOI: https://doi.org/10.2143/LEA.238.0.3212072

[32] Petrukhin, Y., “S5-style non-standard modalities in a hypersequent framework”, Logic and Logical Philosophy, 31, 3 (2022): 427–456. DOI: https://doi.org/10.12775/LLP.2021.020

Petrukhin, Y., “Proof systems for some many-valued and modal logics”, PhD thesis, University of Łódź, 2024. https://www.bip.uni.lodz.pl/fileadmin/user_upload/ROZPRAWA_DOKTORSKA_J._Petrukhin.pdf

Poggiolesi, F., Gentzen Calculi for Modal Propositional Logic, Springer, 2011. DOI: https://doi.org/10.1007/978-90-481-9670-8

Poggiolesi, F., “The method of tree-hypersequents for modal propositional logic”, pages 31–51 in D. Makinson, J. Malinowski and H. Wansing (eds.), Towards Mathematical Philosophy, Trends in Logic, vol. 28, Springer, Dordrecht, 2009. DOI: https://doi.org/10.1007/978-1-4020-9084-4_3

Restall, G., “Proofnets for S5: sequents and circuits for modal logic”, pages 151–172 in C. Dimitracopoulos, L. Newelski, D. Normann and J. R. Steel (eds.) Logic Colloquium 2005, Cambridge University Press, 2007. DOI: https://doi.org/10.1017/CBO9780511546464.012

Savateev, Y., and D. Shamkanov, “Non-well-founded proofs for the Grzegorczyk modal logic”, The Review of Symbolic Logic, 14, 1 (2021): 22–50. DOI: https://doi.org/10.1017/S1755020319000510

Steinsvold, C., “Completeness for various logics of essence and accident”, Bulletin of the Section of Logic 37, 2 (2008): 93–101.

Steinsvold, C., “A note on logics of ignorance and borders”, Notre Dame Journal of Formal Logic 49, 4 (2008): 385–392. DOI: https://doi.org/10.1215/00294527-2008-018

Steinsvold, C., “The boxdot conjecture and the language of essence and accident”, Australasian Journal of Logic, 10 (2011): 18–35. DOI: https://doi.org/10.26686/ajl.v10i0.1822

Takano, M., “A modified subformula property for the modal logics K5 and K5D”, Bulletin of the Section of Logic, 30, 2 (2001): 115–122.

van der Hoek, W., and A. Lomuscio, “A logic for ignorance”, Electronic Notes in Theoretical Computer Science, 85, 2 (2004): 117–133. DOI: https://doi.org/10.1007/978-3-540-25932-9_6

Venturi, G., and P. T. Yago, “Tableaux for essence and contingency”, Logic Journal of IGPL 29, 5 (2021): 719–738. DOI: https://doi.org/10.1093/jigpal/jzaa016

von Wright, G. H., “Deontic logic”, Mind, 60 (1951): 1–15. DOI: https://doi.org/10.1093/mind/LX.237.1

Zolin, E., “Sequential reflexive logics with noncontingency operator”, Mathematical Notes, 72, 5–6 (2002): 784–798. DOI: https://doi.org/10.1023/A:1021485712270

Zolin, E., “Sequential logic of arithmetical noncontingency”, Moscow University Mathematical Bulletin, 56 (2001): 43–48.

Zolin, E., “Modal logics with decidability operator” (in Russian), PhD thesis, 2002.

Zolin, E., “Completeness and definability in the logic of noncontingency”, Notre Dame Journal of Formal Logic 40, 4 (1999): 533–547. DOI: https://doi.org/10.1305/ndjfl/1012429717