@inproceedings{discovery10198560, editor = {Rastislav Kr{\'a}lovi{\vc} and Anton{\'i}n Ku{\vc}era}, year = {2024}, booktitle = {49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)}, title = {When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines}, journal = {Leibniz International Proceedings in Informatics, LIPIcs}, note = {Copyright {\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.}, pages = {30:1--30:19}, publisher = {Dagstuhl Publishing}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = {306}, month = {August}, address = {Wadern, Germany}, issn = {1868-8969}, url = {https://doi.org/10.4230/LIPIcs.MFCS.2024.30}, author = {Bonchi, Filippo and Di Giorgio, Alessandro and Trotta, Davide}, 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.}, keywords = {Relational algebra; hyperdoctrines; cartesian bicategories; string diagrams} }