wjl and I had an edifying conversation about linear logic.So, like, I took for granted that classical linear logic is not conservative over intuitionistic linear logic, but unlike the classical logic vs. intuitionistic logic case, where there are some standard shibboleth propositions that distinguish them (double negation elimination, excluded middle, peirce's formula) I couldn't think of any off the top of my head.
If your notion of "intuitionistic linear logic" is the one from Frank/Kaustuv/Evan's JILL paper, then you at least get ⊥, and you can take the linear double negation elimination formula ((A -o ⊥) -o ⊥) -o A, which is not provable in JILL, but provable in CLL.
But suppose you disallow mentioning bottom: then what's a simple nice formula that's provable in CLL but not ILL? We puzzled over it for a bit, and only came up with the somewhat clunky formula
(A0 & B0)0 -o (A00 ⊕ B00)
(where A0 is an abbreviation for A -o 0, and A00 associates like (A -o 0) -o 0)
Can one do any better?