-
Analytic proofs for logics of evidence and truth
Authors:
Walter Carnielli,
Lorenzzo Frade,
Abilio Rodrigues
Abstract:
This paper presents a sound, complete, and decidable analytic tableau system for the logic of evidence and truth \letf, introduced in
Rodrigues, Bueno-Soler \& Carnielli (Synthese, DOI: 10.1007/s11229-020-02571-w, 2020). \letf\ is an extension of the logic of first-degree entailment (\fde), also known as Belnap-Dunn logic. \fde\ is a widely studied four-valued paraconsistent logic, with applicat…
▽ More
This paper presents a sound, complete, and decidable analytic tableau system for the logic of evidence and truth \letf, introduced in
Rodrigues, Bueno-Soler \& Carnielli (Synthese, DOI: 10.1007/s11229-020-02571-w, 2020). \letf\ is an extension of the logic of first-degree entailment (\fde), also known as Belnap-Dunn logic. \fde\ is a widely studied four-valued paraconsistent logic, with applications in computer science and in the algebra of processes. \letf\ extends \fde\ in a very natural way, by adding a classicality operator \cons, which recovers classical logic for propositions in its scope, and a non-classicality operator \incon, dual of \cons.
△ Less
Submitted 13 December, 2024;
originally announced December 2024.
-
Valuation semantics for first-order logics of evidence and truth (and some related logics)
Authors:
H. Antunes,
A. Rodrigues,
W. Carnielli,
M. E. Coniglio
Abstract:
This paper introduces the logic $QLET_{F}$, a quantified extension of the logic of evidence and truth $LET_{F}$, together with a corresponding sound and complete first-order non-deterministic valuation semantics. $LET_{F}$ is a paraconsistent and paracomplete sentential logic that extends the logic of first-degree entailment ($FDE$) with a classicality operator ${\circ}$ and a non-classicality ope…
▽ More
This paper introduces the logic $QLET_{F}$, a quantified extension of the logic of evidence and truth $LET_{F}$, together with a corresponding sound and complete first-order non-deterministic valuation semantics. $LET_{F}$ is a paraconsistent and paracomplete sentential logic that extends the logic of first-degree entailment ($FDE$) with a classicality operator ${\circ}$ and a non-classicality operator $\bullet$, dual to each other: while ${\circ} A$ entails that $A$ behaves classically, ${\bullet} A$ follows from $A$'s violating some classically valid inferences. The semantics of $QLET_{F}$ combines structures that interpret negated predicates in terms of anti-extensions with first-order non-deterministic valuations, and completeness is obtained through a generalization of Henkin's method. By providing sound and complete semantics for first-order extensions of $FDE$, $K3$, and $LP$, we show how these tools, which we call here the method of ``anti-extensions + valuations'', can be naturally applied to a number of non-classical logics.
△ Less
Submitted 17 June, 2021;
originally announced June 2021.
-
Logics of Formal Inconsistency enriched with replacement: an algebraic and modal account
Authors:
Walter Carnielli,
Marcelo E. Coniglio,
David Fuenmayor
Abstract:
It is customary to expect from a logical system that it can be algebraizable, in the sense that an algebraic companion of the deductive machinery can always be found. Since the inception of da Costa's paraconsistent calculi $C_n$, algebraic equivalents for such systems have been sought. It is known, however, that these systems are not self-extensional (i.e., they do not satisfy the replacement pro…
▽ More
It is customary to expect from a logical system that it can be algebraizable, in the sense that an algebraic companion of the deductive machinery can always be found. Since the inception of da Costa's paraconsistent calculi $C_n$, algebraic equivalents for such systems have been sought. It is known, however, that these systems are not self-extensional (i.e., they do not satisfy the replacement property). More than this, they are not algebraizable in the sense of Blok-Pigozzi. The same negative results hold for several systems of the hierarchy of paraconsistent logics known as Logics of Formal Inconsistency (LFIs). Because of this, several systems belonging to this class of logics are only characterizable by semantics of a non-deterministic nature. This paper offers a solution for two open problems in the domain of paraconsistency, in particular connected to algebraization of LFIs, by extending with rules several LFIs weaker than $C_1$ , thus obtaining the replacement property (that is, such LFIs turn out to be self-extensional). Moreover, these logics become algebraizable in the standard Lindenbaum-Tarski's sense by a suitable variety of Boolean algebras extended with additional operations. The weakest LFI satisfying replacement presented here is called RmbC, which is obtained from the basic LFI called mbC. Some axiomatic extensions of RmbC are also studied. In addition, a neighborhood semantics is defined for such systems. It is shown that RmbC can be defined within the minimal bimodal non-normal logic E+E defined by the fusion of the non-normal modal logic E with itself. Finally, the framework is extended to first-order languages. RQmbC, the quantified extension of RmbC, is shown to be sound and complete w.r.t. the proposed algebraic semantics.
△ Less
Submitted 20 May, 2021; v1 submitted 20 March, 2020;
originally announced March 2020.
-
Twist-Valued Models for Three-valued Paraconsistent Set Theory
Authors:
Walter Carnielli,
Marcelo E. Coniglio
Abstract:
Boolean-valued models of set theory were independently introduced by Scott, Solovay and Vopěnka in 1965, offering a natural and rich alternative for describing forcing. The original method was adapted by Takeuti, Titani, Kozawa and Ozawa to lattice-valued models of set theory. After this, Löwe and Tarafder proposed a class of algebras based on a certain kind of implication which satisfy several ax…
▽ More
Boolean-valued models of set theory were independently introduced by Scott, Solovay and Vopěnka in 1965, offering a natural and rich alternative for describing forcing. The original method was adapted by Takeuti, Titani, Kozawa and Ozawa to lattice-valued models of set theory. After this, Löwe and Tarafder proposed a class of algebras based on a certain kind of implication which satisfy several axioms of ZF. From this class, they found a specific 3-valued model called PS3 which satisfies all the axioms of ZF, and can be expanded with a paraconsistent negation *, thus obtaining a paraconsistent model of ZF. The logic (PS3 ,*) coincides (up to language) with da Costa and D'Ottaviano logic J3, a 3-valued paraconsistent logic that have been proposed independently in the literature by several authors and with different motivations such as CluNs, LFI1 and MPT. We propose in this paper a family of algebraic models of ZFC based on LPT0, another linguistic variant of J3 introduced by us in 2016. The semantics of LPT0, as well as of its first-order version QLPT0, is given by twist structures defined over Boolean agebras. From this, it is possible to adapt the standard Boolean-valued models of (classical) ZFC to twist-valued models of an expansion of ZFC by adding a paraconsistent negation. We argue that the implication operator of LPT0 is more suitable for a paraconsistent set theory than the implication of PS3, since it allows for genuinely inconsistent sets w such that [(w = w)] = 1/2 . This implication is not a 'reasonable implication' as defined by Löwe and Tarafder. This suggests that 'reasonable implication algebras' are just one way to define a paraconsistent set theory. Our twist-valued models are adapted to provide a class of twist-valued models for (PS3,*), thus generalizing Löwe and Tarafder result. It is shown that they are in fact models of ZFC (not only of ZF).
△ Less
Submitted 1 December, 2019; v1 submitted 26 November, 2019;
originally announced November 2019.
-
A Taxonomy of C-systems
Authors:
W. A. Carnielli,
J. Marcos
Abstract:
A thorough investigation of the foundations of paraconsistent logics. Relations between logical principles are formally studied, a novel notion of consistency is introduced, the logics of formal inconsistency, and the subclasses of C-systems and dC-systems are defined and studied. An enormous variety of paraconsistent logics in the literature is shown to constitute C-systems.
A thorough investigation of the foundations of paraconsistent logics. Relations between logical principles are formally studied, a novel notion of consistency is introduced, the logics of formal inconsistency, and the subclasses of C-systems and dC-systems are defined and studied. An enormous variety of paraconsistent logics in the literature is shown to constitute C-systems.
△ Less
Submitted 6 August, 2001;
originally announced August 2001.
