## Paper: Constructing Free Boolean Categories (at LICS 2005)

**François Lamarche Lutz Straßburger**

### Abstract

By Boolean category we mean something which is to a Boolean algebra what a category is to a poset. We propose an axiomatic system for Boolean categories, which is different in several respects from the ones proposed recently. In particular everything is done from the start in a *-autonomous category and not in a weakly distributive one, which simplifies issues like the Mix rule. An important axiom, which is introduced later, is a "graphical" condition, which is closely related to denotational semantics and the Geometry of Interaction. Then we show that a previously constructed category of proof nets is the free "graphical" Boolean category in our sense. This validates our categorical axiomatization with respect to a real-life example. Another important aspect of this work is that we do not assume a-priori the existence of units in the *-autonomous categories we use. This has some retroactive interest for the semantics of linear logic, and is motivated by the properties of our example with respect to units.

### BibTeX

@InProceedings{Straburger-ConstructingFreeBoo, author = {François Lamarche and Lutz Straßburger}, title = {Constructing Free Boolean Categories}, booktitle = {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)}, year = {2005}, month = {June}, pages = {209--218}, location = {Chicago, USA}, publisher = {IEEE Computer Society Press} }