From Translations to Non-Collapsing Logic Combinations

João Rasga; Cristina Sernadas

doi:10.18778/0138-0680.2025.14

Authors

João Rasga Universidade de Lisboa, Instituto Superior Técnico, Dep. Matemática https://orcid.org/0000-0002-1239-8496
Cristina Sernadas 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.2025.14

Keywords:

non-collapsing combination of logics, conservative translation, conservativeness of the combination, Gentzen calculus

Abstract

Prawitz suggested expanding a natural deduction system for intuitionistic logic to include rules for classical logic constructors, allowing both intuitionistic and classical elements to coexist without losing their inherent characteristics. Looking at the added rules from the point of view of the Gödel-Gentzen translation, led us to propose a general method for the coexistent combination of two logics when a conservative translation exists from one logic (the source) to another (the host). Then we prove that the combined logic is a conservative extension of the original logics, thereby preserving the unique characteristics of each component logic. In this way there is no collapse of one logic into the other in the combination. We also demonstrate that a Gentzen calculus for the combined logic can be induced from a Gentzen calculus for the host logic by considering the translation. This approach applies to semantics as well. We then establish a general sufficient condition for ensuring that the combined logic is both sound and complete. We apply these principles by combining classical and intuitionistic logics capitalizing on the Gödel-Gentzen conservative translation, intuitionistic and S4 modal logics relying on the Gödel-McKinsey-Tarski conservative translation, and classical and Jaśkowski’s paraconsistent logics taking into account the existence of a conservative translation.

References

A. Avron, Classical Gentzen-type methods in propositional many-valued logics, [in:] Beyond Two: Theory and Applications of Multiple-valued Logic, Physica (2003), pp. 117–155, DOI: https://doi.org/10.1109/ISMVL.2001.924586
Google Scholar DOI: https://doi.org/10.1007/978-3-7908-1769-0_5

P. Blackburn, J. F. A. K. v. Benthem, Modal logic: A semantic perspective, [in:] P. Blackburn, J. F. A. K. v. Benthem, F. Wolter (eds.), Handbook of Modal Logic, Elsevier (2006), pp. 173–204.
Google Scholar

W. J. Blok, D. Pigozzi, Abstract Algebraic Logic and the Deduction Theorem, Tech. rep., Iowa State University (2001), available at https://faculty.sites.iastate.edu/dpigozzi/files/inline-files/aaldedth.pdf
Google Scholar

C. Caleiro, J. Ramos, From fibring to cryptofibring. A solution to the collapsing problem, Logica Universalis, vol. 1(1) (2007), pp. 71–92, DOI: https://doi.org/10.1007/s11787-006-0004-5
Google Scholar DOI: https://doi.org/10.1007/s11787-006-0004-5

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

S. Demri, R. Goré, An O((n·logn)3)-time transformation from Grz into decidable fragments of classical first-order logic, [in:] Automated Deduction in Classical and Non-classical Logics, vol. 1761 of Lecture Notes in Computer Science, Springer (2000), pp. 152–166, DOI: https://doi.org/10.1007/3-540-46508-1_10
Google Scholar DOI: https://doi.org/10.1007/3-540-46508-1_10

R. Diaconescu, Institution-independent Model Theory, Studies in Universal Logic, Birkhäuser (2008), DOI: https://doi.org/10.1007/978-3-7643-8708-2
Google Scholar DOI: https://doi.org/10.1007/978-3-7643-8708-2

I. M. L. D’Ottaviano, The completeness and compactness of a three-valued first-order logic, Revista Colombiana de Matemáticas, vol. 19(1-2) (1985), pp. 77–94.
Google Scholar

I. M. L. D’Ottaviano, N. C. A. da Costa, Sur un problème de Jaśkowski,Comptes Rendus Hebdomadaires des Séances de l’Académie des Sciences. Séries A et B, vol. 270 (1970), pp. A1349–A1353.
Google Scholar

I. M. L. D’Ottaviano, H. A. Feitosa, Paraconsistent logics and translations, Synthese, vol. 125(1-2) (2000), pp. 77–95, DOI: https://doi.org/10.1023/A:1005298624839
Google Scholar DOI: https://doi.org/10.1023/A:1005298624839

M. Dummett, The Logical Basis of Metaphysics, Harvard University Press (1991).
Google Scholar

J. L. Fiadeiro, A. Sernadas, Structuring theories on consequence, [in:] ADT 1987: Recent Trends in Data Type Specification, vol. 332 of Lecture Notes in Computer Science, Springer (1987), pp. 44–72, DOI: https://doi.org/10.1007/3-540-50325-0_3
Google Scholar DOI: https://doi.org/10.1007/3-540-50325-0_3

D. M. Gabbay, An overview of fibred semantics and the combination of logics, [in:] Frontiers of Combining Systems, vol. 3, Kluwer (1996), pp. 1–55, DOI: https://doi.org/10.1007/978-94-009-0349-4_1
Google Scholar DOI: https://doi.org/10.1007/978-94-009-0349-4_1

G. Gentzen, The Collected Papers of Gerhard Gentzen, North-Holland (1969).
Google Scholar

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

J. A. Goguen, R. M. Burstall, Introducing institutions, [in:] Logics of Programs, vol. 164 of Lecture Notes in Computer Science, Springer (1984), pp. 221–256, DOI: https://doi.org/10.1007/3-540-12896-4_366
Google Scholar DOI: https://doi.org/10.1007/3-540-12896-4_366

J. A. Goguen, R. M. Burstall, Institutions: Abstract model theory for specification and programming, Journal of the Association for Computing Machinery, vol. 39(1) (1992), pp. 95–146, DOI: https://doi.org/10.1145/147508.147524
Google Scholar DOI: https://doi.org/10.1145/147508.147524

P. T. Johnstone, Stone Spaces, vol. 3 of Cambridge Studies in Advanced Mathematics, Cambridge University Press (1986), reprint of the 1982 edition.
Google Scholar

M. Kracht, F. Wolter, Properties of independently axiomatizable bimodal logics, The Journal of Symbolic Logic, vol. 56(4) (1991), pp. 1469–1485, DOI: https://doi.org/10.2307/2275487
Google Scholar DOI: https://doi.org/10.2307/2275487

P. H. Krauss, A constructive refinement of classical logic, [in:] Mathematische Schriften Kassel (1992), preprint 5.
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 DOI: https://doi.org/10.2307/2268135

J. Meseguer, General logics, [in:] Logic Colloquium, vol. 129, North-Holland (1989), pp. 275–329, DOI: https://doi.org/10.1016/S0049-237X(08)70132-0
Google Scholar DOI: https://doi.org/10.1016/S0049-237X(08)70132-0

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

K. R. Popper, On the theory of deduction II, Indagationes Math., vol. 10 (1948), pp. 111–120, DOI: https://doi.org/10.1007/978-3-030-94926-6_6
Google Scholar DOI: https://doi.org/10.1007/978-3-030-94926-6_6

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

W. V. Quine, Philosophy of Logic, Foundations of Philosophy Series, Prentice-Hall (1970), sixth printing.
Google Scholar

J. Ramos, J. Rasga, C. Sernadas, Conservative translations revisited, Journal of Philosophical Logic, vol. 52(3) (2023), pp. 889–913, DOI: https://doi.org/10.1007/s10992-022-09691-3
Google Scholar DOI: https://doi.org/10.1007/s10992-022-09691-3

J. Rasga, C. Sernadas, On combining intuitionistic and S4 modal logic, Bulletin of the Section of Logic, vol. 53(3) (2024), pp. 321–344, DOI: https://doi.org/10.18778/0138-0680.2024.11
Google Scholar DOI: https://doi.org/10.18778/0138-0680.2024.11

J. Rasga, C. Sernadas, W. A. Carnielli, Reduction techniques for proving decidability in logics and their meet-combination, The Bulletin of Symbolic Logic, vol. 27(1) (2021), pp. 39–66, DOI: https://doi.org/10.1017/bsl.2021.17
Google Scholar DOI: https://doi.org/10.1017/bsl.2021.17

V. Rybakov, Admissibility of Logical Inference Rules, North-Holland (1997).
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

S. K. Thomason, Independent propositional modal logics, Studia Logica, vol. 39(2-3) (1980), pp. 143–144, DOI: https://doi.org/10.1007/BF00370317
Google Scholar DOI: https://doi.org/10.1007/BF00370317

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

G. Voutsadakis, Categorical abstract algebraic logic: models of π-institutions, Notre Dame Journal of Formal Logic, vol. 46(4) (2005), pp. 439–460, DOI: https://doi.org/10.1305/ndjfl/1134397662
Google Scholar DOI: https://doi.org/10.1305/ndjfl/1134397662