Cut-elimination theorems for some logics associated with double Stone algebras

Abstract

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 fourvalued 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.