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, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Liste complète des métadonnées

Littérature citée [45 références]  Voir  Masquer  Télécharger

Contributeur : Lutz Straßburger <>
Soumis le : lundi 12 février 2007 - 15:44:51
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : mardi 6 avril 2010 - 21:42:28


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00130508, version 1



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



Consultations de la notice


Téléchargements de fichiers