%0 Generic %A Bonchi, Filippo %A Di Giorgio, Alessandro %A Trotta, Davide %C Wadern, Germany %D 2024 %E Královič, Rastislav %E Kučera, Antonín %F discovery:10198560 %I Dagstuhl Publishing %K Relational algebra; hyperdoctrines; cartesian bicategories; string diagrams %P 30:1-30:19 %T When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines %U https://discovery.ucl.ac.uk/id/eprint/10198560/ %V 306 %X 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. %Z 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.