[L7] _________________________ AMAST Links 02 05

Undecidability of Non-Commutative 2nd Order Multiplicative Linear Logic

by Martin Emms

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