Sequent Systems for Trilattice Logics

Chapter
Part of the Trends in Logic book series (TREN, volume 36)

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 QB for Odintsov’s first-degree proof system ⊢ B presented in the previous chapter. The system G B is a standard Gentzen-type sequent calculus, FB 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 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. 