Abstract

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