SEMANTICS OF WEAKENING AND CONTRACTION

The shriek modality ! of linear logic performs two tasks: it restores in annotated from both weakening and contraction. We separate these tasks by introducing two modalities: !w for weakening and !c for contraction. These give rise to two logics which are ''inbetween'' linear and intuitionistic logic in affine (or weakening) logic one always has weakening and a !c for contraction and in relevant (or contraction) logic one always has contraction and a !w for weakening. The semantics of these logics is obtained from special kinds of monads, introduced by Anders Kock in the early seventies. As subtle point is how to retrieve the ! of linear logic from !w and !c. Technically this will be achieved in terms of distributive laws-introduced by Jon Beck. We find models where one has ! = !!wc and also models with ! = !!cw. It will be shown that on the category of complete lattices one has comonads !w and !c with !!wc = ! = !!wc.