A new algebraic axiomatization of linear logic models is presented. The axiomsdirectly reflect at the model-theoretic level the de Morgan duality exhibited by linear logic, and are considerably simpler than previous axioms. Several equationally defined classes of models are studied. One such class suggests a new variant of linear logic, called cancellative linear logic, in which it is always possible to cancel a proposition p (viewed as a resource) and its negation p1 (viewed as a debt). This provides a semantics for a generalization of the usual token game on Petri nets, called the financial game. Poset models, called Girard algebras, are also defined equationally; they generalize for linear logic the Boolean algebras of classical logic, and contain the quantale models as a special case. The proposed axiomatization also provides a simple set of categorical combinators for linear logic, extending those previously proposed by Lafont.
展开▼
