Maximality is a desirable property of paraconsistent logics, motivated by the aspiration to tolerate inconsistencies, but at the same time retain from classical logic as much as possible. In this paper we introduce the strongest possible notion of maximal paraconsistency, and investigate it in the context of logics that are based on deterministic or non-deterministic three-valued matrices. We show that all reasonable paraconsistent logics based on three-valued deterministic matrices are maximal in our strong sense. This applies to practically all three-valued (...) paraconsistent logics that have been considered in the literature, including a large family of logics which were developed by da Costa's school. Then we show that in contrast, paraconsistent logics based on three-valued properly nondeterministic matrices are not maximal, except for a few special cases (which are fully characterized). However, these non-deterministic matrices are useful for representing in a clear and concise way the vast variety of the (deterministic) three-valued maximally paraconsistent matrices. The corresponding weaker notion of maximality, called premaximal paraconsistency, captures the "core" of maximal paraconsistency of all possible paraconsistent determinizations of a non-deterministic matrix, thus representing what is really essential for their maximal paraconsistency. (shrink)

This paper develops an inference system for natural language within the ‘Natural Logic’ paradigm as advocated by van Benthem, Sánchez and others. The system that we propose is based on the Lambek calculus and works directly on the Curry-Howard counterparts for syntactic representations of natural language, with no intermediate translation to logical formulae. The Lambek -based system we propose extends the system by Fyodorov et~al., which is based on the Ajdukiewicz/Bar-Hillel calculus Bar Hillel,. This enables the system to deal with (...) new kinds of inferences, involving relative clauses, non-constituent coordination, and meaning postulates that involve complex expressions. Basing the system on the Lambek calculus leads to problems with non-normalized proof terms, which are treated by using normalization axioms. (shrink)

Paraconsistent logics are logics that, in contrast to classical and intuitionistic logic, do not trivialize inconsistent theories. In this paper we take a paraconsistent view on two famous modal logics: B and S5. We use for this a well-known general method for turning modal logics to paraconsistent logics by defining a new negation as $\neg \varphi =_{Def} \sim \Box \varphi$. We show that while that makes both B and S5 members of the well-studied family of paraconsistent C-systems, they differ from (...) most other C-systems in having the important replacement property. We further show that B is a very robust C-system in the sense that almost any axiom which has been considered in the context of C-systems is either already a theorem of B or its addition to B leads to a logic that is no longer paraconsistent. There is exactly one notable exception, and the result of adding this exception to B leads to the other logic studied here, S5. (shrink)

Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with (...) unary quantifiers and show that it remains constructive. Then we provide semantics for such canonical systems using 2-valued non-deterministic matrices extended to languages with quantifiers, and prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix. (shrink)

This book is a collection of contributions honouring Arnon Avron’s seminal work on the semantics and proof theory of non-classical logics. It includes presentations of advanced work by some of the most esteemed scholars working on semantic and proof-theoretical aspects of computer science logic. Topics in this book include frameworks for paraconsistent reasoning, foundations of relevance logics, analysis and characterizations of modal logics and fuzzy logics, hypersequent calculi and their properties, non-deterministic semantics, algebraic structures for many-valued logics, and representations of (...) the mechanization of mathematics. Avron’s foundational and pioneering contributions have been widely acknowledged and adopted by the scientific community. His research interests are very broad, spanning over proof theory, automated reasoning, non-classical logics, foundations of mathematics, and applications of logic in computer science and artificial intelligence. This is clearly reflected by the diversity of topics discussed in the chapters included in this book, all of which directly relate to Avron’s past and present works. This book is of interest to computer scientists and scholars of formal logic. (shrink)

An (n, k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical systems with (n, k)-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion of coherence (...) to characterize strong cutelimination in such systems. We show that the following properties of a canonical system G with arbitrary (n, k)-ary quantifiers are equivalent: (i) G is coherent, (ii) G admits strong cut-elimination, and (iii) G has a strongly characteristic two-valued generalized non-deterministic matrix. (shrink)