A dialectica-like model of linear logic

The aim of this work is to define the categories GC, describe their categorical structure and show they are a model of Linear Logic. The second goal is to relate those categories to the Dialectica categories DC, cf.[DC], using different functors for the exponential "of course". It is hoped that this categorical model of Linear Logic should help us to get a better understanding of the logic, which is, perhaps, the first non-intuitionistic constructive logic. This work is divided in two parts, each one with 3 sections. The first section shows that G C is a monoidal closed category and describes bifunctors for tensor "®', internal horn "[-, ] " , par "~", cartesian products "&" and coproducts "q~". The second section defines linear negation as a contravariant functor obtained evaluating the internal hom bifunctor at a "dualising object". The third section makes explicit the connections with Linear Logic, while the fourth introduces the comonads used to model the connective "of course". Section 5 discusses some properties of these comonads and finally section 6 makes the logical connections once more. This work grew out of suggestions of J.Y. Girard at the AMS-Conference on Categories, Logic and Computer Science in Boulder 1987, where I presented my earlier work on the Dialectica categories, hence the title. Still on the lines of given credit where it is due, I would like to say that Martin Hyland, under whose supervision this work was written, has been a continuous source of ideas and inspiration. Many heartfelt thanks to him. 1. The main definitions