协代数逻辑的正向化

我们全面地给出正向协代数逻辑，并展示如何由布尔协代数逻辑获得正向协代数逻辑。在模型侧，这涉及由第二作者等人先前定义的称为 posetification 的程序，从内函子 $T: Set\to Set$ 规范地计算内函子 $T': Pos\to Pos$。在语法侧，这涉及由语法构造函子 $L: BA\to BA$ 规范地计算语法构造函子 $L': DL\to DL$，我们称此对偶程序为 positivication（正向化）。这些运算本身即具趣味，我们显式计算了若干模态逻辑情形下的 posetification 与 positivication。我们展示布尔协代数逻辑的语义如何被规范地提升以定义其正向片段的语义，并且弱完备性从布尔情形转移到正向情形。