Abstract
This article defines and studies a natural deduction system for partially commutative intuitionistic multiplicative linear logic, that is a combination of intuitionistic commutative linear logic with the Lambek calculus, which is non- commutative, and was first introduced as a sequent calculus by de Groote. In this logic, the hypotheses are endowed with a series-parallel partial order: the parallel composition corresponds to the commutative product, while the series composition corresponds to the noncommutative product. The relation between the two products is that a rule, called entropy, allows us to replace a series-parallel order with a sub series-parallel order -- this rule (already studied by Retoré) strictly extends the entropy rule initially introduced by de Groote. A particular subsystem emerges when hypotheses are totally ordered: this is Lambek calculus with product, and when orders are empty it is is multiplicative linear logic. So far only the sequent calculus and cut-elimination have been properly studied. In this article, we define natural deduction with product elimination rules as Abramsky proposed long ago. We then give a brief illustration of its application to computational linguistics and prove normalisation, firstly for the Lambek calculus with product and then for the full partially ordered calcu- lus. We show that normal proofs enjoy the subformula property, thus yielding another proof of decidability of these calculi. This logic was shown to be useful for modelling the truly concurrent exe- cution of Petri nets and for minimalist grammars in computational linguistics. Regarding this latter application, natural deduction and the Curry-Howard iso- morphism is extremely useful since it leads to the semantic representation of analysed sentences.