Decision problems for propositional linear logic (Q1192352)

The main results are: full propositional linear logic LL is undecidable (a) and its exponential-free fragment MALL is PSPACE-complete (b). The proof of (a) has three steps: 1. Consider a variant of two-counter machines called ACM: essentially, there is no ZERO-test instruction and there is a FORK instruction instead. ACMs have an undecidable halting problem, because they can simulate usual two-counter machines. 2. Any ACM instruction translates into a sequent of LL of a special form; to any ACM \(M\) there corresponds a finite set of sequents \(\overline M\), called a ``theory'' in LL. Moreover, to an instantaneous description \(s\) of \(M\) one associates a set \(\theta(s)\) of sequents so that \(M\) accepts \(s\) iff every sequent of \(\theta(s)\) is provable in \(\text{LL}+\overline M\). 3. To conclude, one needs a kind of Deduction Theorem for the ``theories'' introduced in 2. Axioms are of the special form \(t= \lvdash C\), \(p^ \perp_ 1,\dots,p^ \perp_ n\), where \(C\) is exponential-free and \(p_ i\) is a propositional variable. Such a sequent translates into the LL-formula \([t]=C^ \perp\otimes p_ 1\otimes\cdots\otimes p_ n\). If \(T=\{t_ 1,\dots,t_ n\}\) is a (finite) ``theory'', let \(T\) be the multiset of formulas \(?[t_ 1],\dots,?[t_ n]\). Then a sequent \(\lvdash\Gamma\) is provable in \(\text{LL}+T\) iff the sequent \(\lvdash[T],\Gamma\) is provable in LL. The proof of (b): provability in MALL is PSPACE because of cut- elimination (there is a detailed proof of cut-elimination for LL in an Appendix). To prove that the problem is PSPACE-hard, it is shown how to reduce to it the problem of the validity of quantified Boolean formulas (QBF). This is achieved by a careful encoding of any QBF as a sequent in MALL which is provable iff the QBF is valid. There are also other results on the complexity of other fragments of (even non-commutative) linear logic.