Abstract

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 variable-sharing property. SR$_m$ has also the interesting property that classical logic has a strong translation into it. We next 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 will be exactly one designated element, while the addition of the contraction axiom corresponds to the condition that there will be exactly one nondesignated element. Various other systems in which multiplicative conjunction functions as a true conjunction are studied, together with their algebraic counterparts.