Article details

Research area
Natural language & AI

Florida, USA


Harley Eades III, Valeria de Paiva

Multiple Conclusion Linear Logic: Cut-elimination and more


Full Intuitionistic Linear Logic (FILL) was first introduced
by Hyland and de Paiva, and went against current beliefs that it was not
possible to incorporate all of the linear connectives, e.g. tensor, par, and
implication, into an intuitionistic linear logic. It was shown that their
formalization of FILL did not enjoy cut-elimination by Bierman, but
Bellin proposed a change to the definition of FILLĀ  to regain
cut-elimination. In this note we adopt Bellin’s proposed change and give a
direct proof of cut-elimination. Then we show that a categorical model of
FILL in the basic dialectica category is also a LNL model of Benton and
a full tensor model of Mellies’ and Tabareau’s tensorial logic. Lastly, we
give a double-negation translation of linear logic into FILL that explicitly
uses par in addition to tensor.
Read/download now