Uniform Cut-free Bisequent Calculi for Three-valued Logics

TL;DR

The paper develops Uniform Cut-free Bisequent Calculi for Three-valued Logics by introducing BSC, a minimal generalisation of sequent calculus operating on pairs of sequents. It provides a uniform formalisation for key logics like $K_3$ and $LP$, and extends the framework to a wide class of three-valued logics with concrete rule schemata, proving cut-elimination, subformula properties, and interpolation in several cases. The approach yields a constructive, uniform syntactic framework that supports decision procedures and can be extended to four-valued logics and first-order theories, aligning with Suszko’s thesis of two-valued structure underlying many-valued logics. The work offers practical tools for uniform encoding of paraconsistent and paracomplete logics within a concise calculus, enabling systematic analysis across a broad spectrum of three-valued logics.

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.

Theorems & Definitions (23)

• Theorem 1
• proof
• Theorem 2: Soundness
• proof
• Theorem 3: Completeness
• proof
• Theorem 4
• proof
• Lemma 1
• proof