Weak Completeness of Coalgebraic Dynamic Logics
Weak Completeness of Coalgebraic Dynamic Logics
复制标题
代数动态逻辑的弱完备性
DOI：
10.4204/eptcs.191.9
复制
发表时间：
2015
影响因子：
2
通讯作者：
C. Kupke
中科院分区：
文献类型：
--
作者：
H. Hansen;C. Kupke
本文给出了Fischer和拉德纳的命题动态逻辑（PDL）和Parikh的博弈逻辑（GL）的一个共代数推广。在早期的工作中，我们证明了一个通用的强完备性结果的余代数动态逻辑没有迭代。这些程序的共代数语义由单子T给出，模态通过谓词提升l来解释，其转置是从T到邻域单子的单子态射。在本文中，我们表明，如果单子T进行一个完整的半格结构，那么我们可以定义一个迭代构造，和适当的概念的菱形和框状的谓词提升允许定义的axiomatisation参数在T，l和一组选定的逐点程序操作。作为我们的主要结果，我们表明，如果逐点操作是“负自由”和Kleisli组合左分布在诱导加入Kleisli箭头，那么这个公理化是弱完全的标准模型类。作为特例，我们恢复了PDL和双自由博弈逻辑的弱完备性。作为一个适度的新的结果，我们获得了完整的双自由GL扩展与交叉（恶魔的选择）的游戏。
We present a coalgebraic generalisation of Fischer and Ladner’s Propositional Dynamic Logic (PDL) and Parikh’s Game Logic (GL). In earlier work, we proved a generic strong completeness result for coalgebraic dynamic logics without iteration. The coalgebraic semantics of such programs is given by a monad T, and modalities are interpreted via a predicate lifting l whose transpose is a monad morphism from T to the neighbourhood monad. In this paper, we show that if the monad T carries a complete semilattice structure, then we can define an iteration construct, and suitable notions of diamond-likeness and box-likeness of predicate-liftings which allows for the definition of an axiomatisation parametric in T, l and a chosen set of pointwise program operations. As our main result, we show that if the pointwise operations are “negation-free” and Kleisli composition left-distributes over the induced join on Kleisli arrows, then this axiomatisation is weakly complete with respect to the class of standard models. As special instances, we recover the weak completeness of PDL and of dual-free Game Logic. As a modest new result we obtain completeness for dual-free GL extended with intersection (demonic choice) of games.