Constructive negations and paraconsistency (Q932098)

This is the first book-length algebraic study of constructive paraconsistent logics. It contains a comprehensive algebraic investigation of the lattices of extensions of both (i) Johansson's minimal propositional logic \textbf{Lj} and (ii) David Nelson's paraconsistent constructive propositional logic with strong negation \textbf{N4}, as well as its extension by a falsum constant, the system \textbf{N4}\(^{\bot}\). These logics are of interest for quite a few reasons, one being that they are paraconsistent analogues of the better known intuitionistic propositional logic \textbf{Li} and Nelson's intuitionistic logic with strong negation \textbf{N3}, respectively. Whereas the relational (Kripke-style) semantics for \textbf{N3} is three-valued, the relational semantics for the paraconsistent logic \textbf{N4} is four-valued, hence the notation. The monograph under review has a very clear structure. Chapter one is a brief introduction to the subject matter of the book, to the history of constructive paraconsistent logics, and to the presented results. The rest of the material is arranged into two parts, Chapters 2--7 and Chapters 8--10. Moreover, there are some concluding remarks in a rather short Chapter 11, a comprehensive and very useful bibliography, and an index of key terms and some notation. Each part of the book is devoted to a particular treatment of negation in constructive logic. Part I deals with the purely implication treatment of negation as (leading to) absurdity, and Part II is devoted to strong negation in the sense of definite falsity (or denial). The first part of the book offers an in-depth study of the lattice of extensions of \textbf{Lj}. This lattice is shown to be the disjoint union of the class of intermediate logics, the class of all properly paraconsistent extensions of \textbf{Lj}, and the class of extension of \textbf{Lj} containing the scheme \(\neg p\). The notions of intuitionistic and negative counterparts of a paraconsistent logic are defined and consequence relation preserving translations of the counterpart logics into the paraconsistent logics of which they are counterparts are defined. It turns out that the negative counterpart of a paraconsistent logic \(L\) may be seen as \(L\)'s logic of contradictions. The standard implicational treatment of negation as implying an absurdity constant is generalized by introducing a unary absurdity operator \(\mathcal A\): \[ \neg \varphi := \varphi \rightarrow {\mathcal A}\varphi . \] It is shown that the negation of many paraconsistent logics can be defined in this way. The investigation of the lattice of extensions of Nelson's paraconsistent logic with strong negation in Part II of the book reveals some essential difference in comparison with the lattice structure of the extensions of \textbf{Lj}. Axiomatically, the system \textbf{N4}\(^{\bot}\) extends Nelson's \textbf{N4} by introducing the constant \(\bot\) and the axioms \(\bot \rightarrow p\) and \(p \rightarrow {\sim p}\), where \(\sim\) is the strong negation. The algebraic investigation of the extensions of \textbf{N4} utilizes Odintsov's theory of \textbf{N4}-lattices, where the representation of \textbf{N4}-lattices in the form of twist-structures (as introduced by M. Fidel and D. Vakarelov, though not under this name) plays the central role. To deal with extensions of \textbf{N4}\(^{\bot}\), \textbf{N4}\(^{\bot}\)-lattices are introduced. \textbf{N4}\(^{\bot}\) does not admit contradictory extensions, and its class of extensions can again be decomposed into three subclasses. As applications of the developed general theory, a complete description is given of the lattice of extensions of \textbf{N4}\(^{\bot}\) containing Dummett's linearity axiom, as well as of pretabular \textbf{N4}\(^{\bot}\) extensions and \textbf{N4}\(^{\bot}\) extensions with the Craig interpolation property. This monograph is indispensable for anybody interested in the algebraic study of constructive paraconsistent logics in particular, but it is also most rewarding for anyone interested in non-classical logics in general.