A double Stone algebra is a Stone algebra whose dual lattice is also a Stone algebra. Logics that may be associated with double Stone algebras are based on bounded distributive lattices which are endowed with two negations: a Heyting negation (the pseudocomplement) and a Brouwer negation (the dual pseudocomplement) possibly satisfying some constraints. Different authors have studied the order-preserving logic associated with double Stone algebras. Recently, the four-valued character of this logic was exploited by providing a rough set semantics for it. In this paper, we explore the proof-theoretical aspect of two logics associated with double Stone algebras, namely, the truth-preserving and the order-preserving logic, respectively. We provide sequent systems sound and complete for these logics and prove the cut-elimination theorem for both systems.

Abstract In this paper, we investigate proof-theoretic aspects of the logics of evidence and truth $LET_{J}$ and $LET_{F}$. These logics extend, respectively, Nelson’s logic N4 and the logic of first-degree entailment, also known as Belnap–Dunn four-valued logic, with a classicality operator ${{\circ }}$ that recovers classical logic for formulas in its scope. We will present natural deduction and sequent systems for $LET_{J}$ and $LET_{F}$, together with proofs of normalization and cut-elimination theorems, respectively. As a corollary, we obtain decision procedures, which guarantees bottom-up proof search for both logics.

Abstract In [4, 5], it was introduced a logic (called Six) associated to a class of algebraic structures known as involutive Stone algebras. This class of algebras, denoted by S, was considered by the first time in [6] 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 S. Among other things, it was proved that Six is a 6-valued logic that is a 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 [5], 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 [17], proving that just one of these four matrices determine Six, i.e. 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 [3] 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.