A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus

We present a uniform characterisation of three-valued logics by means of bisequent calculus (BSC). It is a generalised form of sequent calculus (SC) where rules operate on the ordered pairs of ordinary sequents. BSC may be treated as the weakest kind of system in the rich family of generalised SC operating on items being some collections of ordinary sequents. This family covers several forms of hypersequent and nested sequent calculi introduced to provide decent SC for several non-classical logics. It seems that for many non-classical logics, including some many-valued, paraconsistent and modal logics, this reasonably modest generalization of standard SC is sufficient. In this paper we examine a variety of three-valued logics and show how they can be formalised in the framework of bisequent calculus. All provided systems are cut-free and satisfy the subformula property. Also the interpolation theorem is constructively proved for some logics.