带及不含 Medial 的布尔范畴的公理化

术语 "布尔范畴" 用于描述一个对象就其范畴而言，类似于布尔代数相对于偏序集。更具体地说，布尔范畴应提供底层抽象代数结构，以捕获布尔逻辑证明的结构，方式类似于笛卡尔闭合范畴捕获直觉主义逻辑证明，以及 *-autonomous 范畴捕获线性逻辑证明。然而，最近的工作表明，布尔范畴不存在标准的公理化。在本工作中，我们将看到一系列（具有递增强度）的可能公理化，全部基于 *-autonomous 范畴的概念。我们将特别关注 medial map，这一概念源自 KS 中的一个推理规则，KS 是一种无切分的布尔逻辑演绎系统，用于结构计算。最后，我们将呈现 proof nets 的范畴作为布尔范畴的一个特别 well-behaved 的例子。