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.
@InProceedings{bonchi_et_al:LIPIcs.MFCS.2024.30, author = {Bonchi, Filippo and Di Giorgio, Alessandro and Trotta, Davide}, title = {{When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines}}, booktitle = {49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)}, pages = {30:1--30:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-335-5}, ISSN = {1868-8969}, year = {2024}, volume = {306}, editor = {Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.30}, URN = {urn:nbn:de:0030-drops-205867}, doi = {10.4230/LIPIcs.MFCS.2024.30}, annote = {Keywords: relational algebra, hyperdoctrines, cartesian bicategories, string diagrams} }
Feedback for Dagstuhl Publishing