STIT逻辑的能力片段初探

A Simple Analysis of The Ability Fragment of STIT Formalisms

STIT理论作为刻画主体能动性的一类哲学逻辑,近来受到了多主体系统研究者们的关注。由于群体STIT逻辑被证明不可判定且无法有穷公理化,相关研究者们转而寻找其中可判定且可有穷公理化的片段。本文限制公式的定义,将目标限定在形如◇[a:cstit]φ及◇[G:cstit]φ的能力公式上,分别称之为个体STIT逻辑与群体STIT逻辑的能力片段。可以证明,如果只考虑STIT逻辑的能力片段,每个STIT模型都存在一个等价的邻域模型。此外,个体STIT逻辑与群体STIT逻辑的能力片段都是可有穷公理化的。

As a class of philosophical logics of agency,STIT formalisms have recently attracted the attention of researchers who aim at using this machineries to model and reason about multi-agent systems.Since the STIT logic for groups proved to be undecidable and not finitely axiomatizable,researchers turned to look for fragments in which decidability and finite axiomatics remain.By means of restricting the construction of formulas,this article highlights the so-called can-formulas which are of the form ◇[a:cstit]φand ◇[G:cstit]φin STIT formalisms.These formulas are therefore refered as the ability fragment of individual STIT and group STIT respectively.If only the ability fragments of STIT formalisms are considered,there exists an equivalent neighborhood model for each STIT model in the sense that they satisfy the same formulas.In addition,the ability fragments of both individual and group STIT are finitely axiomatizable.