Arnon Avron

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.

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.

There is a long tradition (See e.g. [9, 10]) starting from [12], according to which the meaning of a connective is determined by the introduction and elimination rules which are associated with it. The supporters of this thesis usually have in mind natural deduction systems of a certain ideal type (explained in Section 3 below). Unfortunately, already the handling of classical negation requires rules which are not of that type. This problem can be solved in the framework of multiple-conclusion Gentzen-type systems (also first introduced in [12]), where instead of introduction and elimination rules there are left introduction rules and right introduction rules.

We suggest a new framework for the Weyl-Feferman predicativist program by constructing a formal predicative set theory P ZF which resembles ZF, and is suitable for mechanization. The basic idea is that the predicatively acceptable instances of the comprehension schema are those which determine the collections they define in an absolute way, independent of the extension of the “surrounding universe”. The language of P ZF is type-free, and it reflects real mathematical practice in making an extensive use of statically defined abstract set terms. Another important feature of P ZF is that its underlying logic is ancestral logic (i.e. the extension of first-order logic with a transitive closure operation)

Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with unary quantifiers and show that it remains constructive. Then we provide semantics for such canonical systems using 2-valued non-deterministic matrices extended to languages with quantifiers, and prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix.

According to Suszko's Thesis,any multi-valued semantics for a logical system can be replaced by an equivalent bivalent one. Moreover: bivalent semantics for families of logics can frequently be developed in a modular way. On the other hand bivalent semantics usually lacks the crucial property of analycity, a property which is guaranteed for the semantics of multi-valued matrices. We show that one can get both modularity and analycity by using the semantic framework of multi-valued non-deterministic matrices. We further show that for using this framework in a constructive way it is best to view "truth-values" as information carriers, or "information-values"

Hypersequents are finite sets of ordinary sequents. We show that multiple-conclusion sequents and single-conclusion hypersequents represent two different natural methods of switching from a single-conclusion calculus to a multiple-conclusion one. The use of multiple-conclusion sequents corresponds to using a multiplicative disjunction, while the use of single-conclusion hypersequents corresponds to using an additive one. Moreover: each of the two methods is usually based on a different natural semantic idea and accordingly leads to a different class of algebraic structures. In the cases we consider here the use of multiple-conclusion sequents corresponds to focusing the attention on structures in which there is a full symmetry between the sets of designated and antidesignated elements. The use of single-conclusion hypersequents, on the other hand, corresponds to the use of structures in which all elements except one are designated. Not surprisingly, the use of multiple-conclusion hypersequents corresponds to the use of structures which are both symmetrical and with a single nondesignated element.

Paradefinite logics are logics that can be used for handling contradictory or partial information. As such, paradefinite logics should be both paraconsistent and paracomplete. In this paper we consider the simplest semantic framework for introducing paradefinite logics. It consists of the four-valued matrices that expand the minimal matrix which is characteristic for first degree entailments: Dunn–Belnap matrix. We survey and study the expressive power and proof theory of the most important logics that can be developed in this framework.

It is well known that every propositional logic which satisfies certain very natural conditions can be characterized semantically using a multi-valued matrix ([Los and Suszko, 1958; W´ ojcicki, 1988; Urquhart, 2001]). However, there are many important decidable logics whose characteristic matrices necessarily consist of an infinite number of truth values. In such a case it might be quite difficult to find any of these matrices, or to use one when it is found. Even in case a logic does have a finite characteristic matrix it might be difficult to discover this fact, or to find such a matrix. The deep reason for these difficulties is that in an ordinary multi-valued semantics the rules and axioms of a system should be considered as a whole, and there is no method for separately determining the semantic effects of each rule alone.

We provide a general investigation of Logic in which the notion of a simple consequence relation is taken to be fundamental. Our notion is more general than the usual one since we give up monotonicity and use multisets rather than sets. We use our notion for characterizing several known logics (including Linear Logic and non-monotonic logics) and for a general, semantics-independent classi cation of standard connectives via equations on consequence relations (these include Girard's \multiplicatives" and \additives"). We next investigate the standard methods for uniformly representing consequence relations: Hilbert type, Natural Deduction and Gentzen type. The advantages and disadvantages of using each system and what should be taken as..

We present a new unified framework for formalizations of axiomatic set theories of different strength, from rudimentary set theory to full ZF. It allows the use of set terms, but provides a static check of their validity. Like the inconsistent “ideal calculus” for set theory, it is essentially based on just two set-theoretical principles: extensionality and comprehension (to which we add ∈-induction and optionally the axiom of choice). Comprehension is formulated as: x ∈ {x | ϕ} ↔ ϕ, where {x | ϕ} is a legal set term of the theory. In order for {x | ϕ} to be legal, ϕ should be safe with respect to {x}, where safety is a relation between..

Around 1950, B.A. Trakhtenbrot proved an important undecidability result (known, by a pure accident, as \Trakhtenbrot's theorem"): there is no algorithm to decide, given a rst-order sentence, whether the sentence is satis able in some nite model. The result is in fact true even if we restrict ourselves to languages that has only one binary relation Tra63]. It is hardly conceivable that at that time Prof. Trakhtenbrot expected his result to in uence the development of the theory of relational databases query languages, but it did. This perhaps is not surprising in view of the following two facts: 1) The theory of relational databases is strongly rooted in logic and can easily be abstracted to make it a branch of mathematical logic. 2) The main interest in the theory of relational databases is in nite relations. In the rst section we explain those two points in more detail. Then, in section 2 of the present paper, we discuss the question: \What constitutes a reasonable query to a database?" The discussion naturally leads to a certain class of queries, known as the \domain independent" queries, as an ideal query language. At this point Trakhtenbrot's theorem appears as a major obstacle, since it easily implies that this ideal class is undecidable. Real query languages cannot be allowed to have this property. Section 3 outlines then several possible ways to circumvent this di culty. The following section explains the..

Non-deterministic matrices are multiple-valued structures in which the value assigned by a valuation to a complex formula can be chosen non-deterministically out of a certain nonempty set of options. We consider two different types of semantics which are based on Nmatrices: the dynamic one and the static one. We use the Rasiowa-Sikorski decomposition methodology to get sound and complete proof systems employing finite sets of mv-signed formulas for all propositional logics based on such structures with either of the above types of semantics. Later we demonstrate how these systems can be converted into cut-free ordinary Gentzen calculi which are also sound and complete for the corresponding non-deterministic semantics. As a by-product, we get new semantic characterizations for some well-known logics.

This paper has two goals. First, we develop frameworks for logical systems which are able to reflect not only non-monotonic patterns of reasoning, but also paraconsistent reasoning. Our second goal is to have a better understanding of the conditions that a useful relation for nonmonotonic reasoning should satisfy. For this we consider a sequence of generalizations of the pioneering works of Gabbay, Kraus, Lehmann, Magidor and Makinson. These generalizations allow the use of monotonic nonclassical logics as the underlying logic upon which nonmonotonic reasoning may be based. Our sequence of frameworks culminates in what we call plausible, nonmonotonic, multiple-conclusion consequences relations. Our study yields intuitive justifications for conditions that have been proposed in previous frameworks and also clarifies the connections among some of these systems. In addition, we present a general method for constructing plausible nonmonotonic relations. This method is based on a multiple-valued semantics, and on Shoham's idea of preferential models.

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 quasi-canonical Gentzen-type system is a Gentzen-type system in which each logical rule introduces either a formula of the form, or of the form, and all the active formulas of its premises belong to the set. In this paper we investigate quasi-canonical systems in which exactly one of the two classical rules for negation is included, turning the induced logic into either a paraconsistent logic or a paracomplete logic, but not both. We provide a constructive coherence criterion for such systems, and show that a quasi-canonical system of the type we investigate is coherent iff it is strongly paraconsistent or strongly paracomplete (in a sense defined in the paper), iff it has a trivalent, non-deterministic semantics of a special type (also defined in the paper) for which it is sound and complete. Finally, we determine when a system of this sort admits cut-elimination, and provide a simple procedure for transforming one which does not into one which does.