[Prev][Next][Index][Thread]
non-commut !-free LL is PSPACE-complete
It is known that (commutative) Multiplicative-Additive fragment of
Linear Logic is PSPACE-complete
(Lincoln, Mitchell, Scedrov, and Shankar).
We prove that non-commutative Multiplicative-Additive fragment
of Linear Logic is PSPACE-complete, as well.
Moreover, intuitionistic version of this fragment, or
Lambek Calculus enriched by additives: {+,&},
is PSPACE-complete.
In addition, PSPACE-completeness can be obtained even
for one-literal sequents (containing only ONE atomic literal)
that use only one version of implication (either right or left),
product, +, and &.
PSPACE-completeness can be obtained also for 1-only
non-commutative Multiplicative-Additive sequents
(containing no literals at all).
For modalized case, we can improve Kanovich's result on
undecidability of the modalized purely
implicational Lambek Calculus as follows:
Even one-literal modalized purely implicational Lambek Calculus
(with \, /, and outside !) is undecidable.
Moreover, ALL partial recursive relations are strongly definable
in this one-literal fragment of the modalized Lambek Calculus.
As a corollary, we get the undecidability of
non-commutative Multiplicative-Exponential fragment of Linear
logic (without additives!) even for 1-only sequents
(built up of the single constant 1 by |x|, \Par, -o, and
outside !) that contain neither \bot nor literals at all.
My best regards,
Max Kanovich.