[Prev][Next][Index][Thread]

MLLW2 is undecidable



              Second order  Linear Affine Logic is Undecidable.
                               Alexei Kopylov

 In referring to linear logic fragments,
   N stands for non-commutative versions
     (with -o and o- being left and right implications, respectively,
     and "*" being non-commutative product),
   M for multiplicative fragment,
   A for additive fragment,
   2 for second order quantifiers, and
   I for "intuitionistic" version of linear logic fragments,
   W for Linear Logic with the weakening rule (called Linear Affine Logic).


 Lincoln, Scedrov, and Shankar showed the undecidability of IMLL2 and IMALL2
 by embedding of LJ2 (announced in this forum, LICS '95).
 Lafont has proved the undecidability of MALL2 (announced in this forum, to
 appear in the Journal of Symbolic Logic).
 Recently, Lafont and Scedrov proved that MLL2 is undecidable (announced in
 this forum).
 Emms shows embedding of LJ2 into N-IMLL2 as well.
 Kanovich demonstrated the undecidability of N-MLL2 and second order
 Lambek Calculus (LC2). (Announced in this forum).

 Here we prove that MLLW2 is also undecidable. The main ideas of the proof is
 similar to ideas in Lafont and Scedrov's paper. Namely, we encode two counter
 machines (Minsky machines) in LLW2. In order to obtain the faithfulness of
 the encoding we use the phase semantic. But here we need the phase semantic
 for linear affine logic. So, we introduce such semantic.

 Let we have a phase space (M,\bot), where M is a commutative monoid, and \bot
 is a subset of M. We say that the phase space (M,\bot) is suitable for LLW if
 M*\bot=\bot.

 Theorem.  If a formula A is derivable in MALLW2, then any phase space
 (M,\bot) which is suitable for LLW satisfies A.

 We can encode Minsky machines by the following way. Let us consider two
 formulas:
    F[x]=(x -o f) -o h,     G[x]=(x -o g) -o e.
 Then we construct the following infinite sets of formulas:
    F_0=F[a],  F_1=F[F[a]], ....,  F_n=F[F_{n-1}]
    G_0=G[b],  G_1=G[G[b]], ....,  G_n=G[G_{n-1}]
 Any machine configuration (i,p,q) is encoded by the following formula:
    c_i * F_p * G_q.
 Here a, b, c_i, e, f, g, h are literals.
 A increment transition (i,p,q) -> (j,p+1,q) is encoded by the formula
    \forall x,y (c_i * F[x] * G[y]  -o  c_j * F[F[x]] * G[y]).
 A decrement transition (i,p,q) -> (j,p-1,q), if p>0 is encoded by the formula
    \forall x,y (c_i * F[F[x]] * G[y]  -o  c_j * F[x] * G[y]).
 And a test-for-zero transition (i,0,q) -> (k,0,q) is encoded by the formula
    \forall y   (c_i * F[a] * G[y]  -o  c_k * F[a] * G[y].
 By analogous for the second register transitions (i,p,q) -> (j,p,q+1);
 (i,p,q) -> (j,p,q-1), if q>0; and (i,p,0) -> (k,p,0) are encoded by the
 following formulas
    \forall x,y (c_i * F[x] * G[y]  -o  c_j * F[x] * G[G[y]]).
    \forall x,y (c_i * F[x] * G[G[y]]  -o  c_j * F[x] * G[y]).
    \forall x   (c_i * F[x] * G[b]  -o  c_k * F[x] * G[b].
 Let \Gamma be a set of formulas of the above kind which encode all
 transitions of our machine.

 Theorem.  The following three assertions are equivalent:
   (i) The configuration (i,p,q) is accepted by the machine.
  (ii) The following sequent is derivable in MLLW2:
           c_i * F_p * G_q, \Gamma^4, C^5   |-   c_0 * F_0 * G_0
       where C=\forall x (x^4 -o x^5). Here x^n means x*x*...*x (n times),
       and \Gamma^n means {A^n | A in G}.
 (iii) The above sequent is derivable in MALLW2.

 Ptoof.
    (i) => (ii).  By induction on the length of the computation.
   (ii) => (iii). This implication is trivial.
  (iii) => (i).   By means of phase space.

 Moreover, if we add in our sequent the formula W=\forall x,y,z (x*y*z -o y),
 then we obtain a stronger theorem:

 Theorem.  The following four assertions are equivalent:
   (1) The configuration (i,p,q) is accepted by the machine.
   (2) The following sequent is derivable in LC2:
 c_i*F_p*G_q, \Gamma, W, \Gamma, W, \Gamma, W, \Gamma, W, C'^5, W |- c_0*F_0*G_0
       where C'=\forall x (x^4 -o x^6).
   (3) The above sequent is derivable in any logic L, such that L is a subset
       of LLW2, and a superset of LC2.
   (4) This sequent is derivable in LLW2.

 Proof.
   (1) => (2).  By induction on the length of the computation.
   (2) => (3), (3) => (4). These implications are trivial.
   (4) => (1).  By means of phase space.

 As a corollary, we get the undecidability of all logics described in the
 item (3). The undecidability of some of these logics are already known:
 IMLL2, IMALL2 (Lincoln, Scedrov and Shankar), MALL2 (Lafont), MALL2 (Lafont
 and Scedrov), N-IMLL2 (Emms), N-MLL2, LC2 (Kanovich). Additionally we obtain
 some new undecidability results. For example, MLLW2, MALLW2, LLW2, IMLLW2,
 N-IMLLW2 and so on.

 Best regards,
 Alexei Kopylov.