Logics preserving degrees of truth from varieties of residuated lattices

TL;DR

This paper introduces a new logic that preserves degrees of truth in residuated lattices, analyzing its algebraic properties, classification, and relation to the traditional truth-preserving logic within the framework of abstract algebraic logic.

Contribution

It defines and characterizes a novel logic preserving degrees of truth, exploring its algebraic models, classification, and connections to existing logics in residuated lattice varieties.

Findings

The new logic is fully selfextensional.

It is non-protoalgebraic for most varieties K.

It is algebraizable only when K is a variety of generalized Heyting algebras.

Abstract

Let K be a variety of (commutative, integral) residuated lattices. The substructural logic usually associated with K is an algebraizable logic that has K as its equivalent algebraic semantics, and is a logic that preserves truth, i.e., 1 is the only truth value preserved by the inferences of the logic. In this paper we introduce another logic associated with K, namely the logic that preserves degrees of truth, in the sense that it preserves lower bounds of truth values in inferences. We study this second logic mainly from the point of view of abstract algebraic logic. We determine its algebraic models and we classify it in the Leibniz and the Frege hierarchies: we show that it is always fully selfextensional, that for most varieties K it is non-protoalgebraic, and that it is algebraizable if and only K is a variety of generalized Heyting algebras, in which case it coincides with the logic that preserves truth. We also characterize the new logic in three ways: by a Hilbert style axiomatic system, by a Gentzen style sequent calculus, and by a set of conditions on its closure operator. Concerning the relation between the two logics, we prove that the truth preserving logic is the purely inferential extension of the one that preserves degrees of truth with either the rule of Modus Ponens or the rule of Adjunction for the fusion connective.