From Translations to Non-Collapsing Logic Combinations

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.