. This paper continues a systematic approach to build natural deduction calculi and corresponding proof procedures for non-classical logics. Our attention is now paid to the framework of paraconsistent logics. These logics are used, in particular, for reasoning about systems where paradoxes do not lead to the `deductive explosion', i.e., where formulae of the type `A follows from false', for any A, are not valid. We formulate the natural deduction system for the logic PCont, explain its main concepts, define a (...) proof searching technique and illustrate it by examples. The presentation is accompanied by demonstrating the correctness of these developments. (shrink)

This document collects natural derivation systems for logics described in Priest, An Introduction to Non-Classical Logic [4]. It provides an alternative or supplement to the semantic tableaux of his text. Except that some chapters are collapsed, there are sections for each chapter in Priest, with an additional, final section on quantified modal logic. In each case, (i) the language is briefly described and key semantic definitions stated, (ii) the derivation system is presented with a few examples given, and (iii) soundness (...) and completeness are proved. There should be enough detail to make the parts accessible to students would work through parallel sections of Priest. (shrink)

Taking our inspiration from modal correspondence theory, we present the idea of correspondence analysis for many-valued logics. As a benchmark case, we study truth-functional extensions of the Logic of Paradox (LP). First, we characterize each of the possible truth table entries for unary and binary operators that could be added to LP by an inference scheme. Second, we define a class of natural deduction systems on the basis of these characterizing inference schemes and a natural deduction system for LP. Third, (...) we show that each of the resulting natural deduction systems is sound and complete with respect to its particular semantics. (shrink)

In the present paper, various features of the class of propositional literal paralogics are considered. Literal paralogics are logics in which the paraproperties such as paraconsistence, paracompleteness and paranormality, occur only at the level of literals; that is, formulas that are propositional letters or their iterated negations. We begin by analyzing Bochvar’s three-valued nonsense logic B3, which includes two isomorphs of the propositional classical logic CPC. The combination of these two ‘strong’ isomorphs leads to the construction of two famous paralogics (...) P1 and I1, which are functionally equivalent. Moreover, each of these logics is functionally equivalent to the fragment of logic B3 consisting of external formulas only. In conclusion, we structure a four-element lattice of three-valued paralogics with respect to the possession of paraproperties. (shrink)

This paper introduces new logical systems which axiomatize a formal representation of inconsistency (here taken to be equivalent to contradictoriness) in classical logic. We start from an intuitive semantical account of inconsistent data, fixing some basic requirements, and provide two distinct sound and complete axiomatics for such semantics, LFI1 and LFI2, as well as their first-order extensions, LFI1* and LFI2*, depending on which additional requirements are considered. These formal systems are examples of what we dub Logics of Formal Inconsistency (LFI) (...) and form part of a much larger family of similar logics. We also show that there are translations from classical and paraconsistent first-order logics into LFI1* and LFI2*, and back. Hence, despite their status as subsystems of classical logic, LFI1* and LFI2* can codify any classical or paraconsistent reasoning. (shrink)

I apply Kooi and Tamminga's (2012) idea of correspondence analysis for many-valued logics to strong three-valued logic (K3). First, I characterize each possible single entry in the truth-table of a unary or a binary truth-functional operator that could be added to K3 by a basic inference scheme. Second, I define a class of natural deduction systems on the basis of these characterizing basic inference schemes and a natural deduction system for K3. Third, I show that each of the resulting natural (...) deduction systems is sound and complete with respect to its particular semantics. Among other things, I thus obtain a new proof system for Lukasiewicz's three-valued logic. (shrink)