[Prev][Next][Index][Thread]
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
ftp.cis.uni-muenchen.de/pub/incoming/emms/deci.dvi.Z
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