decision problem for non-commutative linear logic

Lincoln, Scedrov and Shankar have shown second order intuitionistic 
multiplicative linear logic to be undecidable, by an embedding of LJ2
into it using 2nd order formulae to recover the lost structural rules
of weakening and contraction. In the paper available by anonymous from


it is shown how in a similar way on can obtain an embedding into the
non-commutative version, so-called polymorphic lambek calculus, and thereby
show undecidability of this calculus.

Martin Emms