Leibniz-linked pairs of deductive systems (Q647411)

A pair of deductive systems \((S,S')\) sharing the same language is Leibniz-linked when \(S'\) is an extension of (i.e., a stronger logic than) \(S\) and on every algebra there is a map (the Leibniz link) sending each filter of \(S\) to a filter of \(S'\) having the same Leibniz congruence. Another, perhaps more informative, characterization is the following (Theorem 5): a pair \((S, S')\) such that \(S'\) is an extension of \(S\) is Leibniz-linked if and only if the algebraic counterparts of \(S\) and \(S'\) according to the general theory of abstract algebraic logic (i.e., the algebraic reducts of reduced models) coincide. It follows that the algebraic reducts of generalized models of \(S\) and \(S'\) also coincide. Some natural examples of this situation are: {\parindent=4mm \begin{itemize}\item[--] the ``local'' and ``global'' consequence relations associated via the Kripke semantics to normal modal logics; \item[--] logics associated to ordered algebras (fuzzy logics, logics of residuated lattices) with \(S\) being the consequence relation that preserves the degree of truth (i.e., the (lattice) order of the associated algebras) and \(S'\) being the 1-assertional logic, i.e., the one that just preserves ``absolute truth'' (represented, in each algebra, by the top element 1). \end{itemize}} The paper contains an extensive study of Leibniz-linked pairs, generalizing previous results on the so-called strong version of a protoalgebraic logic and considering several examples and counterexamples. Section 1 contains interesting results on the significance of properties of the Leibniz link for the Leibniz hierarchy, for instance: {\parindent=4mm \begin{itemize}\item[--] characterizations of properties of the Leibniz operator of \(S\) in terms of properties of the Leibniz link map between \(S\) and \(S'\) (Proposition 15); \item[--] a classification of \(S\) (such as being protoalgebraic, truth-equational, weakly algebraizable) in terms of properties of the Leibniz link map (Corollaries 16 and 17). \end{itemize}} Section 2 focuses on the situation in which the stronger system \(S'\) of the pair \((S,S')\) is truth-equational. In this case (Theorem 24) the link is unique and uniquely determined through the defining equations of \(S'\). The question of when \(S\) and \(S'\) have the same theorems is also addressed (Theorem 38). The last Section (3) deals with the issue of definability (through a set of formulas or of equations with parameters) of the Leibniz link map (Definition 41), both in general and in the truth-equational case. Some results on the strong version of a protoalgebraic logic are also obtained, for instance (Corollary 46): if \(S\) is protoalgebraic and its strong version \(S+\) is truth-equational, then \(S+\) can always be obtained by adding to \(S\) a set of unary rules that are admissible for \(S\).