arXiv · 2404.18795
When Lawvere meets Peirce: an equational presentation of boolean hyperdoctrines
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.
Explore related subjects
Keep this discovery
Filippo Bonchi, Alessandro Di Giorgio, Davide Trotta. 2024-04-29. When Lawvere meets Peirce: an equational presentation of boolean hyperdoctrines. https://arxiv.org/abs/2404.18795
Cite the original work for its findings. Save a collection to share your selection of sources.