Multiplicative Conjunction as an Extensional Conjunction
Arnon Avron · Logic Journal of IGPL · 1997
We show that the rule that allows the inference of A from A ⊗ B is admissible in many of the basic multiplicative (intensional) 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 (= multiplicative linear logic together with contraction and its converse) 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 (= finite sequences of ordinary sequents). Moreover: classical logic has a simple, strong translation into this logic. This translation uses definable connectives and preserves the consequence relation of classical logic (not just the set of theorems). Similar results, but with a 3-valued semantics, obtain if instead of RMIm we use RMm (the purely multiplicative fragment of RM).