Walter Carnielli

This paper introduces the logic _Q__L__E__T_ _F_, a quantified extension of the logic of evidence and truth _L__E__T_ _F_, together with a corresponding sound and complete first-order non-deterministic valuation semantics. _L__E__T_ _F_ is a paraconsistent and paracomplete sentential logic that extends the logic of first-degree entailment (_FDE_) with a classicality operator ∘ and a non-classicality operator ∙, dual to each other: while ∘_A_ entails that _A_ behaves classically, ∙_A_ follows from _A_’s violating some classically valid inferences. The semantics of _Q__L__E__T_ _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.

We propose here an extension of Rice's Theorem to first-order logic, proven by totally elementary means. If P is any property defined over the collection of all first-order theories and P is non-trivial over the set of finitely axiomatizable theories , then P is undecidable. This not only means that the problem of deciding properties of first-order theories is as hard as the problem of deciding properties about languages accepted by Turing machines, but also offers a general setting for proving several undecidability results in first-order theories

Motivated by H. Curry’s well-known objection and by a proposal of L. Henkin, this article introduces the positive tableaux, a form of tableau calculus without refutation based upon the idea of implicational triviality. The completeness of the method is proven, which establishes a new decision procedure for the (classical) positive propositional logic. We also introduce the concept of paratriviality in order to contribute to the question of paradoxes and limitations imposed by the behavior of classical implication.

This paper extends the three-valued paraconsistent logic LFI1 to a class of multimodal systems, generating an infinite hierarchy of three-valued paraconsistent multimodal logics. LFI1, a member of the family of Logics of Formal Inconsistency, is now enriched with multimodal operators. A system is classified as multimodal if its language has more than one modal operator as primitive and such operators are not interdefinable. We provide possible-worlds (or Kripke semantics) characterizations for all such multimodal logics by means of natural canonical models ruled by a relation algebra, and discuss some aspects connected to the interpretation and uses of such logics.

We start from the algebraic method of theorem-proving based on the translation of logic formulas into polynomials over finite fields, and adapt the case of first-order formulas by employing certain rings equipped with infinitary operations. This paper defines the notion of M-ring, a kind of polynomial ring that can be naturally associated to each first-order structure and each first-order theory, by means of generators and relations. The notion of M-ring allows us to operate with some kind of infinitary version of Boolean sums and products, in this way expressing algebraically first-order logic with a new gist. We then show how this polynomial representation of first-order sentences can be seen as a legitimate algebraic semantics for first-order logic, an alternative to cylindric and polyadic algebras and closer to the primordial forms of algebraization of logic. We suggest how the method and its generalization could be lifted successfully to n-valued logics and to other non-classical logics helping to reconcile some lost ties between algebra and logic.

In the previous chapters, LFIs have been approached exclusively from the propositional viewpoint. This is justified by the fact that the main notions and issues of paraconsistency in general, and LFIs, in particular, occur at the propositional level, related to their main connectives, namely, paraconsistent negation, consistency and inconsistency operators. This chapter gives a full account of LFIs for first-order languages, taking into account that quantified versions of LFIs are essential for mathematical applications such as set theory, and also for applications in computer science, such as databases and logic programming.

A Constructive Logic of Evidence and Truth ( $\mathsf {LET_C}$ ) is introduced. This logic is both paraconsistent and paracomplete, providing connectives for consistency and determinedness that enable the independent recovery of explosiveness and the law of excluded middle for specific propositions. Dual connectives for inconsistency and undeterminedness are also defined in $\mathsf {LET_C}$. Evidence is explicitly formalised by integrating lambda calculus terms into $\mathsf {LET_C}$, resulting in the type system $\mathsf {LET_C^{\lambda }}$. In this system, lambda calculus terms represent procedures for constructing evidence for compound formulas based on the evidence of their constituent parts. A realisability interpretation is provided for $\mathsf {LET_C}$, establishing a strong connection between deductions in this system and recursive functions.

Bayesian epistemology has close connections to inductive reasoning, accepting the view that inductive inferences should be analyzed in terms of epistemic probabilities. An important precept of Bayesian epistemology is the dynamics of belief change, with change in belief resulting from updating procedures based on new evidence. The inductive relations between evidence E and hypotheses or theories H are essential, particularly the notions of plausibility, confirmation, and acceptability, which are critical but subject to several difficulties. As a non-deductive process, Bayesian reasoning cannot itself be subjected to strict deductive logic, but it can take advantage of an enabling logical environment. The present paper proposes that paraconsistent and paracomplete logics can be helpful for some questions of Bayesian epistemology, even to the point of being relevant in developing a legitimate paraconsistent Bayesian epistemology. By developing a novel probability theory based on the Logic of Evidence and Truth (LETF\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${LET}_{F}$$\end{document}), a logic that deals with evidence for or against a judgment, including contradictory or missing evidence, we allow for the possibility of quantifying the degree of evidence attributed to a proposition through novel probability measures. We illustrate, through examples, some ways to address challenging problems in the area by using paraconsistent and paracomplete paradigms. This topic is of significant interest not only in the philosophy of science but also in Artificial Intelligence and other emerging trends such as probabilistic networks and related models (see Haenni et al. Probabilistic logics and probabilistic networks, volume 350, Springer, Berlin, 2010)

In this paper we present a philosophical motivation for the logics of formal inconsistency, a family of paraconsistent logics whose distinctive feature is that of having resources for expressing the notion of consistency within the object language in such a way that consistency may be logically independent of non- contradiction. We defend the view according to which logics of formal inconsistency may be interpreted as theories of logical consequence of an epistemological character. We also argue that in order to philosophically justify paraconsistency there is no need to endorse dialetheism, the thesis that there are true contradictions. Furthermore, we argue that an intuitive reading of the bivalued semantics for the logic mbC, a logic of formal inconsistency based on classical logic, fits in well with the basic ideas of an intuitive interpretation of contradictions. On this interpretation, the acceptance of a pair of propositions A and ¬A does not mean that A is simultaneously true and false, but rather that there is conflicting evidence about the truth value of A.

In this paper we propose a very general de nition of combination of logics by means of the concept of sheaves of logics. We first discuss some properties of this general definition and list some problems, as well as connections to related work. As applications of our abstract setting, we show that the notion of possible-translations semantics, introduced in previous papers by the first author, can be described in categorial terms. Possible-translations semantics constitute illustrative cases, since they provide a new semantical account for abstract logical systems, particularly for many-valued and paraconsistent logics.