Sequent-Type Calculi for Systems of Nonmonotonic Paraconsistent Logics

TL;DR

This paper develops uniform sequent calculus systems for a family of nonmonotonic paraconsistent logics based on minimal inconsistency, including Priest's three-valued logic and four-valued inference relations, facilitating proof analysis.

Contribution

It introduces a general method to derive sequent calculi for many-valued paraconsistent logics based on minimal inconsistency, unifying several existing systems.

Findings

Provided sequent calculi for Priest's three-valued logic.

Developed calculi for Arieli and Avron's four-valued inference.

Established a general method for many-valued logic axiomatisation.

Abstract

Paraconsistent logics constitute an important class of formalisms dealing with non-trivial reasoning from inconsistent premisses. In this paper, we introduce uniform axiomatisations for a family of nonmonotonic paraconsistent logics based on minimal inconsistency in terms of sequent-type proof systems. The latter are prominent and widely-used forms of calculi well-suited for analysing proof search. In particular, we provide sequent-type calculi for Priest's three-valued minimally inconsistent logic of paradox, and for four-valued paraconsistent inference relations due to Arieli and Avron. Our calculi follow the sequent method first introduced in the context of nonmonotonic reasoning by Bonatti and Olivetti, whose distinguishing feature is the use of a so-called rejection calculus for axiomatising invalid formulas. In fact, we present a general method to obtain sequent systems for any many-valued logic based on minimal inconsistency, yielding the calculi for the logics of Priest and of Arieli and Avron as special instances.