Propositional modal logic with implicit modal quantification
Propositional modal logic with implicit modal quantification
复制标题
具有隐式模态量化的命题模态逻辑
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
R. Ramanujam
中科院分区：
文献类型：
--
作者：
A. Padmanabha;R. Ramanujam
命题术语模态逻辑是在具有无限多个可访问性关系的克里普克结构上解释的，因此语法允许对模态进行索引和量化的变量。这种逻辑是不可判定的，我们考虑具有隐式量化的无变量命题双模态逻辑。因此 ([forall ]alpha ) 断言所有可访问性关系上的必然性，而 ([exists ]alpha ) 是某些可访问性关系上的经典必然性。该逻辑与模型上的自然互模拟关系相关联，并且我们证明该逻辑正是二排序一阶逻辑的互模拟不变片段。该逻辑很容易被视为可判定的，并且允许有效公式的完全公理化。此外，决策过程自然延伸到全项模态逻辑的“捆绑片段”。
Propositional term modal logic is interpreted over Kripke structures with unboundedly many accessibility relations and hence the syntax admits variables indexing modalities and quantification over them. This logic is undecidable, and we consider a variable-free propositional bi-modal logic with implicit quantification. Thus ([forall ]alpha ) asserts necessity over all accessibility relations and ([exists ]alpha ) is classical necessity over some accessibility relation. The logic is associated with a natural bisimulation relation over models and we show that the logic is exactly the bisimulation invariant fragment of a two sorted first order logic. The logic is easily seen to be decidable and admits a complete axiomatization of valid formulas. Moreover the decision procedure extends naturally to the ‘bundled fragment’ of full term modal logic.