Uniform Cut-free Bisequent Calculi for Three-valued Logics

TL;DR

This paper introduces a uniform bisequent calculus framework for three-valued logics, enabling cut-free proofs, subformula property, and interpolation, thus advancing proof theory for non-classical logics.

Contribution

It develops a generalised sequent calculus (BSC) for three-valued logics, demonstrating its effectiveness and applicability to various non-classical logics.

Findings

BSC can formalise multiple three-valued logics.

The systems are cut-free and satisfy the subformula property.

Interpolation theorem holds in many cases.

Abstract

We present a uniform characterisation of three-valued logics by means of the bisequent calculus (BSC). It is a generalised form of a 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, like hypersequent and nested sequent calculi. It seems that for many non-classical logics, including some many-valued, paraconsistent and modal logics, the reasonably modest generalisation of standard SC offered by BSC is sufficient. In this paper we examine a variety of three-valued logics and show how they can be formalised in the framework of BSC. We present a constructive syntactic proof provided that these systems are cut-free, satisfy the subformula property, and allow one to prove the interpolation theorem in many cases.