条件/判定对偶性与广延限制范畴的内逻辑

在流程图语言中，谓词扮演一种有趣的双面角色。在文本表示中，它们常作为条件出现，即易于与其他条件（常通过布尔组合子）结合形成新条件的表达式，尽管它们仅在辅助分支语句选择执行分支时起支持作用。另一方面，在图形表示中它们通常作为判定出现，本质上能引导控制流却大多对布尔组合不敏感。尽管对流程图语言的范畴化处理屡见不鲜，但无一处理谓词这种双重性质。本文主张，广延限制范畴恰是捕捉此种条件/判定对偶性的范畴，借助的态射巧合地也称为判定。进一步，我们表明拥有这些范畴判定等价于拥有一种内逻辑：类比于拓扑斯中对象的子对象形成 Heyting 代数，我们证明广延限制范畴中对象的判定形成 De Morgan 拟格——与（三值）弱 Kleene 逻辑 $\mathbf{K}^w_3$ 相关的代数结构。通过限制到全判定可恢复完整经典命题逻辑，从而得到通常意义上的广延范畴，并从另一方向确认了效应论（effectus theory）的一个结果：广延范畴中对象的谓词形成布尔代数。作为一个应用，由于（范畴）判定是部分同构，该方法为经典命题逻辑与弱 Kleene 逻辑提供了天然可逆的模型。