9 Apr
2004
9 Apr
'04
10:56 a.m.
Hi Vaughan,
This view of intuitionistic logic as a fragment of the bigger linear logic,
is widely held but I don't agree with it. A model of (propositional) intuitionistic logic is a bicartesian closed category. (I'm assuming we want to model proofs, not just provability.) But a model of linear logic doesn't, as far as I'm aware, give rise to a bicartesian closed category. So there's no translation (at the level of proofs, rather than provability) from intuitionistic logic to linear logic. Paul