Skip to Main content Skip to Navigation
Conference papers

Constructing Free Boolean Categories

François Lamarche 1 Lutz Strassburger
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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, similar to but differing in several respects from the one given very recently by Führmann and Pym. In particular everything is done from the start in a *-autonomous category and not a linear 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.
Complete list of metadatas
Contributor : Francois Lamarche <>
Submitted on : Wednesday, October 19, 2005 - 1:41:17 PM
Last modification on : Thursday, January 11, 2018 - 6:19:48 AM


  • HAL Id : hal-00012296, version 1



François Lamarche, Lutz Strassburger. Constructing Free Boolean Categories. 2005, pp.478. ⟨hal-00012296v1⟩