[Prev][Next][Index][Thread]
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.
Theorem.
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.