re: Complexity questions on linear logic
To: email@example.com, firstname.lastname@example.org
[In reply to message from email@example.com 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).