[Prev][Next][Index][Thread]
Multiplicative conjunction
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
The following paper is available by anonymous ftp:
MULTIPLICATIVE CONJUNCTION AND THE ALGEBRAIC MEANING OF
CONTRACTION AND WEAKENING
We show that the elimination rule for the multiplicative (or intensional)
conjunction $\wedge$ is admissible in many important multiplicative
substructural
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