Abstract
The term "Boolean category" should be used for describing an object that is to categories what a Boolean algebra is to posets. More specifically, a Boolean category should provide the abstract algebraic structure underlying the proofs in Boolean Logic, in the same sense as a Cartesian closed category captures the proofs in intuitionistic logic and a *-autonomous category captures the proofs in linear logic. However, recent work has shown that there is no canonical axiomatisation of a Boolean category. In this work, we will see a series (with increasing strength) of possible such axiomatisations, all based on the notion of *-autonomous category. We will particularly focus on the medial map, which has its origin in an inference rule in KS, a cut-free deductive system for Boolean logic in the calculus of structures. Finally, we will present a category of proof nets as a particularly well-behaved example of a Boolean category.
| Original language | English |
|---|---|
| Pages (from-to) | 536-601 |
| Number of pages | 66 |
| Journal | Theory and Applications of Categories |
| Volume | 18 |
| Publication status | Published - 18 Oct 2007 |
| Externally published | Yes |
Keywords
- *-autonomous category
- Boolean category
- Classical logic
- Proof nets
- Proof theory