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 Author 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 Author 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 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.

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

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

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 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 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 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 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 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.

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

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 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

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 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 DOI: https://doi.org/10.1017/CBO9781139168717