Search

Most non-classical logics are subclassical, that is, every inference/theorem they validate is also valid classically. A notable exception is the three-valued propositional Logic of Ordinary Discourse (OL) proposed and extensively motivated by W. S. Cooper as a more adequate candidate for formalizing everyday reasoning (in English). OL challenges classical logic not only by rejecting some theses, but also by accepting non-classically valid principles, such as so-called Aristotle's and Boethius' theses. Formally, OL shows a number of unusual features - it is non-structural, connexive, paraconsistent and contradictory - making it all the more interesting for the mathematical logician. We present our recent findings on OL and its structural companion (that we call sOL). We introduce Hilbert-style multiple-conclusion calculi for OL and sOL that are both modular and analytic, and easily allow us to obtain single-conclusion axiomatizations. We prove that sOL is algebraizable and single out its equivalent semantics, which turns out to be a discriminator variety generated by a three-element algebra. Having observed that sOL can express the connectives of other three-valued logics, we prove that it is definitionally equivalent to an expansion of the three-valued logic J3 of D'Ottaviano and da Costa, itself an axiomatic extension of paraconsistent Nelson logic.

Over the past 50 years, Nelson algebras have been extensively studied by distinguished scholars as the algebraic counterpart of Nelson's constructive logic with strong negation. Despite these studies, a comprehensive survey of the topic is currently lacking, and the theory of Nelson algebras remains largely unknown to most logicians. This paper aims to fill this gap by focussing on the essential developments in the field over the past two decades. Additionally, we explore generalisations of Nelson algebras, such as N4-lattices which correspond to the paraconsistent version of Nelson's logic, as well as their applications to other areas of interest to logicians, such as duality and rough set theory. A general representation theorem states that each Nelson algebra is isomorphic to a subalgebra of a rough set-based Nelson algebra induced by a quasiorder. Furthermore, a formula is a theorem of Nelson logic if and only if it is valid in every finite Nelson algebra induced by a quasiorder., Comment: Accepted for publication in Journal of Applied Non-Classical Logics. In this version of the manuscript, certain typographical errors have been rectified

In general, providing an axiomatization for an arbitrary logic is a task that may require some ingenuity. In the case of logics defined by a finite logical matrix (three-valued logics being a particularly simple example), the generation of suitable finite axiomatizations can be completely automatized, essentially by expressing the matrix tables via inference rules. In this chapter we illustrate how two formalisms, the 3-labelled calculi of Baaz, Ferm\"uller and Zach and the multiple-conclusion (or Set-Set) Hilbert-style calculi of Shoesmith and Smiley, may be uniformly employed to axiomatize logics defined by a three-valued logical matrix. The generating procedure common to both formalisms can be described as follows: first (i) convert the matrix semantics into rule form (we refer to this step as the generating subprocedure) and then (ii) simplify the set of rules thus obtained, essentially relying on the defining properties of any Tarskian consequence relation (we refer to this step as the streamlining subprocedure). We illustrate through some examples that, if a minimal expressiveness assumption is met (namely, if the matrix defining the logic is monadic), then it is straightforward to define effective translations guaranteeing the equivalence between the 3-labelled and the Set-Set approach.

We extend classical work by Janusz Czelakowski on the closure properties of the class of matrix models of entailment relations - nowadays more commonly called multiple-conclusion logics - to the setting of non-deterministic matrices (Nmatrices), characterizing the Nmatrix models of an arbitrary logic through a generalization of the standard class operators to the non-deterministic setting. We highlight the main differences that appear in this more general setting, in particular: the possibility to obtain Nmatrix quotients using any compatible equivalence relation (not necessarily a congruence); the problem of determining when strict homomorphisms preserve the logic of a given Nmatrix; the fact that the operations of taking images and preimages cannot be swapped, which determines the exact sequence of operators that generates, from any complete semantics, the class of all Nmatrix models of a logic. Many results, on the other hand, generalize smoothly to the non-deterministic setting: we show for instance that a logic is finitely based if and only if both the class of its Nmatrix models and its complement are closed under ultraproducts. We conclude by mentioning possible developments in adapting the Abstract Algebraic Logic approach to logics induced by Nmatrices and the associated equational reasoning over non-deterministic algebras.

Perfect paradefinite algebras are De Morgan algebras expanded with an operation that allows for the full behavior of classical negation to be restored. They form a variety that is term-equivalent to the variety of involutive Stone algebras. Their associated multiple-conclusion (Set-Set) and single-conclusion (Set-Fmla) order-preserving logics are non-algebraizable self-extensional logics of formal inconsistency and undeterminedness determined by a six-valued matrix, studied in depth by Gomes et al. (2022) from both the algebraic and the proof-theoretical perspectives. In the present paper, we continue that study by investigating directions for conservatively expanding these logics with an implication connective (essentially, one that admits the deduction-detachment theorem). We first consider logics given by very simple and manageable non-deterministic semantics whose implication (in isolation) is classical. These, nevertheless, fail to be self-extensional. We then consider the implication realized by the relative pseudo-complement over the six-valued perfect paradefinite algebra. Our strategy is to expand the language of the latter algebra with this connective and study the (self-extensional) Set-Set and Set-Fmla order-preserving and top-assertional logics of the variety induced by the resulting algebra. We provide axiomatizations for such new variety and for such logics, drawing parallels with the class of symmetric Heyting algebras and with Moisil's 'symmetric modal logic'. For the Set-Set logic, in particular, the axiomatization we obtain is analytic. We close by studying interpolation properties for these logics and concluding that the new variety has the Maehara amalgamation property., Comment: New version after a round of peer reviewing, no critical changes

The class of quasi-N4-lattices (QN4-lattices) was introduced as a common generalization of quasi-Nelson algebras and N4-lattices, in such a way that N4-lattices are precisely the QN4-lattices satisfying the double negation law (~~x = x) and quasi-Nelson algebras are the QN4-lattices satisfying the explosive law (x ^ ~x) -> y = ((x ^ ~x) -> y) -> ((x ^ ~x) -> y). In this paper we introduce, via a Hilbert-style presentation, a logic (L_QN4) whose algebraic semantics is a class of algebras that we show to be term-equivalent to QN4-lattices. The result is obtained by showing that the calculus introduced by us is algebraizable in the sense of Blok and Pigozzi, and its equivalent algebraic semantics is term-equivalent to the class of QN4-lattices. As a prospect for future investigation, we consider the question of how one could place L_QN4 within the family of relevance logics., Comment: In Proceedings NCL 2022, arXiv:2204.06359

The present study shows how to enrich De Morgan algebras with a perfection operator that allows one to express the Boolean properties of negation-consistency and negation-determinedness. The variety of perfect paradefinite algebras thus obtained (PP-algebras) is shown to be term-equivalent to the variety of involutive Stone algebras, introduced by R. Cignoli and M. Sagastume, and more recently studied from a logical perspective by M. Figallo-L. Cant\'u and by S. Marcelino-U. Rivieccio. This equivalence plays an important role in the investigation of the 1-assertional logic and of the order-preserving logic associated to PP-algebras. The latter logic (here called PP<=) is characterized by a single 6-valued matrix and is shown to be a Logic of Formal Inconsistency and Formal Undeterminedness. We axiomatize PP<= by means of an analytic finite Hilbert-style calculus, and we present an axiomatization procedure that covers the logics corresponding to other classes of De Morgan algebras enriched by a perfection operator., Comment: In Proceedings LSFA 2021, arXiv:2204.03415

An involutive Stone algebra (IS-algebra) is a structure that is simultaneously a De Morgan algebra and a Stone algebra (i.e. a pseudo-complemented distributive lattice satisfying the well-known Stone identity ~xv~~x=1). IS-algebras have been studied algebraically and topologically since the 1980's, but a corresponding logic (here denoted IS$\leq$) has been introduced only very recently. The logic IS$\leq$ is the departing point for the present study, which we then extend to a wide family of previously unknown logics defined from IS-algebras. We show that IS$\leq$ is a conservative expansion of the Belnap-Dunn four-valued logic (i.e. the order-preserving logic of the variety of De Morgan algebras), and we give a finite Hilbert-style axiomatization for it. More generally, we introduce a method for expanding conservatively every super-Belnap logic so as to obtain an extension of IS$\leq$. We show that every logic thus defined can be axiomatized by adding a fixed finite set of rule schemata to the corresponding super-Belnap base logic. We also consider a few sample extensions of IS$\leq$ that cannot be obtained in the above-described way, but can nevertheless be axiomatized finitely by other methods. Most of our axiomatization results are obtained in two steps: through a multiple-conclusion calculus first, which we then reduce to a traditional one. The multiple-conclusion axiomatizations introduced in this process, being analytic, are of independent interest from a proof-theoretic standpoint. Our results entail that the lattice of super-Belnap logics (which is known to be uncountable) embeds into the lattice of extensions of IS$\leq$. Indeed, as in the super-Belnap case, we establish that the finitary extensions of IS$\leq$ are already uncountably many., Comment: preprint, 20 pages

This paper focuses on order-preserving logics defined from varieties of distributive lattices with negation, and in particular on the problem of whether these can be axiomatized by means of finite Hilbert calculi. On the side of negative results, we provide a syntactic condition on the equational presentation of a variety that entails failure of finite axiomatizability for the corresponding logic. An application of this result is that the logic of all distributive lattices with negation is not finitely axiomatizable; likewise, we establish that the order-preserving logic of the variety of all Ockham algebras is also not finitely axiomatizable. On the positive side, we show that an arbitrary subvariety of semi-De Morgan algebras is axiomatized by a finite number of equations if and only if the corresponding order-preserving logic is axiomatized by a finite Hilbert calculus. This equivalence also holds for every subvariety of a Berman variety of Ockham algebras. We obtain, as a corollary, a new proof that the implication-free fragment of intuitionistic logic is finitely axiomatizable, as well as a new Hilbert calculus for it. Our proofs are constructive in that they allow us to effectively convert an equational presentation of a variety of algebras into a Hilbert calculus for the corresponding order-preserving logic, and vice versa. We also consider the assertional logics associated to the above-mentioned varieties, showing in particular that the assertional logics of finitely axiomatizable subvarieties of semi-De Morgan algebras are finitely axiomatizable as well., Comment: preprint, 21 pages

Besides the better-known Nelson's Logic and Paraconsistent Nelson's Logic, in "Negation and separation of concepts in constructive systems" (1959), David Nelson introduced a logic called S with the aim of analyzing the constructive content of provable negation statements in mathematics. Motivated by results from Kleene, in "On the Interpretation of Intuitionistic Number Theory" (1945), Nelson investigated a more symmetric recursive definition of truth, according to which a formula could be either primitively verified or refuted. The logic S was defined by means of a calculus lacking the contraction rule and having infinitely many schematic rules, and no semantics was provided. This system received little attention from researchers and it even remained unnoticed that on its original presentation it was inconsistent. Fortunately, the inconsistency was caused by typos and by a rule whose hypothesis and conclusion were swapped.We investigate in the present study a corrected version of the logic S, and focus at its propositional fragment, showing that it is algebraizable (in fact, implicative) with respect to a certain special class of involutive residuated lattices. We thus introduce the first (algebraic) semantics for S as well as a finite Hilbert-style calculus equivalent to Nelson's presentation. We also compare S with the other two above-mentioned logics of the Nelson family., Comment: 16 pages

Besides the better-known Nelson logic (N3) and paraconsistent logic (N4), in 1959 David Nelson introduced, with motivations of realizability and constructibility, a logic called S. The logic S was originally presented by means of a calculus (crucially lacking the contraction rule) with infinitely many rule schemata and no semantics (other than the intended interpretation into Arithmetic.) We look here at the propositional fragment of S, showing that it is algebraizable (in fact, implicative), in the sense of Blok and Pigozzi, with respect to a variety of three-potent involutive residuated lattices. We thus introduce the first known algebraic semantics for S as well as a finite Hilbert-style calculus equivalent to Nelson's presentation; this also allows us to clarify the relation between S and the other two Nelson logics N3 and N4., Comment: 20 pages, 1 figure

We introduce a proper multi-type display calculus for bilattice logic (with conflation) for which we prove soundness, completeness, conservativity, standard subformula property and cut-elimination. Our proposal builds on the product representation of bilattices and applies the guidelines of the multi-type methodology in the design of display calculi.

The aim of this work is to develop a study from the perspective of Abstract Algebraic Logic of some bilattice-based logical systems introduced in the nineties by Ofer Arieli and Arnon Avron. The motivation for such an investigation has two main roots. On the one hand there is an interest in bilattices as an elegant formalism that gave rise in the last two decades to a variety of applications, especially in the field of Theoretical Computer Science and Artificial Intelligence. In this respect, the present study aims to be a contribution to a better understanding of the mathematical and logical framework that underlie these applications. On the other hand, our interest in bilattice-based logics comes from Abstract Algebraic Logic. In very general terms, algebraic logic can be described as the study of the connections between algebra and logic. One of the main reasons that motivate this study is the possibility to treat logical problems with algebraic methods and viceversa: this is accomplished by associating to a logical system a class of algebraic models that can be regarded as the algebraic counterpart of that logic. Starting from the work of Tarski and his collaborators, the method of algebraizing logics has been increasingly developed and generalized. In the last two decades, algebraic logicians have focused their attention on the process of algebraization itself: this kind of investigation forms now a subfield of algebraic logic known as Abstract Algebraic Logic (which we abbreviate AAL)., Comment: PhD Dissertation