On Combining Intuitionistic and S4 Modal Logic

João Rasga; Cristina Sernadas

doi:10.18778/0138-0680.2024.11

Authors

João Rasga Instituto de Telecomunicações, Basic Sciences and Enabling Technologies Campus Universitário de Santiago; Universidade de Lisboa, Instituto Superior Técnico, Dep. Matemática https://orcid.org/0000-0002-1239-8496
Cristina Sernadas Instituto de Telecomunicações, Basic Sciences and Enabling Technologies Campus Universitário de Santiago; Universidade de Lisboa, Instituto Superior Técnico, Dep. Matemática https://orcid.org/0000-0002-5510-3512

DOI:

https://doi.org/10.18778/0138-0680.2024.11

Keywords:

combination of logics, intuitionistic logic, modal logic, cut elimination

Abstract

We address the problem of combining intuitionistic and S4 modal logic in a non-collapsing way inspired by the recent works in combining intuitionistic and classical logic. The combined language includes the shared constructors of both logics namely conjunction, disjunction and falsum as well as the intuitionistic implication, the classical implication and the necessity modality. We present a Gentzen calculus for the combined logic defined over a Gentzen calculus for the host S4 modal logic. The semantics is provided by Kripke structures. The calculus is proved to be sound and complete with respect to this semantics. We also show that the combined logic is a conservative extension of each component. Finally we establish that the Gentzen calculus for the combined logic enjoys cut elimination.

References

L. F. del Cerro, A. Herzig, Combining classical and intuitionistic logic, [in:] F. Baader, K. U. Schulz (eds.), Frontiers of Combining Systems, Springer (1996), pp. 93–102, DOI: https://doi.org/10.1007/978-94-009-0349-4_4
Google Scholar

G. Dowek, On the definition of the classical connectives and quantifiers, [in:] Why is this a Proof? Festschrift for Luiz Carlos Pereira, College Publications (2015), pp. 228–238.
Google Scholar

D. Gabbay, Fibred semantics and the weaving of logics: Modal and intuitionistic logics, The Journal of Symbolic Logic, vol. 61(4) (1996), pp. 1057–1120, DOI: https://doi.org/10.2307/2275807
Google Scholar

D. Gabbay, Fibring Logics, Oxford University Press, Oxford (1999), DOI: https://doi.org/10.1093/oso/9780198503811.001.0001
Google Scholar

J.-Y. Girard, On the unity of logic, Annals of Pure and Applied Logic, vol. 59(3) (1993), pp. 201–217, DOI: https://doi.org/10.1016/0168-0072(93)90093-S
Google Scholar

K. Gödel, Collected Works. Vol. I, Oxford University Press (1986).
Google Scholar

S. Marin, L. C. Pereira, E. Pimentel, E. Sales, A pure view of ecumenical modalities, [in:] Logic, Language, Information, and Computation, vol. 13038 of Lecture Notes in Computer Science, Springer (2021), pp. 388– 407, DOI: https://doi.org/10.1007/978-3-030-88853-4_24
Google Scholar

J. C. C. McKinsey, A. Tarski, Some theorems about the sentential calculi of Lewis and Heyting, The Journal of Symbolic Logic, vol. 13 (1948), pp. 1–15, DOI: https://doi.org/10.2307/2268135
Google Scholar

S. Negri, J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge (2001), DOI: https://doi.org/10.1017/CBO9780511527340
Google Scholar

L. C. Pereira, R. O. Rodriguez, Normalization, Soundness and Completeness for the Propositional Fragment of Prawitz’ Ecumenical System, Revista Portuguesa de Filosofia, vol. 73(3/4) (2017), pp. 1153–1168, DOI: https://doi.org/10.17990/RPF/2017_73_3_1153
Google Scholar

E. Pimentel, L. C. Pereira, V. de Paiva, An ecumenical notion of entailment, Synthese, vol. 198(suppl. 22) (2021), pp. S5391–S5413, DOI: https://doi.org/10.1007/s11229-019-02226-5
Google Scholar

D. Prawitz, Classical versus intuitionistic logic, [in:] Why is this a Proof? Festschrift for Luiz Carlos Pereira, College Publications (2015), pp. 15–32.
Google Scholar

D. Prawitz, P.-E. Malmn¨as, A survey of some connections between classical, intuitionistic and minimal logic, [in:] Contributions to Mathematical Logic Colloquium, North-Holland, Amsterdam (1968), pp. 215–229, DOI: https://doi.org/10.1016/S0049-237X(08)70527-5
Google Scholar

J. Rasga, C. Sernadas, Decidability of Logical Theories and their Combination, Birkh¨auser, Basel (2020), DOI: https://doi.org/10.1007/978-3-030-56554-1
Google Scholar

V. Rybakov, Admissibility of Logical Inference Rules, North-Holland, Amsterdam (1997), URL: https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/136/suppl/C
Google Scholar

C. Sernadas, J. Rasga, W. A. Carnielli, Modulated fibring and the collapsing problem, The Journal of Symbolic Logic, vol. 67(4) (2002), pp. 1541–1569, DOI: https://doi.org/10.2178/jsl/1190150298
Google Scholar

A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, Cambridge (2000), DOI: https://doi.org/10.1017/CBO9781139168717
Google Scholar