SEQUENT CALCULI FOR SOME TRILATTICE LOGICS

The trilattice SIXTEEN3 introduced in Shramko & Wansing (2005) is a natural generalization of the famous bilattice FOUR2. Some Hilbert-style proof systems for trilattice logics related to SIXTEEN3 have recently been studied (Odintsov, 2009; Shramko & Wansing, 2005). In this paper, three sequent calculi Gb, Fb, and Qb are presented for Odintsovʹs (2009) first-degree proof system I—b related to SIXTEEN3. The system Gb is a standard Gentzen-type sequent calculus, F_g is a four-place (horizontal) matrix sequent calculus, and Qb is a quadruple (vertical) matrix sequent calculus. In contrast with Gb , the calculus Fb satisfies the subformula property, and the calculus Qb reflects Odintsovʹs coordinate valuations associated with valuations in SIXT EE N3. The equivalence between Gb , Fb , and Qb , the cut-elimination theorems for these calculi, and the decidability of —b are proved. In addition, it is shown how the sequent systems for —b can be extended to cut-free sequent calculi for Odintsovʹs Lb , which is an extension of —b by adding classical implication and negation connectives.