[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.

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 ïntuitionistic" 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,

• Emms shows embedding of LJ2 into N-IMLL2 as well,
• 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.