The undecidability of second order multiplicative linear logic (Q1917079)

The authors show that the multiplicative fragment of second-order propositional linear logic is undecidable. In referring to linear logic fragments, we use the standard conventions: M stands for multiplicatives, A for additives, E for exponentials, 1 for first order quantifiers, 2 for second-order propositional quantifiers, and I for the intuitionistic version. Decision problems for propositional (quantifier-free) linear logic were first studied by \textit{P. Lincoln}, \textit{J. Mitchell}, \textit{A. Scedrov}, and \textit{N. Shankar} [Ann. Pure Appl. Logic 56, 239-311 (1992; Zbl 0768.03003)]. They showed that full propositional linear logic is undecidable and that MALL is PSPACE-complete. The NP-completeness of MLL has been obtained by \textit{M. I. Kanovich} [Ann. Pure Appl. Logic 69, 195-241 (1994; Zbl 0812.03007)]. Related results have been obtained by Lincoln, Scedrov, Shankar, and Winkler. \textit{G. Amiot} showed the undecidability of MLL12 and MALL12 with function symbols [PhD. thesis, University of Paris 7 (1994)]. More recently, \textit{P. Lincoln}, \textit{A. Scedrov}, and \textit{N. Shankar} showed the undecidability of IMLL2 and IMALL2, and the undecidability of MLL12 and MALL12 without function symbols [Proc. 10th Annual IEEE Symp. on Logic in Computer Science, San Diego, California, 476-485 (1995)]. The present author then proved the undecidability of MALL2 [J. Symb. Logic 61, No. 2, 541-548 (1996)]. To establish the undecidability of MLL2, the authors combine the key ideas of the last two papers: an encoding of contraction using second-order quantifiers instead of exponentials (by Lincoln, Scedrov, and Shankar), and the use of the phase semantics to show that the counter machines are faithfully encoded into the logic (by Lafont). Because of the absence of additives, the encoding is a bit more complicated than in the previous papers.