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.

翻译：Fo-双范畴是Peirce关系演算的一种范畴化推广。值得注意的是，其法则为纯等式且完备的一阶逻辑提供了证明系统。本文揭示了fo-双范畴与Lawvere超词项之间的对应关系。为简化证明，我们引入Peircean双范畴，它提供了对fo-双范畴更简洁的特征刻画。