Cut-free sequent-style systems for a logic associated to involutive Stone algebras

In \cite{LC, LCMF}, it was introduced a logic (called \Six ) associated to a class of algebraic structures known as {\em involutive Stone algebras}. This class of algebras, denoted by \Sto , was considered by the first time in \cite{CS1} as a tool for the study of certain problems connected to the theory of finite–valued Łukasiewicz–Moisil algebras. In fact, \Six\ is the logic that preserves degrees of truth with respect to the class \Sto . Among other things, it was proved that \Six\ is a 6–valued logic that is a {\em Logic of Formal Inconsistency} (\LFI ); moreover, it is possible to define a consistency operator in terms of the original set of connectives. A Gentzen-style system (which does not enjoy the cut–elimination property) for \Six\ was given. Besides, in \cite{LCMF}, it was shown that \Six\ is matrix logic that is determined by a finite number of matrices; more precisely, four matrices. However, this result was further sharpened in \cite{SMUR} proving that just one of these four matrices determine \Six , that is, \Six\ can be determined by a single 6–element logic matrix. In this work, taking advantage of this last result, we apply a method due to Avron, Ben-Naim and Konikowska \cite{Avron02} to present different Gentzen systems for \Six\ enjoying the cut–elimination property. This allows us to draw some conclusions about the method as well as to propose additional tools for the streamlining process. Finally, we present a decision procedure for \Six\ based in one of these systems.