余代数动态逻辑的弱完全性

我们给出了 Fischer 和 Ladner 命题动态逻辑（PDL）以及 Parikh 博弈逻辑（GL）的余代数推广。在前期工作中，我们证明了无迭代的余代数动态逻辑的一个通用强完全性结果。此类程序的余代数语义由一个单子 T 给出，模态通过谓词提升 \^I 解释，其转置是从 T 到邻域单子的一个单子态射。本文中，我们展示如果单子 T 携带一个完备半格结构，那么我们可以定义一个迭代构造，以及谓词提升的菱形相似性和框相似性的合适概念，从而允许定义关于 T、\^I 和一组选定的点态程序运算参数化的公理化。作为主要结果，我们表明如果点态运算是“无否定的”且 Kleisli 复合在 Kleisli 箭头上的诱导 join 上左分配，则该公理化相对于标准模型类是弱完全的。作为特例，我们恢复了 PDL 和无对偶博弈逻辑的弱完全性。作为一个不大的新结果，我们得到了无对偶 GL 扩展以博弈的交（恶魔选择）的完全性。