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.
Type
Publication
In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)
Davide Trotta
Assistant professor (RTDA)
I am a mathematician, and my research is mainly focused on categorical logic and its applications in theoretical computer science.