We describe a family of decidable propositional dynamic logics, where atomic modalities satisfy some extra conditions (for example, given by axioms of the logics K5, S5, or K45 for different atomic modalities). It follows from recent results (Kikot, Shapirovsky, Zolin, 2014; 2020) that if a modal logic $L$ admits a special type of filtration (so-called definable filtration), then its enrichments with modalities for the transitive closure and converse relations also admit definable filtration. We use these results to show that if logics $L_1, \ldots , L_n$ admit definable filtration, then the propositional dynamic logic with converse extended by the fusion $L_1*\ldots * L_n$ has the finite model property.
翻译:关于具有逆运算的命题动态逻辑的可判定扩展
摘要:
我们描述了一族可判定的命题动态逻辑,其中原子模态满足一些额外条件(例如,由不同原子模态的K5、S5或K45的公理给出)。由最近的研究结果(Kikot、Shapirovsky、Zolin,2014;2020)可知,如果一种模态逻辑L具有特殊类型的过滤(即可定义过滤),则其具有传递闭包和逆关系模态的丰富也具有可定义过滤。我们使用这些结果来展示,如果逻辑L1,……,Ln具有可定义过滤,则具有融合L1 *……* Ln的逆命题动态逻辑具有有限模型性质。