HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Other publications

On the Axiomatisation of Boolean Categories with and without Medial

Lutz Straßburger 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : In its most general meaning, a Boolean category is to categories what a Boolean algebra is to posets. In a more specific meaning 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 proof nets as a particularly well-behaved example of a Boolean category.
Complete list of metadata

Cited literature [45 references]  Display  Hide  Download

https://hal.inria.fr/inria-00130508
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Monday, February 12, 2007 - 3:44:51 PM
Last modification on : Thursday, January 20, 2022 - 5:30:48 PM
Long-term archiving on: : Tuesday, April 6, 2010 - 9:42:28 PM

File

medial.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00130508, version 1

Collections

Citation

Lutz Straßburger. On the Axiomatisation of Boolean Categories with and without Medial. 2006. ⟨inria-00130508⟩

Share

Metrics

Record views

227

Files downloads

128