Proof theory of Nelson’s paraconsistent logic: A uniform perspective

The aim of this paper is to obtain a theoretical foundation of inconsistency-tolerant (or paraconsistent) reasoning by presenting a comprehensive study of the structural proof-theory of David Nelson’s paraconsistent logic. Inconsistency handling has a growing importance in Computer Science since inconsistencies may frequently occur in knowledge-based and intelligent information systems. Paraconsistent, inconsistency-tolerant logics have been studied to cope with such inconsistencies. In this paper, proof systems for Nelson’s paraconsistent logic N4 are comprehensively studied. The logic N4 is a fundamental system and known to be a common basis for various extended and useful paraconsistent logics. Some basic theorems including cut-elimination, normalization and completeness are uniformly proved using various embedding theorems. A variety of sequent calculi and natural deduction systems for N4 and some closely related systems are presented and compared.