Truth and Falsehood pp 113-141 | Cite as

# Sequent Systems for Trilattice Logics

## Abstract

In the present chapter, we will define various standard and non-standard sequent calculi for logics related to the trilattice
*SIXTEEN* _{3}. In a *first* step, we will introduce three sequent calculi *G*_{ B },
*F*_{ B },
and *Q*_{B}
for Odintsov’s
first-degree proof system ⊢_{ B } presented in the previous chapter. The system *G*_{ B } is a standard Gentzen-type sequent calculus, *F*_{B} is a four-place (horizontal) matrix sequent calculus, and *Q*_{ B } is a quadruple (vertical) matrix sequent calculus. In contrast with *G*_{ B }, the calculus \(\hbox{F}_B\) satisfies the subformula property, and the calculus \(\hbox{Q}_B\) reflects Odintsov’s co-ordinate valuations associated with valuations in \(SIXTEEN_3\). The mutual equivalence between \(G_B\), \(\hbox{F}_B, \) and \(\hbox{Q}_B\), the cut-elimination theorems for these calculi, and the decidability of \(\vdash _B\) are proved. In addition, it is shown how the sequent systems for \(\vdash _B\) can be extended to cut-free sequent calculi for Odintsov’s \(L_B\), which is an extension of \(\vdash_B\) by adding classical implication and negation connectives. The axiom systems \(L_T,L_B,L^{f}_{T},L^{f}_{B},{L'}_T,{L'}_B,{{{L}^{f}}'}_{T},\) and \({{{L}^{f}}'}_{B}\) from Chap. 5 are all auxiliary calculi in the sense that they do not capture truth entailment \(\models_t\) or falsity entailment \(\models _f\) in the respective languages. The chief axiom systems are those capturing the semantically defined logics \(L^t,L^f,{L'},{{L}^f}',L^{t*}\) and \(L^{f*}\). In a *second* step, we will present cut-free sound and complete higher-arity sequent calculi for all these axiom systems. The semantical foundation of these calculi is provided by the co-ordinate valuations. A sequent calculus \({\text{GL}}^*\)
for truth entailment in \(SIXTEEN_3\) in the full language \({\fancyscript{L}}^*_{tf}\) is introduced and shown to be sound and complete and admitting of cut-elimination. This sequent calculus directly takes up Odintsov’s presentation of \(SIXTEEN_3\) as a twist-structure over the two-element Boolean algebra and enjoys all the nice properties known from the **G3c** sequent calculus for classical logic, see Troelstra and Schwichtenberg (Cambridge University Press, Cambridge, 2000). Moreover, a sequent calculus for falsity entailment in \(SIXTEEN_3\) in \({\fancyscript{L}}^*_{tf}\) can be obtained from \({\text{GL}}^{*}\) not by changing any of the inference rules of the system but simply by appropriately changing the notion of a provable formula.