Bruno Da Re

In this chapter we will introduce Classical Logic, from both a valuational and a proof-theoretical point of view. We will start by defining some basic tools pertaining to both these frameworks, in a general fashion, so they will be useful for subsequent chapters too. Then, we will present Classical inferential Logic, through the sequent calculus LK and boolean bivaluations. We will then prove various metatheorical results about them, such as Soundness and Completeness, Compactness and Decidability. In the second half of the chapter, we will tackle the metainferential side, presenting different concepts of metainferential validity—both semantical and proof-theoretical. We will also show some metainferential versions of the metatheorems previously proved for the inferential part. We end the chapter by proving Cut-elimination and discussing some of its consequences.

The aim of this work is to introduce a series of requisites for building sound and complete tableaux systems for inferential logics based on non-deterministic valuation schemes and extend them with rules for metainferences, thus yielding metainferential tableaux system capable of proving metainferences of any level n. We show the construction of our tableaux for the logics of the Strong Kleene family and a wide range of different logical systems, most of which have not been studied previously from a metainferential standpoint. Furthermore, we implement this system into a user-friendly, publicly accessible software, designed both for educational purposes as well as assistance in research endeavors.

Recently, Da Ré, Szmuc, Chemla and Égré (2024) showed that all logics based on Boolean Normal monotonic three-valued schemes coincide with classical logic when defined using a strict-tolerant standard (st). Conversely, they proved that under a tolerant-strict standard (ts), the resulting logics are all empty. Building on these results, we show that classical logic can be obtained by closing under transitivity the union of two logics defined over (potentially different) Boolean normal monotonic schemes, using a strict-strict standard (ss) for one and a tolerant-tolerant standard (tt) for the other, with the first of these logics being paracomplete and the other being paraconsistent. We then identify a notion dual to transitivity that allows us to characterize the logic TS as the dual transitive closure of the intersection of any two logics defined over (potentially different) Boolean normal monotonic schemes, using an ss standard for one and a tt standard for the other. Finally, we expand on the abstract relations between the transitive closure and dual transitive closure operations, showing that they give rise to lattice operations that precisely capture how the logics discussed relate to one another.

In recent years, there has been an increasing debate about some philosophical aspects of paraconsistent logics. The focus of this controversy has been on whether the notion of philosophical interpretation of a logic is separable or independent from the notion of application of a logic. The concept of application of a logic, or applied logic, comes from Priest (2005). Given a purely technical system, one can apply it to different domains, such as computer science, programming, formal linguistics, electric circuits, neural networks, control systems, reasoning, etc. On the other hand, Barrio (2018) and Barrio and Da R´e (2018) have argued that there is a third dimension of a logic that consists in its philosophical interpretation. This aspect is related to some intended meaning of the logical constants and the consequence relation of the pure system. In this sense, while Barrio and Da R´e have argued that, at least in some contexts, the concept of philosophical interpretation has an explanatory role, Arenhart (2022) has claimed that this concept can be reduced to the notion of application. In this article, we will show that the philosophical interpretation of a logic has a crucial role in the usual stances of logicians and philosophers, which can and must be distinguished from the application of the system. We will focus on paraconsistent logics as study cases for our points since the debate has developed almost entirely around these systems. However, most of our claims can be applied to any logical system. In fact, throughout the paper, we will also provide examples using non-paraconsistent logics.

Paradoxes make us reflect on our assumptions and intuitions linked to many central notions that we thought were clear and precise. They provoke us to the point of having to abandon basic beliefs about vast areas of our knowledge. Notions such as infinity, truth, knowledge, justification and rationality have been victims of this challenge. In this article we will challenge a widespread view about paradoxes claiming that all of them involve circularity and that their problem is they lead to contradictions. For the former we will employ Yablo’s paradox. Against the latter, we will argue that the key notion is not that of consistency or contradiction, but that of non-triviality. In addition, we will briefly review some nontrivial but inconsistent theories of truth, and argue that ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\omega $$\end{document}-consistency is a requirement for consistent theories of truth, but that inconsistent and non-trivial theories of truth can retain intended models. Finally, we will introduce and defend what we think is the right way of solving semantic paradoxes based on the BA-Plan. In this framework, it is possible to define a naive truth theory avoiding triviality, without abandoning any classical principle, inferential or metainferential.

Much of the interest that substructural logics held over during the last years revolves around how they deal with metainferences. Most notably, the non-transitive—and, therefore, substructural—logic ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{ST }$$\end{document} has sometimes been described as a theory that validates every classical inference while making invalid some classical metainferences. But, what exactly is a metainference?

The validity of an inference has traditionally been associated with the preservation of truth from premises to conclusions. Mixed logics call against this way of understanding this relation: impure mixed logics cannot be understood as preserving some set of designated values from premises to conclusions. Also, some of them have proved to be extremely interesting, and have multiple applications, despite lacking this feature of designated-values preservation. ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{ST }$$\end{document}, in particular, shares all the inferential validities of classical logic, but, unlike it, can be expanded in a non-trivial way with a transparent truth predicate. Thus, if a logic is just a set of inferential validities, then it is no longer true that classical logic cannot be non-trivially extended with a transparent truth predicate.

In this chapter, we will introduce the most studied family of pure and impure mixed metainferential logics of level 1: the Strong Kleene metainferential logics. We will only focus on some of them: the ones that can be characterized through the inferential logics K3,LP,ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{K3}, \textbf{LP}, \textbf{ST }$$\end{document}, and TS\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{TS }$$\end{document}, which will be introduced below.

In this book, as the title suggests, we undertake the task of giving a general account of several aspects of metainferences and metainferential logics. Thus, we need to start by providing a precise definition of what a metainference is. As is commonly assumed, we will take an inference to be an ordered pair of collections of formulas of some formal language. Moreover, logics are usually identified with a certain set of inferences, which are the valid ones. Therefore, inferential consequence relations are defined over collections of formulas. In the traditional picture, metainferences appear as properties that emerge from the set of valid inferences. This is what we call the notion of metainferences as properties.

As we have mentioned in Chap. 3, in [1], PailosPailos, Federico introduces twelve impure metainferential logics defined using two different inferential Tarskian or non-Tarskian (e.g., substructural) logics: K3\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{K3}$$\end{document}, LP\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{LP}$$\end{document}, ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{ST }$$\end{document} or TS\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{TS }$$\end{document}. The standard for premises and conclusions is different in each case. Five of these logics—i.e., TS/ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {TS/ST }$$\end{document}, TS/LP\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {TS/LP }$$\end{document}, TS/K3\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {TS/K3 }$$\end{document}, LP/ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {LP/ST }$$\end{document}, K3/ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {K3/ST }$$\end{document}—are Tarskian logics–i.e., they validate Cut, Identity and Weakening. Moreover, they also validate Meta-Identity, Contraction, and Exchange. Nevertheless, they are defined using substructural inferential logics. In fact, TS/ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {TS/ST }$$\end{document} is built entirely with substructural inferential standards. More significantly, TS/ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {TS/ST }$$\end{document} collapses with CL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{CL }$$\end{document} at the metainferential level, proving to be the only one of these twelve logics with this feature. So, one could wonder what happens when at least one of these standards is not defined through the Strong Kleene schema.

As we have seen, there is a whole family of Strong Kleene mixed and impure metainferential logics. We have already presented the twelve metainferential mixed and impure consequence relations that can be characterized through four inferential logics with the previously mentioned—and well-known—three-valued semantics based on the Strong Kleene schema: ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{ST }$$\end{document}, TS\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{TS }$$\end{document}, K3\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{K3}$$\end{document}, and LP\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{LP}$$\end{document}.

The aim of this chapter is to apply to some metainferential logics the notions of meta-validity presented in Chapter 2. First, we will explore the global2\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$_2$$\end{document} notion (since it is a bit simpler to handle from a technical point of view), and we will show that the pure metainferential logic ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{ST }$$\end{document} also recovers classical logic by substructural means, just as the ST\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textbf{ST }$$\end{document}-hierarchy does locally.

This article aims to dualize several results concerning various types (including possibly Cut-free and Identity-free systems) of canonical multiple-conclusion sequent calculi, i.e. Gentzen-style deduction systems for sequents, equipped with well-behaved forms of left and right introduction rules for logical expressions. In this opportunity, we focus on a different kind of calculi that we dub cocanonical, that is, Gentzen-style deduction systems for sequents, equipped with well-behaved forms of left and right elimination rules for logical expressions. These systems, simply put, have rules that proceed from sequents featuring complex formulas to sequents featuring their component subformulas. Our main goals are to prove soundness and completeness results for the target systems’ consequence relations in terms of their characteristic 3- or 4-valued non-deterministic matrices.

Our aim is to provide a sequent calculus whose external consequence relation coincides with the three-valued paracomplete logic ‘of nonsense’ introduced by Dmitry Bochvar and, independently, presented as the weak Kleene logic $$\textbf{K}_{\textbf{3}}^{\textbf{w}}$$ by Stephen C. Kleene. The main features of this calculus are (i) that it is non-reflexive, i.e., Identity is not included as an explicit rule (although a restricted form of it with premises is derivable); (ii) that it includes rules where no variable-inclusion conditions are attached; and (iii) that it is hybrid, insofar as it includes both left and right operational introduction as well as elimination rules.

This book is the first to present a comprehensive investigation of the technical features of the metainferential logics developed in the last years, with their most relevant results and applications. It provides some new paths to define and investigate metainferential logics and offers a thorough study of the semantics and the proof-theories of this new and exciting variety of families of logics. This volume examines the hierarchies of metainferential logics and gives a general and systematic theory of them, and of the truth theories based on these logics. This book puts forward the prospects for truth-theories based on the metainferential logics of the TS/ST hierarchy and argues for its promise noting that each of these logics can be safely expanded with a transparent truth predicate. It also goes onto to explore new developments in three fields related to logics – namely metainferential logics built by means of the Weak Kleene schema and combining them with logics defined through the Strong Kleene schema, proof-theoretic presentations, and those with a with a global or an absolutely global validity standard, instead of a local one. This book is of interest to scholars in formal logic.

Many authors have considered that the notions of paraconsistency and dialetheism are intrinsically connected, in many cases, to the extent of confusing both phenomena. However, paraconsistency is a formal feature of some logics that consists in invalidating the rule of explosion, whereas dialetheism is a semantical/ontological position consisting in accepting true contradictions. In this paper, we argue against this connection and show that it is perfectly possible to adopt a paraconsistent logic and reject dialetheism, and, moreover, that there are examples of non-paraconsistent logics that can be interpreted in a dialetheic way.

Given a three-valued definition of validity, which choice of three-valued truth tables for the connectives can ensure that the resulting logic coincides exactly with classical logic? We give an answer to this question for the five monotonic consequence relations $st$, $ss$, $tt$, $ss\cap tt$, and $ts$, when the connectives are negation, conjunction, and disjunction. For $ts$ and $ss\cap tt$ the answer is trivial (no scheme works), and for $ss$ and $tt$ it is straightforward (they are the collapsible schemes, in which the middle value acts like one of the classical values). For $st$, the schemes in question are the Boolean normal schemes that are either monotonic or collapsible.

Infectious logics are systems that have a truth-value that is assigned to a compound formula whenever it is assigned to one of its components. This paper studies four-valued infectious logics as the basis of transparent theories of truth. This take is motivated as a way to treat different pathological sentences differently, namely, by allowing some of them to be truth-value gluts and some others to be truth-value gaps and as a way to treat the semantic pathology suffered by at least some of these sentences as infectious. This leads us to consider four distinct four-valued logics: one where truth-value gaps are infectious, but gluts are not; one where truth-value gluts are infectious, but gaps are not; and two logics where both gluts and gaps are infectious, in some sense. Additionally, we focus on the proof theory of these systems, by offering a discussion of two related topics. On the one hand, we prove some limitations regarding the possibility of providing standard Gentzen sequent calculi for these systems, by dualizing and extending some recent results for infectious logics. On the other hand, we provide sound and complete four-sided sequent calculi, arguing that the most important technical and philosophical features taken into account to usually prefer standard calculi are, indeed, enjoyed by the four-sided systems.

Recently, several authors have pointed out that substructural logics are adequate for developing naive theories that represent semantic concepts such as truth. Among them, three proposals have been explored: dropping cut, dropping contraction and dropping reflexivity. However, nowhere in the substructural literature has anyone proposed rejecting the structural rule of weakening, while accepting the other rules. Some theorists have even argued that this task was not possible, since weakening plays no role in the derivation of semantic paradoxes. In this article, I introduce a theory for naive truth based on the logic resulting from dropping the rule of weakening from classical logic, and maintaining the other structural rules.

In this article, our aim is to take a step towards a full understanding of the notion of paraconsistency in the context of metainferential logics. Following the work initiated by Barrio et al. [2018], we will consider a metainferential logic to be paraconsistent whenever the metainferential version of Explosion (or meta-Explosion) is invalid. However, our contribution consists in modifying the definition of meta-Explosion by extending the standard framework and introducing a negation for inferences and metainferences. From this new perspective, Tarskian paraconsistent logics such as LP will not turn out to be metainferentially paraconsistent, in contrast to, for instance, non-transitive logics like ST. Finally, we will end up by defining a logic which is metainferentially paraconsistent at every level, and discussing whether this logic is uniform through translations.

In recent years, some theorists have argued that the clogics are not only defined by their inferences, but also by their metainferences. In this sense, logics that coincide in their inferences, but not in their metainferences were considered to be different. In this vein, some metainferential logics have been developed, as logics with metainferences of any level, built as hierarchies over known logics, such as \, and \. What is distinctive of these metainferential logics is that they are mixed, i.e. the standard for the premises and the conclusion is not necessarily the same. However, so far, all of these systems have been presented following a semantical standpoint, in terms of valuations based on the Strong Kleene truth-tables. In this article, we provide sound and complete sequent-calculi for the valid inferences and the invalid inferences of the logics \ and \, and introduce an algorithm that allows obtaining sound and complete sequent-calculi for the global validities and the global invalidities of any metainferential logic of any level.

The aim of this article is to study the notion of derivability and its semantic counterpart in the context of non-transitive and non-reflexive substructural logics. For this purpose we focus on the study cases of the logics _S__T_ and _T__S_. In this respect, we show that this notion doesn’t coincide, in general, with a nowadays broadly used semantic approach towards metainferential validity: the notion of local validity. Following this, and building on some previous work by Humberstone, we prove that in these systems derivability can be characterized in terms of a notion we call absolute global validity. However, arriving at these results doesn’t lead us to disregard local validity. First, because we discuss the conditions under which local, and also global validity, can be expected to coincide with derivability. Secondly, because we show how taking into account certain families of valuations can be useful to describe derivability for different calculi used to present _S__T_ and _T__S_.

This article is concerned with an exploration of a family of systems—called immune logics—that arise from certain dualizations of the well-known family of infectious logics. The distinctive feature of the semantic of infectious logics is the presence of a certain “infectious” semantic value, by which two different though equivalent things are meant. On the one hand, it is meant that these values are zero elements for all the operations in the underlying algebraic structure. On the other hand, it is meant that these values behave in a value-in-value-out fashion for all the operations in the underlying algebraic structure. Thus, in a rather informal manner, we will refer to immune logics as those systems whose underlying semantics count with a certain “immune” semantic value behaving in a way that is somewhat dual to that of the infectious values. In a more formal manner, carrying out this dualization will prove to be not as straightforward as one could imagine, since the two characterizations of infectiousness discussed above lead to two different outcomes when one tries to conduct them. We explore these alternatives and provide technical results regarding them, and the various logical systems defined using such semantics.