LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
11.00, Friday 18th April 1997

** NOTE NONSTANDARD DAY AND TIME (Semantics & Logic Club Slot) **

Title: Multiplicative Conjunction, Contraction and Weakening

Speaker: Arnon Avron (Tel Aviv University, Israel)

We show that the elimination rule for the multiplicative conjunction is admissible in many important multiplicative substructural logics. These include LL_m (the multiplicative fragment of Linear Logic) and RMI_m (LL_m together with contraction and its converse). An exception is R_m (the multiplicative fragment of the relevance logic R) which is LL_m together with contraction.

Let, SLL_m, SR_m and SRMI_m be, respectively, the systems which are obained from LL_m, R_m and RMI_m by adding the elimination rule of the multiplicative conjunction as a new rule of inference. In these systems the multiplicative conjunction is a real conjunction, since all the standard natural deduction rules for conjunction are valid for it. Now according to the results above, the set of theorems of SLL_m and of SRMI_m are identical to those of LL_m and RMI_m (respectively). The set of theorems of SR_m is, in contast, a proper extension of that of R_m. On the other hand it can be shown to be a proper subset of the set of theorems of $RMI_m$. Now both SR_m and SRMI_m have the interesting property that classical logic has a strong translation into them in which classical conjunction is translated into the multiplicative conjunction. Moreover: both systems have corresponding cut-free Gentzen-type formulations. These formulations employ hypersequents (finite sets of ordinary sequents) rather than usual sequents. It follows that these systems are rather interesting from a proof-theoretical point of view.

In order to show that the systems with the extra rule are also interesting from a semantical point of view, we introduce general algebraic structures, called strong multiplicative structures, and prove strong soundness and completeness of SLL_m relative to them. We show that in the framework of these structures, the addition of the weakening axiom to SLL_m corresponds to the condition that there is exactly one designated element, while the addition of the contraction axiom corresponds to the condition that there is exactly one nondesignated element. In the first case we get the system BCK_m, in the second - the system SR_m. Adding also a condition of flatness yields a sound and complete semantics for SRMI_m. In the case of SRMI_m this semantics leads to a decision procedure. The decision problem for SR_m is still open, though. other systems in which multiplicative conjunction functions as a true conjunction are studied, together with their algebraic counterparts.