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

Second order Lambek is undecidable



 Undecidability of the Second Order Lambek Calculus

                    Max Kanovich

 In my previous message on the undecidability of non-commutative
 second order multiplicative linear logic the problem whether the
 second order Lambek calculus is decidable remained open.
 The point is that the Lambek calculus does not allow sequents with
 the empty antecedent, and, in particular, we meet problems with 1
 and Weakening.

 Nevertheless, we can improve constructions from my previous message
 to get also the undecidability for the second order Lambek calculus.

 Let "\" and "/" stand for left and right implications, respectively,
     "*" for non-commutative product.

 We define a 'self-reproductive' formula R as follows:

  R = forall C,A,T ( (C * @C * @A * T * A)/(@C * @A * T) )

 where   
       @B = ( (f/(f*B)) * B)     (f is a fixed atom)

 Minsky machines with two counters x and y are simulated in the
 second order Lambek calculus as follows:

 Any configuration of a given Minsky machine M
                   (l_i,a,b)
 is represented by a formula of the form (where l_i,p,q,b,e are atoms)
            (b * p^a * l_i * q^b * e)
 Atoms b and e designate the end 'markers', the left part represents
 the content of counter x, the right one represents the content of y.

 An instruction of the form
     l_i:  x:=x+1;  goto l_j;
 is axiomatized by:
     forall A,B ( (b * A * p * l_j * B * e)/(b * A * l_i * B * e)).

 An instruction of the form
     l_i:  y:=y-1;  goto l_j;
 is axiomatized by:
     forall A,B ( (b * A * l_j * B * e)/(b * A * l_i * q * B * e)).
 
 A zero-test instruction of the form
     l_i:  if (x=0) then goto l_k;
 is axiomatized by:
     forall B ( (b * l_k * B * e)/(b * l_i * B * e)).
 etc.

 Theorem.
 Let             A_1, A_2, ..., A_n
 be the formulas encoding instructions of M.
 Let Delta be a formula of the form:
   Delta = (R * @R * @A_1 * R * @R * @A_2 * ... * R * @R * @A_n).
 The following sentences are equivalent:
 1. M can go from an initial configuration (l_1,a,b) to the terminal
    configuration (l_0,0,0).
 2. A sequent of the form
     Delta, b, p^a, l_1, q^b, e |- (Delta * b * l_0 * e)
    is derivable in the second order Lambek calculus.
 3. The above sequent is derivable in second order cyclic linear
    logic.

 Proof.
 1 -> 2: By a straightforward induction.
 3 -> 1: The faithfulness of our encoding is proved by means of
         the Girard's phase semantics adapted to the non-commutative
         case.

 As a corollary, we get the undecidability of the second order Lambek
 calculus and second order cyclic multiplicative linear logic as well.

 Remark: In our encoding we use only one of two directed implications,
 namely, /, and product *. We can eliminate *, and prove thereby the
 undecidability of the purely implicational second order Lambek
 calculus.

 Best regards,
 Max Kanovich

(Moderators note: this message was delayed by an oversight on my part.
My apologies to the author for the delay.  -- Patrick Lincoln)