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 ⊢B related to SIXTEEN3. The system GB is a standard Gentzen-type sequent calculus, FB 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 SIXTEEN3. 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. [ABSTRACT FROM AUTHOR]