Decision Problems For Second Order Linear Logic

           Decision Problems For Second Order Linear Logic

        Patrick Lincoln, Andre Scedrov, and Natarajan Shankar

Relating to the study of polymorphic languages based on linear logic, we have 
been studying fragments of second order linear logic. The main surprise is 
that the structural rules of contraction and weakening may be simulated by 
second order propositional quantifiers and the multiplicatives. 

Let M stand for multiplicatives, A for additives, E for exponentials, 
1 for first order quantifiers, 2 for second order quantifiers, and I for 
"intuitionistic" version of linear logic fragments.  LJ2 is second order 
intuitionistic propositional logic, shown undecidable by Loeb 
[JSL 41 (1976) 705-718] and Gabbay.  LK12 is second order classical
predicate logic.

1) IMLL2 is undecidable.
2) MLL12 is undecidable. 

The first main result is obtained by the following encoding of LJ2:  => gets 
-o, forall gets forall. Let us call this encoding []. Let us write * for 
tensor. Define C = (forall X. X -o X*X) and W = (forall X. X -o 1). Then    
Sigma |- A  is provable in LJ2 iff  C,C,C,W,[Sigma] |- [A]  is provable in 
IMLL2. Note that faithfulness is straightforward because C and W are both 
translations of provable LJ2 formulas, so one can use cut to produce a LJ2 
proof of Sigma |- A. LK12 can be similarly embedded in MLL12. 
It readily follows from the argument that IMALL2 and MALL12 are undecidable. 

The main open problems along these lines is the decidability of MLL2 and 
MALL2. The constructions we use for the "intuitionistic" versions do not 
apply in these cases. (The undecidability of MELL2 should follow from Girard's
translation of LJ2). Of course, the decidability of (quantifier-free) MELL 
is still an open question.