# Arnon Avron

Tel Aviv, Israel
Areas of Interest
•  11
##### Multiplicative Conjunction and an Algebraic Meaning of Contraction and Weakening Journal of Symbolic Logic 63 (3): 831-859. 1998.
We show that the elimination rule for the multiplicative conjunction \$\wedge\$ is admissible in many important multiplicative substructural logics. These include LL\$_m\$ and RMI\$_m\$ An exception is R\$_m\$. Let SLL\$_m\$ and SR\$_m\$ be, respectively, the systems which are obtained from LL\$_m\$ and R\$_m\$ by adding this rule as a new rule of inference. The set of theorems of SR\$_m\$ is a proper extension of that of R\$_m\$, but a proper subset of the set of theorems of RMI\$_m\$. Hence it still has the variabl…Read more
•  97
##### What is relevance logic? Annals of Pure and Applied Logic 165 (1): 26-48. 2014.
We suggest two precise abstract definitions of the notion of ‘relevance logic’ which are both independent of any proof system or semantics. We show that according to the simpler one, R → source is the minimal relevance logic, but R itself is not. In contrast, R and many other logics are relevance logics according to the second definition, while all fragments of linear logic are not
•  41
•  59
##### Implicational f-structures and implicational relevance logics Journal of Symbolic Logic 65 (2): 788-802. 2000.
We describe a method for obtaining classical logic from intuitionistic logic which does not depend on any proof system, and show that by applying it to the most important implicational relevance logics we get relevance logics with nice semantical and proof-theoretical properties. Semantically all these logics are sound and strongly complete relative to classes of structures in which all elements except one are designated. Proof-theoretically they correspond to cut-free hypersequential Gentzen-ty…Read more
•  25
##### Tonk- A Full Mathematical Solution
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 G…Read more
•  37
##### Four-Valued Paradefinite Logics with Ofer Arieli Studia Logica 105 (6): 1087-1122. 2017.
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 logi…Read more
•  100
##### Cut-free ordinary sequent calculi for logics having generalized finite-valued semantics with Jonathan Ben-Naim and Beata Konikowska Logica Universalis 1 (1): 41-70. 2007.
.  The paper presents a method for transforming a given sound and complete n-sequent proof system into an equivalent sound and complete system of ordinary sequents. The method is applicable to a large, central class of (generalized) finite-valued logics with the language satisfying a certain minimal expressiveness condition. The expressiveness condition decrees that the truth-value of any formula φ must be identifiable by determining whether certain formulas uniformly constructed from φ have des…Read more
•  68
•  54
##### A Non-deterministic View on Non-classical Negations Studia Logica 80 (2-3): 159-194. 2005.
We investigate two large families of logics, differing from each other by the treatment of negation. The logics in one of them are obtained from the positive fragment of classical logic (with or without a propositional constant ff for “the false”) by adding various standard Gentzen-type rules for negation. The logics in the other family are similarly obtained from LJ+, the positive fragment of intuitionistic logic (again, with or without ff). For all the systems, we provide simple semantics whic…Read more
•  1
##### A Formula-Preferential Base for Paraconsistent and Plausible Reasoning Systems with Iddo Lev In Arnon Avron & Iddo Lev (eds.), Proceedings of the Workshop on Inconsistency in Data and Knowledge, . pp. 60-70. 2001.
We provide a general framework for constructing natural consequence relations for paraconsistent and plausible nonmonotonic reasoning. The framework is based on preferential systems whose preferences are based on the satisfaction of formulas in models. We show that these natural preferential In the research on paraconsistency, preferential systems systems that were originally designed for for paraconsistent reasoning fulfill a key condition (stopperedness or smoothness) from the theoretical res…Read more
•  42
##### Multi-valued Semantics: Why and How Studia Logica 92 (2): 163-182. 2009.
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-determinis…Read more
•  26
##### Cut-Elimination and Quantification in Canonical Systems with Anna Zamansky Studia Logica 82 (1): 157-176. 2006.
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 n…Read more
•  7
##### LFIs with Marco's Schema
We construct a modular semantic frameworks for LFIs (logics of formal (in)consistency) which extends the framework developed in [1; 3], but includes Marco’s schema too (and so practically all the axioms considered in [11] plus a few more). In addition, the paper provides another demonstration of the power of the idea of nondeterministic semantics, especially when it is combined with the idea of using truth-values to encode relevant data concerning propositions
•  33
##### Two types of multiple-conclusion systems Logic Journal of the IGPL 6 (5): 695-718. 1998.
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 s…Read more
•  44
•  20
##### Formulas for which contraction is admissible Logic Journal of the IGPL 6 (1): 43-48. 1998.
A formula A is said to have the contraction property in a logic L if whenever A, A, Γ ⊨ L B also A, Γ &amp; ; L B. In MLL and in MALL without the additive constants a formula has the contraction property if it is a theorem. Adding the mix rule does not change this fact. In MALL and in affine logic A has the contraction property if either A is provable of A is equivalent to the additive constant 0. We present some general proof-theoretical principles from which all these results easily follow
•  15
##### Simple Consequence Relations
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 \multiplicati…Read more
•  17
•  113
•  21
##### A New Approach to Predicative Set Theory In Ralf Schindler (ed.), Ways of Proof Theory, De Gruyter. pp. 31-64. 2010.
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 deﬁne in an absolute way, independent of the extension of the “surrounding universe”. The language of P ZF is type-free, and it reﬂects real mathematical practice in making an extensi…Read more
•  62
•  27
##### Multi-valued Calculi for Logics Based on Non-determinism with Beata Konikowska Logic Journal of the IGPL 13 (4): 365-387. 2005.
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 structu…Read more
•  5
##### What reasonable first-order queries are permitted by Trakhtenbrot's theorem?
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 dat…Read more
•  256
•  7
##### Implicational F-Structures and Implicational Relevance Logics Journal of Symbolic Logic 65 (2): 788-802. 2000.
We describe a method for obtaining classical logic from intuitionistic logic which does not depend on any proof system, and show that by applying it to the most important implicational relevance logics we get relevance logics with nice semantical and proof-theoretical properties. Semantically all these logics are sound and strongly complete relative to classes of structures in which all elements except one are designated. Proof-theoretically they correspond to cut-free hypersequential Gentzen-ty…Read more
•  22
##### The Classical Constraint on Relevance Logica Universalis 8 (1): 1-15. 2014.
We show that as long as the propositional constants t and f are not included in the language, any language-preserving extension of any important fragment of the relevance logics R and RMI can have only classical tautologies as theorems . This property is not preserved, though, if either t or f is added to the language, or if the contraction axiom is deleted
•  119
##### Ideal Paraconsistent Logics with O. Arieli and A. Zamansky Studia Logica 99 (1-3): 31-60. 2011.
We define in precise terms the basic properties that an ‘ideal propositional paraconsistent logic’ is expected to have, and investigate the relations between them. This leads to a precise characterization of ideal propositional paraconsistent logics. We show that every three-valued paraconsistent logic which is contained in classical logic, and has a proper implication connective, is ideal. Then we show that for every n > 2 there exists an extensive family of ideal n -valued logics, each one of …Read more
•  34
##### Decomposition proof systems for gödel-Dummett logics with Beata Konikowska Studia Logica 69 (2): 197-219. 2001.
The main goal of the paper is to suggest some analytic proof systems for LC and its finite-valued counterparts which are suitable for proof-search. This goal is achieved through following the general Rasiowa-Sikorski methodology for constructing analytic proof systems for semantically-defined logics. All the systems presented here are terminating, contraction-free, and based on invertible rules, which have a local character and at most two premises
•  8