Completeness and cut-elimination theorems for trilattice logics (Q639681)

The paper deals with Gentzen-type formulations of logics (see [\textit{S. P. Odintsov}, Stud. Log. 91, No.~3, 407--428 (2009; Zbl 1170.03014)]), related to the trilattice \(\mathit{SIXTEEN}_3\) (see [\textit{Y. Shramko} and \textit{H. Wansing}, J. Philos. Log. 34, No.~2, 121--153 (2005; Zbl 1094.03012)]). The authors present a sequent calculus \(L_{16}\) for Odintsov's logic \(L_B\), differing from the sequent calculus \(GL_B\) introduced in an earlier paper by the same authors [Rev. Symb. Log. 2, No.~2, 374--395 (2009; Zbl 1174.03008)]. By using the Maehara's method, it is shown that the calculus \(L_{16}\) is strongly complete with respect to a variant of the co-ordinate valuations semantics introduced by Odintsov, enabling a semantic proof of the cut-elimination theorem. Schütte's method, involving the notion of saturated sequents, is used in the proof that the corresponding first-order extension of \(F_{16}\) is sound and complete with respect to first-order models, giving, as a by-product, a semantical proof of the cut-elimination theorem.