Consider the sequent calculus presentations of propositional linear logic (LL) and propositional intuitionistic linear logic (ILL). Clearly, there are formulas in LL that are not in ILL, such as $\bot$ or $?X$ or $X \,⅋\, X^\perp$. So, a natural question arises:
For every formula $F$ of LL, is there a formula $G$ in ILL that is provably equivalent in LL to $F$?
I say that $F$ is provably equivalent to $G$ in LL if the formulas $F^\perp \,⅋\, G$ and $G^\perp \,⅋\, F$ (i.e. $F \multimap G$ and $G \multimap F$ in the two-sided sequent calculus) are provable in LL.
If the same question is about classical logic LK (instead of LL) and intuitionistic logic LJ (instead of ILL), the answer is positive thanks to double negation translations. But the same argument cannot be applied here, even because it is not clear to me what a negation is in ILL.