-
Axiomatizing the Logic of Ordinary Discourse
Authors:
Vitor Greati,
Sérgio Marcelino,
Umberto Rivieccio
Abstract:
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, b…
▽ More
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.
△ Less
Submitted 6 May, 2024;
originally announced May 2024.
-
Nelson algebras, residuated lattices and rough sets: A survey
Authors:
Jouni Järvinen,
Sándor Radeleczki,
Umberto Rivieccio
Abstract:
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 d…
▽ More
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.
△ Less
Submitted 2 March, 2024; v1 submitted 4 February, 2024;
originally announced February 2024.
-
Generating proof systems for three-valued propositional logics
Authors:
Vitor Greati,
Giuseppe Greco,
Sérgio Marcelino,
Alessandra Palmigiano,
Umberto Rivieccio
Abstract:
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 ho…
▽ More
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üller 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.
△ Less
Submitted 6 January, 2024;
originally announced January 2024.
-
Finite Hilbert systems for Weak Kleene logics
Authors:
Vitor Greati,
Sérgio Marcelino,
Umberto Rivieccio
Abstract:
Multiple-conclusion Hilbert-style systems allow us to finitely axiomatize every logic defined by a finite matrix. Having obtained such axiomatizations for Paraconsistent Weak Kleene and Bochvar-Kleene logics, we modify them by replacing the multiple-conclusion rules with carefully selected single-conclusion ones. In this way we manage to introduce the first finite Hilbert-style single-conclusion a…
▽ More
Multiple-conclusion Hilbert-style systems allow us to finitely axiomatize every logic defined by a finite matrix. Having obtained such axiomatizations for Paraconsistent Weak Kleene and Bochvar-Kleene logics, we modify them by replacing the multiple-conclusion rules with carefully selected single-conclusion ones. In this way we manage to introduce the first finite Hilbert-style single-conclusion axiomatizations for these logics.
△ Less
Submitted 20 March, 2024; v1 submitted 6 January, 2024;
originally announced January 2024.
-
Some more theorems on structural entailment relations and non-deterministic semantics
Authors:
Carlos Caleiro,
Sérgio Marcelino,
Umberto Rivieccio
Abstract:
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 high…
▽ More
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.
△ Less
Submitted 4 October, 2023;
originally announced October 2023.
-
Adding an Implication to Logics of Perfect Paradefinite Algebras
Authors:
Vitor Greati,
Sérgio Marcelino,
João Marcos,
Umberto Rivieccio
Abstract:
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…
▽ More
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.
△ Less
Submitted 6 April, 2024; v1 submitted 13 September, 2023;
originally announced September 2023.
-
Algebraizability of the Logic of Quasi-N4-Lattices
Authors:
Clodomir Silva Lima Neto,
Thiago Nascimento da Silva,
Umberto Rivieccio
Abstract:
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 H…
▽ More
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.
△ Less
Submitted 13 April, 2022;
originally announced April 2022.
-
On Logics of Perfect Paradefinite Algebras
Authors:
Joel Gomes,
Vitor Greati,
Sérgio Marcelino,
João Marcos,
Umberto Rivieccio
Abstract:
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 stu…
▽ More
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ú 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.
△ Less
Submitted 8 April, 2022; v1 submitted 17 June, 2021;
originally announced June 2021.
-
Logics of involutive Stone algebras
Authors:
Sérgio Marcelino,
Umberto Rivieccio
Abstract:
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…
▽ More
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.
△ Less
Submitted 12 March, 2021; v1 submitted 10 February, 2021;
originally announced February 2021.
-
Finite axiomatizability of logics of distributive lattices with negation
Authors:
Sérgio Marcelino,
Umberto Rivieccio
Abstract:
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.…
▽ More
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.
△ Less
Submitted 10 February, 2021;
originally announced February 2021.
