Hi, Paul,
This view of intuitionistic logic as a fragment of the bigger linear logic, is widely held but I don't agree with it.
What's to disagree with? Girard's ! admits bicartesian models.
But a model of linear logic doesn't, as far as I'm aware, give rise to a bicartesian closed category.
"Give rise to"? Granted the LL axioms don't stipulate that the image of bang be bicartesian (have sum in addition to product), but neither do they disallow it. The interpretations of ! encountered in LL applications tend to be bicartesian closed, in particular the one that my message was all about, namely Set.
So there's no translation (at the level of proofs, rather than provability) from intuitionistic logic to linear logic.
Perhaps so, but then that's your problem, you're the one who's insisting on a different definition of "intuitionistic" from the one Girard had in mind when he axiomatized !. If he'd wanted bicartesian closed, the axioms for ! would have said so. Since you're the one who wants it, the responsibility for axiomatizing ! accordingly is yours, not Girard's. Vaughan Pratt