re: Complexity questions on linear logic

To: types@theory.lcs.mit.edu, logic@theory.lcs.mit.edu

[In reply to message from gunter@central.cis.upenn.edu sent Sun, 4 Feb 90 17:08:16 EST.]

[Message from Grigori Mints, who is visiting Stanford and can be reached
through Vladimir Lifschitz (VAL@SAIL.STANFORD.EDU) until the end of March.]

Upper bound is probably P-space by Gentzen-type argument, probably taking
notice of Kripke trick for relevant implication, due to possible absence
of thinning rule. Lower bound is P-space via Girard translation of
intuitionistic implication in terms of linear implication and ! (of course).
Decidable fragments of relevance logic R  are in: G. Mints, A cut elimination
theorem for relevance logics, J. Soviet Math, V. 6 (1976), which is based on
the decidability of relevant implication (Kripke, abstract in JSL about
1965), and of relevant implication with negation (Belnap and Wallace, Z. fur
Math. Logik, after 1965).

--Grigori Mints