[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)