Bonchi, Filippo;
Di Giorgio, Alessandro;
Trotta, Davide;
(2024)
When Lawvere Meets Peirce: An Equational
Presentation of Boolean Hyperdoctrines.
In: Královič, Rastislav and Kučera, Antonín, (eds.)
49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024).
(pp. 30:1-30:19).
Dagstuhl Publishing: Wadern, Germany.
Preview |
Text
LIPIcs.MFCS.2024.30.pdf - Published Version Download (949kB) | Preview |
Abstract
Fo-bicategories are a categorification of Peirce’s calculus of relations. Notably, their laws provide a proof system for first-order logic that is both purely equational and complete. This paper illustrates a correspondence between fo-bicategories and Lawvere’s hyperdoctrines. To streamline our proof, we introduce peircean bicategories, which offer a more succinct characterization of fo-bicategories.
| Type: | Proceedings paper |
|---|---|
| Title: | When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines |
| Event: | Mathematical Foundations of Computer Science (MFCS) |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.4230/LIPIcs.MFCS.2024.30 |
| Publisher version: | https://doi.org/10.4230/LIPIcs.MFCS.2024.30 |
| Language: | English |
| Additional information: | Copyright © Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta; licensed under Creative Commons License CC-BY 4.0, https://creativecommons.org/licenses/by/4.0/legalcode. |
| Keywords: | Relational algebra; hyperdoctrines; cartesian bicategories; string diagrams |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10198560 |
Archive Staff Only
 |
View Item |
