On combining intuitionistic and S4 modal logic

João Rasga; Cristina Sernadas

doi:10.18778/0138-0680.2024.11

Authors

João Rasga Universidade de Lisboa, Instituto Superior Técnico, Departamento de Matemática and Instituto de Telecomunicações https://orcid.org/0000-0002-1239-8496
Cristina Sernadas Dep Matemática, IST ULisboa 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 DOI: https://doi.org/10.1007/978-94-009-0349-4_4

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 DOI: https://doi.org/10.2307/2275807

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

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 DOI: https://doi.org/10.1016/0168-0072(93)90093-S

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 DOI: https://doi.org/10.1007/978-3-030-88853-4_24

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 DOI: https://doi.org/10.2307/2268135

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

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 DOI: https://doi.org/10.17990/RPF/2017_73_3_1153

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 DOI: https://doi.org/10.1007/s11229-019-02226-5

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äs, 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 DOI: https://doi.org/10.1016/S0049-237X(08)70527-5

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

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 DOI: https://doi.org/10.2178/jsl/1190150298

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