A PSPACE-complete fragment of Second Order Linear Logic

Existentially quantified variables are the source of non decidability for second order linear logic without exponentials (MALL2). We present a decision procedure for a fragment of MALL2 based on a canonical instantiation of these variables and using inference permutability in proofs. We also establish that this fragment is PSPACE-complete. Introduction The decision problem for second order linear logic without exponentials (MALL2) has given rise recently to many papers and results. P. Lincoln, A. Scedrov and N. Shankar have shown that the multiplicative fragment of second order intuitionistic linear logic (IMLL2) is undecidable by encoding second order intuitionistic propositional logic --- known to be undecidable --- into IMLL2 [10]. M. Emms has extended this strategy to prove the undecidability of the second order Lambek Calculus (L2) [3], which can be viewed as the multiplicative fragment of intuitionistic non-commutative linear logic. The undecidability of MALL2 has been show..