On the logic that preserves degrees of truth associated to involutive Stone algebras

Involutive Stone algebras (or {\bf S}–algebras) were introduced by R. Cignoli and M. Sagastume in connection to the theory of $n$-valued Łukasiewicz–Moisil algebras. In this work we focus on the logic that preserves degrees of truth associated to involutive Stone algebras, named {\bf \em Six}. This follows a very general pattern that can be considered for any class of truth structure endowed with an ordering relation, and which intends to exploit many–valuedness focusing on the notion of inference that results from preserving lower bounds of truth values, and hence not only preserving the value $1$. Among other things, we prove that {\bf \em Six} is a many–valued logic (with six truth values) that can be determined by a finite number of matrices (four matrices). Besides, we show that {\bf \em Six} is a paraconsistent logic. Moreover, we prove that it is a genuine LFI (Logic of Formal Inconsistency) with a consistency operator that can be defined in terms of the original set of connectives. Finally, we study the proof theory of {\bf \em Six} providing a Gentzen calculus for it, which is sound and complete with respect to the logic.