Models of linear logic

Marc Bergeron ; William Hatcher

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part IX, Tome 220 (1995), pp. 23-35

Résumé

We engage a study of non-modal linear logic which takes times $\otimes$ and the linear conditional $\multimap$ to be the basic connectives instead of times and linear negation $()^\bot$ as in Girard's approach. This difference enables us to obtain a very large subsystem of linear logic (called positive linear logic) without an involutionary negation (if the law of double negation is removed from linear logic in Girard's formulation, the resulting subsystem is extremely limited). Our approach enables us to obtain several natural models for various subsystems of linear logic, including a generic model for so-called minimal linear logic. In particular, it is seen that these models arise spontaneously in the transition from set theory to multiset theory. We also construct a model of full (nonmodal) linear logic that is generic relative to any model of positive linear logic. However, the problem of constructing a generic model for positive linear logic remains open. Bibliography: 2 titles.