Sayantan Roy

Paraconsistency is commonly defined and/or characterized as the failure of a principle of explosion. The various standard forms of explosion involve one or more logical operators or connectives, among which the negation operator is the most frequent and primary. In this article, we start by asking whether a negation operator is essential for describing explosion and paraconsistency. In other words, is it possible to describe a principle of explosion and hence a notion of paraconsistency that is independent of connectives? A negation-free paraconsistency resulting from the failure of a generalized principle of explosion is presented first. We also derive a notion of quasi-negation from this and investigate its properties. Next, more general principles of explosion are considered. These are also negation-free; moreover, these principles gradually move away from the idea that an explosion requires a statement and its opposite. Thus, these principles can capture the explosion observed in logics where a statement and its negation explode only in the presence of additional information, such as in the logics of formal inconsistency.

Cut-elimination theorems constitute one of the most important classes of theorems of proof theory. Since Gentzen’s proof of the cut-elimination theorem for the system LK, several other proofs have been proposed. Even though the techniques of these proofs can be modified to sequent systems other than $$\textbf{LK}$$, they are essentially of a very particular nature; each of them describes an algorithm to transform a given proof to a cut-free proof. However, due to its reliance on heavy syntactic arguments and case distinctions, such an algorithm makes the fundamental structure of the argument rather opaque. We, therefore, consider rules abstractly, within the framework of logical structures familiar from universal logic in the sense of Béziau (Universal logic, Prague, 1994) and aim to clarify the essence of the so-called “elimination theorems”. To do this, we first give a non-algorithmic proof of the cut-elimination theorem for the propositional fragment of $$\textbf{LK}$$. From this proof, we abstract the essential features of the argument and define something called normal sequent structures relative to a particular rule. We then prove a version of the rule-elimination theorem for these. Abstracting even more, we define abstract sequent structures and show that for these structures, the corresponding version of the rule-elimination theorem has a converse as well.

In this paper, we study some classes of logical structures from the universal logic standpoint, viz., those of the Tarski- and the Lindenbaum-types. The characterization theorems for the Tarski- and two of the four different Lindenbaum-type logical structures have been proved as well. The separations between the five classes of logical structures, viz., the four Lindenbaum-types and the Tarski-type have been established via examples. Finally, we study the logical structures that are of both Tarski- and a Lindenbaum-type, show their separations, and end with characterization, adequacy, minimality, and representation theorems for one of the Tarski–Lindenbaum-type logical structures.