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