%O 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. %D 2024 %V 306 %A Filippo Bonchi %A Alessandro Di Giorgio %A Davide Trotta %J Leibniz International Proceedings in Informatics, LIPIcs %S Leibniz International Proceedings in Informatics (LIPIcs) %P 30:1-30:19 %L discovery10198560 %T When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines %I Dagstuhl Publishing %K Relational algebra; hyperdoctrines; cartesian bicategories; string diagrams %E Rastislav KráloviÄ %E AntonÃn KuÄera %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. %C Wadern, Germany %B 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)