Recently, Lincoln, Scedrov, and Shankar proved that IMLL2 and MLL12 are undecidable by simulating the rules of contraction and weakening using second order propositional quantifiers and the multiplicatives (see the last message of the linear list).
Here is a new result:
Theorem: MALL2 is undecidable.
This is proved by a direct encoding of Minsky machines. We do not use the contraction axiom C = forall X. X -o X*X, but a `soft' version:
C' = forall X. X&1 -o X*X.
Our encoding is essentially Kanovich's one with A&1 in place of !A. Of course, the main difficulty is to show that C' does not produce fake computations. For this, we introduce a specific phase model.
Two remarks: