%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)