Arnon Avron

We define the notions of a canonical inference rule and a canonical system in the framework of single-conclusion Gentzen-type systems (or, equivalently, natural deduction systems), and prove that such a canonical system is non-trivial iff it is coherent (where coherence is a constructive condition). Next we develop a general non-deterministic Kripke-style semantics for such systems, and show that every constructive canonical system (i.e. coherent canonical single-conclusion system) induces a class of non-deterministic Kripke-style frames for which it is strongly sound and complete. We use this non-deterministic semantics to show that all constructive canonical systems admit a strong form of the cut-elimination theorem. We also use it for providing a decision procedure for every such system. These results identify a large family of basic constructive connectives, each having both a proof-theoretical characterization in terms of a coherent set of canonical rules, as well as a semantic characterization using non-deterministic frames. The family includes the standard intuitionistic connectives, together with many other independent connectives

A paraconsistent logic is a logic which allows non-trivial inconsistent theories. One of the oldest and best known approaches to the problem of designing useful paraconsistent logics is da Costa’s approach, which seeks to allow the use of classical logic whenever it is safe to do so, but behaves completely differently when contradictions are involved. da Costa’s approach has led to the family of Logics of Formal (In)consistency (LFIs). In this paper we provide non-deterministic semantics for a very large family of first-order LFIs (which includes da Costa’s original system..

Until not too many years ago, all logics except classical logic (and, perhaps, intuitionistic logic too) were considered to be things esoteric. Today this state of a airs seems to have completely been changed. There is a growing interest in many types of nonclassical logics: modal and temporal logics, substructural logics, paraconsistent logics, non-monotonic logics { the list is long. The diversity of systems that have been proposed and studied is so great that a need is felt by many researchers to try to put some order in the present logical jungle. Thus Cl91], Ep90] and Wo88] are three recent books in which an attempt is made to develop a general theoretical framework for the study of logics. On the more pragmatic side, several systems have been developed with the goal of providing a computerized logical framework in which many di erent logical systems can be implemented in a uniform way. An example is the Edinburgh LF( HHP91])

Maximality is a desirable property of paraconsistent logics, motivated by the aspiration to tolerate inconsistencies, but at the same time retain from classical logic as much as possible. In this paper we introduce the strongest possible notion of maximal paraconsistency, and investigate it in the context of logics that are based on deterministic or non-deterministic three-valued matrices. We show that all reasonable paraconsistent logics based on three-valued deterministic matrices are maximal in our strong sense. This applies to practically all three-valued paraconsistent logics that have been considered in the literature, including a large family of logics which were developed by da Costa's school. Then we show that in contrast, paraconsistent logics based on three-valued properly nondeterministic matrices are not maximal, except for a few special cases (which are fully characterized). However, these non-deterministic matrices are useful for representing in a clear and concise way the vast variety of the (deterministic) three-valued maximally paraconsistent matrices. The corresponding weaker notion of maximality, called premaximal paraconsistency, captures the "core" of maximal paraconsistency of all possible paraconsistent determinizations of a non-deterministic matrix, thus representing what is really essential for their maximal paraconsistency

In the paper we explore the idea of describing Pawlak’s rough sets using three-valued logic, whereby the value t corresponds to the positive region of a set, the value f — to the negative region, and the undefined value u — to the border of the set. Due to the properties of the above regions in rough set theory, the semantics of the logic is described using a non-deterministic matrix (Nmatrix). With the strong semantics, where only the value t is treated as designated, the above logic is a “common denominator” for Kleene and Łukasiewicz 3-valued logics, which represent its two different “determinizations”. In turn, the weak semantics—where both t and u are treated as designated—represents such a “common denominator” for two major 3-valued paraconsistent logics. We give sound and complete, cut-free sequent calculi for both versions of the logic generated by the rough set Nmatrix. Then we derive from these calculi sequent calculi with the same properties for the various “determinizations” of those two versions of the logic (including Łukasiewicz 3-valued logic). Finally, we show how to embed the four above-mentioned determinizations in extensions of the basic rough set logics obtained by adding to those logics a special two-valued “definedness” or “crispness” operator.

We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deduction-style proof systems for representing both truth (local) and validity (global) consequence relations for various Modal Logics. We introduce several techniques for encoding the structural peculiarities of necessitation rules, in the typed -calculus metalanguage of the Logical Frameworks. These formalizations yield readily proof-editors for Modal Logics when implemented in Proof Development Environments, such as Coq or LEGO

In the paper we examine the use of non-classical truth values for dealing with computation errors in program specification and validation. In that context, 3-valued McCarthy logic is suitable for handling lazy sequential computation, while 3-valued Kleene logic can be used for reasoning about parallel computation. If we want to be able to deal with both strategies without distinguishing between them, we combine Kleene and McCarthy logics into a logic based on a non-deterministic, 3-valued matrix, incorporating both options as a non-deterministic choice. If the two strategies are to be distinguished, Kleene and McCarthy logics are combined into a logic based on a 4-valued deterministic matrix featuring two kinds of computation errors which correspond to the two computation strategies described above. For the resulting logics, we provide sound and complete calculi of ordinary, two-valued sequents

An (n, k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical systems with (n, k)-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion of coherence to characterize strong cutelimination in such systems. We show that the following properties of a canonical system G with arbitrary (n, k)-ary quantifiers are equivalent: (i) G is coherent, (ii) G admits strong cut-elimination, and (iii) G has a strongly characteristic two-valued generalized non-deterministic matrix.

In order to handle inconsistent knowledge bases in a reasonable way, one needs a logic which allows nontrivial inconsistent theories. Logics of this sort are called paraconsistent. One of the oldest and best known approaches to the problem of designing useful paraconsistent logics is da Costa’s approach, which seeks to allow the use of classical logic whenever it is safe to do so, but behaves completely differently when contradictions are involved. Da Costa’s approach has led to the family of logics of formal (in)consistency (LFIs). In this paper we provide in a modular way simple non-deterministic semantics for 64 of the most important logics from this family. Our semantics is 3-valued for some of the systems, and infinite-valued for the others. We prove that these results cannot be improved: neither of the systems with a three-valued non-deterministic semantics has either a finite characteristic ordinary matrix or a two-valued characteristic non-deterministic matrix, and neither of the other systems we investigate has a finite characteristic non-deterministic matrix. Still, our semantics provides decision procedures for all the systems investigated, as well as easy proofs of important proof-theoretical properties of them

We show that the rule that allows the inference of A from A ⊗ B is admissible in many of the basic multiplicative systems. By adding this rule to these systems we get, therefore, conservative extensions in which the tensor behaves as classical conjunction. Among the systems obtained in this way the one derived from RMIm has a particular interest. We show that this system has a simple infinite-valued semantics, relative to which it is strongly complete, and a nice cut-free Gentzen-type formulation which employs hypersequents . Moreover: classical logic has a simple, strong translation into this logic. This translation uses definable connectives and preserves the consequence relation of classical logic . Similar results, but with a 3-valued semantics, obtain if instead of RMIm we use RMm

In advanced books and courses on logic (e.g. Sm], BM]) Gentzen-type systems or their dual, tableaux, are described as techniques for showing validity of formulae which are more practical than the usual Hilbert-type formalisms. People who have learnt these methods often wonder why the Automated Reasoning community seems to ignore them and prefers instead the resolution method. Some of the classical books on AD (such as CL], Lo]) do not mention these methods at all. Others (such as Ro]) do, but the connections and reasons for preference remain unclear after reading them (at least to the present author, and obviously also the authors of OS], in which a theorem-prover, based exclusively on tableaux, is described). The confusion becomes greater when the reader is introduced to Kowalski's form of a clause ( Ko], Bu]), which is nothing but a Gentzen's sequent of atomic formulae, and when he realizes that resolution is just a form of a Cut, and so that while the elimination of cuts is the principal tool in proof-theory, its use is the main technique in AD!

Propositional canonical Gentzen-type systems, introduced in [2], are systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a connective is introduced and no other connective is mentioned. [2] provides a constructive coherence criterion for the non-triviality of such systems and shows that a system of this kind admits cut-elimination iff it is coherent. The semantics of such systems is provided using two-valued non-deterministic matrices (2Nmatrices). [23] extends these results to systems with unary quantifiers of a very restricted form. In this paper we substantially extend the characterization of canonical systems to (n, k)-ary quantifiers, which bind k distinct variables and connect n formulas, and show that the coherence criterion remains constructive for such systems. Then we focus on the case of k ∈ {0, 1} and show that the following statements concerning a canonical calculus G are equivalent: (i) G is coherent, (ii) G has a strongly characteristic 2Nmatrix, and (iii) G admits strong cut-elimination. We also show that coherence is not a necessary condition for standard cut-elimination, and then characterize a subclass of canonical systems for which this property does hold.

We introduce a general framework for solving the problem of a computer collecting and combining information from various sources. Unlike previous approaches to this problem, in our framework the sources are allowed to provide information about complex formulae too. This is enabled by the use of a new tool — non-deterministic logical matrices. We also consider several alternative plausible assumptions concerning the framework. These assumptions lead to various logics. We provide strongly sound and complete proof systems for all the basic logics induced in this way

The notion of a bilattice was rst introduced by Ginsburg (see Gin]) as a general framework for a diversity of applications (such as truth maintenance systems, default inferences and others). The notion was further investigated and applied for various purposes by Fitting (see Fi1]- Fi6]). The main idea behind bilattices is to use structures in which there are two (partial) order relations, having di erent interpretations. The two relations should, of course, be connected somehow in order for the mathematical structure to be useful. It is not clear, however, what this connection should be. Ginsberg, for example, has made the connection through an extra operation of negation. Fitting, on the other hand, has investigated connections in the form of conditions on the structure (such as being interlaced { see below). These conditions are independent of the existence, or even the possibility to de ne, operations like Ginsberg's negation.* Fitting de nes, accordingly, notions like \an interlaced bilattice", \a distributive bilattice", \a bilattice with negation" and others. He does not provide, however, any de nition of the notion of bilattice itself (without an extra modi er). I was unable to nd anywhere, in fact, a de nition which will cover all the structures which were called \bilattice" in the literature

A paraconsistent logic is a logic which allows non-trivial inconsistent theories. One of the oldest and best known approaches to the problem of designing useful paraconsistent logics is da Costa’s approach, which seeks to allow the use of classical logic whenever it is safe to do so, but behaves completely differently when contradictions are involved. da Costa’s approach has led to the family of Logics of Formal (In)consistency (LFIs). In this paper we provide non-deterministic semantics for a very large family of first-order LFIs (which includes da Costa’s original system..

Many efforts have been made in recent years to construct formal systems for mechanizing general mathematical reasoning. Most of these systems are based on logics which are stronger than first-order logic. However, there are good reasons to avoid using full second-order logic for this task. In this work we investigate a logic which is intermediate between FOL and SOL, and seems to be a particularly attractive alternative to both: ancestral logic. This is the logic which is obtained from FOL by augmenting it with the transitive closure operator. While the study of this logic has so far been mostly model-theoretical, this work is devoted to its proof theory. Two natural Gentzen-style proof systems for ancestral logic are presented: one for the reflexive transitive closure, and one for the non-reflexive one. We show that these systems are sound for ancestral logic and provide evidence that they indeed encompass all forms of reasoning for this logic that are used in practice. The two systems are shown to be equivalent by providing translation algorithms between them. We end with an investigation of two main proof-theoretical properties: cut elimination and constructive consistency proof.

Linear logic is a new logic which was recently developed by Girard in order to provide a logical basis for the study of parallelism. It is described and investigated in Gi]. Girard's presentation of his logic is not so standard. In this paper we shall provide more standard proof systems and semantics. We shall also extend part of Girard's results by investigating the consequence relations associated with Linear Logic and by proving corresponding str ong completeness theorems. Finally, we shall investigate the relation between Linear Logic and previously known systems, especially Relevance logics

The notion of bilattice was introduced by Ginsberg, and further examined by Fitting, as a general framework for many applications. In the present paper we develop proof systems, which correspond to bilattices in an essential way. For this goal we introduce the notion of logical bilattices. We also show how they can be used for efficient inferences from possibly inconsistent data. For this we incorporate certain ideas of Kifer and Lozinskii, which happen to suit well the context of our work. The outcome are paraconsistent logics with a lot of desirable properties.1