From translations to non-collapsing logic combinations

TL;DR

The paper develops a universal method for the noncollapsing coexistence of two logics linked by a conservative translation. It constructs a Gentzen calculus for the coexistent logic by enriching the host calculus with translation-driven rules for the noncommon constructors and provides semantic frameworks that ensure the combined system is a conservative extension of each component. Under mild conditions, the authors prove soundness and completeness of the coexistent logic, with the host logic guiding derivations via a formula translation $\tau_{\sqcup}$. They illustrate the approach through classical/intuitionistic, Gödel-McKinsey-Tarski, and Jaśkowski paraconsistent combinations, showing that conservativity and extensivity hold and that no collapse occurs. The work lays groundwork for further preservation results, including cut elimination, interpolation, and decision problems, across broader families of logics and translations.

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 Godel-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 Godel-Gentzen conservative translation, intuitionistic and S4 modal logics relying on the Godel-McKinsey-Tarski conservative translation, and classical and Jaskowski's paraconsistent logics taking into account the existence of a conservative translation.