[L8] ================================================ AMAST Links 02 05

Undecidability of Non-Commutative 2nd Order Multiplicative Linear Logic 
                            by Max Kanovich

   The full version of this contribution is available at URL:
   http://www.cs.utwente.nl/data/amast/links/v02/i05/full/AC0205L8.txt

  In referring to linear logic fragments let N stand for noncommutative
versions (with "\" and "/" being left and right implications,
respectively, and "*" being non-commutative product),
   M for multiplicatives, 
   A for additives,
   E for exponentials,
   2 for second order quantifiers, and
   I for "intuitionistic" version of linear logic fragments.  

  Lincoln, Scedrov, and Shankar showed the undecidability of IMLL2 and
IMALL2 by embedding of LJ2 (announced in the Types forum, to appear in
LICS'95).
  Lafont has proved the undecidability of MALL2 (announced in the Types
forum, to appear in the Journal of Symbolic Logic).
  Recently, Lafont & Scedrov proved that MLL2 is undecidable (announced
in the Types forum).

  As for non-commutative linear logic,
 o  Emms shows embedding of LJ2 into N-IMLL2 as well,
 o  Kanovich proved the undecidability of Lambek calculus enriched by
    the exponential !, and thereby the undecidability of N-MELL.

  Here (see full version of the contribution) we prove that classical
N-MLL2 is also undecidable.