The complexity of neutrals in linear logic
Max Kanovich · 2002
The main result announced in the paper is the proof of the existence of strongly independent (free) sets of linear logic formulas that are built up of only neutrals. The motivating application is a uniform and transparent technique for obtaining the exact computational characterization of constant only fragments of commutative and noncommutative linear logic. In particular, we prove the surprising results that: multiplicative additive fragments of constant only linear logic are PSPACE complete; all partial recursive predicates are directly definable in the full constant only linear logic.