Multiplicative conjunction

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

The following paper is available by anonymous ftp:

                        CONTRACTION AND WEAKENING

 We show that the elimination rule for the multiplicative (or intensional) 
conjunction $\wedge$ is admissible in many important multiplicative 
logics. These include $LL_m$ (the multiplicative fragment of Linear Logic)
and $RMI_m$ (the system obtained from $LL_m$ by adding the contraction axiom
and its converse, the mingle axiom.) An exception is $R_m$ (the intensional
fragment of the relevance logic $R$, which is $LL_m$ together with the
contraction axiom). 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 (in the first
case we get the system $BCK_m$, in the second - the system $SR_m$). Various 
other systems in which multiplicative conjunction functions as a true 
conjunction are studied, together with their algebraic counterparts.


This paper can be retrieved by anonymous ftp using the instructions below.
If you want a copy but cannot use ftp to this site, send me
(aa@math.tau.ac.il) your postal address.

% ftp ftp.math.tau.ac.il
Name: anonymous
Password:  <<your e-mail address>>
ftp> cd /pub/aa
ftp> get mult_algeb.ps.gz
ftp> quit

use gunzip to uncompress the file before printing it.

Arnon Avron