The ubiquity of conservative translations

TL;DR

This paper demonstrates that classical propositional logic and many other nonclassical logics are universal targets for conservative translations of finitary consequence relations, highlighting the broad applicability of such translations.

Contribution

It proves the universality of classical propositional logic and certain nonclassical logics for conservative translations of finitary consequence relations.

Findings

CPC is universal for finitary consequence relations

Translations are computable if the consequence relation is decidable

Most nonclassical logics studied can be conservatively translated into CPC or similar logics

Abstract

We study the notion of conservative translation between logics introduced by Feitosa and D'Ottaviano. We show that classical propositional logic (CPC) is universal in the sense that every finitary consequence relation over a countable set of formulas can be conservatively translated into CPC. The translation is computable if the consequence relation is decidable. More generally, we show that one can take instead of CPC a broad class of logics (extensions of a certain fragment of full Lambek calculus FL) including most nonclassical logics studied in the literature, hence in a sense, (almost) any two reasonable deductive systems can be conservatively translated into each other. We also provide some counterexamples, in particular the paraconsistent logic LP is not universal.