[Prev][Next][Index][Thread]
MLL2 is undecidable
The Undecidability of Second Order Multiplicative Linear Logic
Yves Lafont and Andre Scedrov
Abstract
In referring to linear logic fragments, let M stand for multiplicatives,
A for additives, 2 for second order quantifiers, and I for "intuitionistic"
version of linear logic fragments.
Lincoln, Scedrov, and Shankar showed the undecidability IMLL2 and IMALL2
(announced in this forum, to appear in LICS '95). Lafont has subsequently
proved the undecidability of MALL2 (announced in this forum, to appear in
the Journal of Symbolic Logic). It is the case that MLL2 is undecidable.
Consider
#A = A * (A -o 1)
and
D = Forall X Forall Y (#X * #Y -o X * X * #Y * Y).
The formula D may be used to encode a restricted kind of contraction.
Indeed, the rules
Gamma |- B D^2, #A, A, Gamma |- B
------------------------- ------------------------
D^2, #Theta, Gamma |- B D^2, #A, Gamma |- B
are derivable. Also, D holds in any phase model in which {1} is
closed under double orthogonal (i.e., the singleton {1} is a "fact")
and in which 1 is the only invertible element of the commutative
monoid underlying the phase model.
A register machine configuration (i,p,q) consisting of a state i,
first counter value p, and second counter value q, is encoded as
b_i * F[a^p] * G[a^q], where b_i is an atom, a^p is the p-fold
tensor of a's, and the formulas F and G are defined as follows:
F[X] = X^3 * (X -o d) * (X -o e) -o f ,
G[X] = X^3 * (X -o d) * (X -o e) -o g ,
where d,e,f,g are atoms. For instance, first counter increment
is encoded as Forall X (b_i * F[X] -o b_j * F[a*X]), zero test as
b_i * F[1] -o b_k * F[1], and similarly for the other transitions.
Theorem. Let T_1, ..., T_n be the formulas encoding the machine
transitions. The following are equivalent:
1. A machine configuration id (i,p,q) is accepted,
2. The sequent
D^2, #T_1, ..., #T_n, b_i * F[a^p] * G[a^q] |- b_0 * F[1] * G[1]
is provable in IMLL2,
3. The above sequent is provable in MLL2.
The direction 1 -> 2 does not depend on the particular choice of F,G.
The difficult part, 3 -> 1, uses a particular phase model constructed
to represent exactly the accepted configurations.