论模态逻辑的集合论语义，本文主要内容关键词为：集合论论文,语义论文,逻辑论文,模态论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
中图分类号：B81 文献标识码：A 文章编号：1674-3202(2009)-04-0082-15
修订日期：2009-11-17
集合论与逻辑的联系十分密切，集合论的语言是带二元属于关系符号的一阶语言。一方面公理集合论可以看作一阶理论，它是在一阶逻辑公理的基础上增加关于集合的公理得到的。因此它以一阶逻辑为基础。另一方面，集合论有足够强的表达能力，它几乎能定义所有一般的数学概念。从语义方面看，集合也可以作为解释逻辑语言的语义结构。这一点在构造集合论模型的过程中已经体现出来了。不仅如此，作为语义结构的集合还有更广泛的应用。
本文探讨在集合上对模态逻辑的解释，在这种语义下研究模态逻辑的一些语义问题。首先介绍基本模态逻辑的句法和语义，说明关系结构与集合之间的联系，由此引入非良基集合。第二部分讨论集合论语义，定义集合与公式之间的满足关系，并分析这种语义与克里普克关系语义之间的联系。第三部分讨论模态语言与集合论语言的联系。第四部分研究集合论语义下集合构造的问题，定义一些非标准的集合运算，并且证明模态公式在这些运算下的保持结果。
一、模态逻辑的句法和语义
在命题逻辑语言的基础上增加模态算子就得到模态语言。基本模态语言ML(Φ，◇)是由(可数)命题变号集Φ和一元模态词◇组成的。基本模态公式由如下规则给出：
模态语言是谈论关系结构的语言。基本模态语言只含一个一元模态词，它所处理的关系结构只含一个二元关系。对于基本模态语言来说，一个框架F=(W,R)是关系结构，其中W是非空集，R是W上的二元关系。W中的元素称为可能世界、结点、状态等等，R称为状态之间的可及关系。一个模型M=(F，V)由框架F和赋值V组成，V是从命题变号集Ф到W的幂集的函数，对每个命题变号p指派W的子集V(p)。一个模态公式ф在模型M=(W，R，V)的状态w上真(记号：M，w
ф)递归定义如下：
以上给出了模态逻辑的句法和关系语义，下面进一步探讨模态逻辑的语义与集合论之间的联系。首先，在模态逻辑的关系语义中，框架可被看作数学的图论中的有向图，而模型可以看作加标图。一个图(G，R)是由一些结点的集合G和结点之间的边关系R组成的，而一个加标图则是在图的基础上为每个结点增加标签得到的。集合与图的联系在于，集合中元素之间的属于关系构成一个图。反过来，给定一个图也可以通过下面定义的装饰函数来给出相应的集合。
给定一个加标图(G，R，l)，它的装饰函数f定义如下：对每个结点w指派一个集合f(w)=d(w)∪l(w)，其中d是图(G，R)的装饰函数，l是加标函数。在加标图中，每个结点w的标签l(w)是一个命题变号集合。因此，f(w)这个集合中不仅有集合作为元素，还有命题变号这样的不是集合的元素。这里对集合的概念做一点说明。在公理集合论ZF中，集合论的论域中每个对象都是集合，每个非空集合中的元素都是集合，因此不存在不是集合的元素。但这里规定一个类U，它由不是集合也不是类的元素组成，这些元素称为本元。在本文中我们只使用命题变号作为本元。
二、模态逻辑的集合论语义
其次，讨论模态逻辑系统K的几个推理规则。注意Sub规则和Gen规则在框架(类)上保持有效性，并且Gen在模型上也保持有效性，即对任意模型M，如果Mф，那么M□ф。但是，一个集合类不能确定一个正规模态逻辑，因为Sub规则和Gen规则在集合类上不保持有效：
1.Sub在集合上不保持有效性。例如，任给集合a使得命题变号p∈a但q
a，q可以看作p的代入结果。
2.在一个集合a上Gen规则也不保持有效。令集合a=｛p，｛q｝｝。由于p∈a，因此p在a上是真的，但□p在a上是假的。在集合论语义下，关于Gen规则可得下面命题2。
3.二元关系符号：R
4.逻辑符号：
、
(量词)，
、∧、∨、→(命题联结词)。
定义了集合论标准翻译，一个问题就是证明van Benthem类型的刻画定理，即找出一个集合论表达式是一个模态公式的翻译的充分必要条件。④但证明这样一条复杂定理需要考虑模态公式在一些模型论构造下保持或不变的性质。第四部分我们将给出一些初步的结果。
四、集合运算与模态可定义性
在经典模型论中，使用映射对公式分类是一个重要问题。在集合论语义下，可以使用集合之间的映射对模态公式进行分类。通过定义集合上的一些运算，考虑所有模态公式在这些集合运算下的保持结果。有一些标准的集合运算，比如并、交、补等等。但借助集合与加标图之间的关系，可以定义如下非标准的集合运算：不交并、生成子集合、p-态射、树展开等等。所证明的主要结果是所有模态公式在这些运算下具有不变性。
4.3 p-态射
从K.Segerberg的著作《论经典模态逻辑》([8])开始，模态逻辑的研究开始大量使用p-态射。在集合传递闭包上，我们也可以定义一种p-态射，使得所有模态公式在这样的运算下具有不变性。
定义13 给定集合a和b，从集合传递闭包STC(｛a｝)到STC(｛b｝)的一个p-态射是一个函数f：STC(｛a｝)→STC(｛b｝)使得：
1.f是满射；
2.如果f(x)=y，则对所有命题变号p，p∈x当且仅当p∈y；
3.如果u∈x∈STC(｛a｝)，则f(u)∈f(x)∈STC(｛b｝)；
4.如果v∈f(x)∈STC(｛b｝)，则存在u∈STC(｛a｝)使f(u)=v且u∈x。
一般地，给定一个集合类S，如果S是模态可定义的，那么S应该在上面给出的几种运算下封闭，即给定一种运算f，它作用于S中的元素产生的结果仍然在S中。如果S不在某种运算下封闭，那么S就不是模态可定义的。下面的命题给出两个并非模态可定义的集合类。
树展开的例子有许多，比如集合Ω的树展开就是一个无穷长的链。把自返、对称的点都展开，由此得到禁自返、禁对称的集合。因此，这样的集合类在模态语言中也是不可定义的。
五、结论
本文所探讨的语义是在集合上解释模态公式，主要工作如下：1)探讨了关系语义学下模型和框架与集合之间的联系；2)在集合论语义下探讨了模态语言与一阶集合论语言之间的联系；3)定义了集合传递闭包的概念，进一步定义了四种非标准的集合运算：集合传递闭包的不交并、生成子集合、p-态射和树展开，并且证明了所有模态公式在这些集合运算下的不变性结果。这奠定了在集合论语义下研究模态逻辑的基础。尚有许多问题值得进一步探究，比如模型和框架的区别如何在集合论语义下表示出来；如何利用集合上的互模拟概念，在一阶集合论语言中刻画模态语言，也就是证明van Benthem类型的刻画定理；如何在集合论语义下研究模态逻辑系统的一些逻辑性质等等。
注释：
①一个代入是从命题变号集到公式集的函数。对一个公式代入的结果是对该公式中命题变号代入的结果。
②这些基本概念的定义参见[3]第十一章。后面的命题2、3和定理1、2都取自该章节，这些命题和定理的意义在于，它们表明集合论语义与关系语义学一样具有重要意义，在集合论语义下，模态逻辑得到了新的解释。
③参见[7]麦金森在这篇文章中使用代数方法证明的结果如下：任给一致的正规模态逻辑L，如果◇
∈L，那么L
Triv；如果◇L，那么LVerum。
④参见[5]第二章。对于模态逻辑的一阶翻译来说，van Benthem定理说明，一个一阶公式α(x)等价于某个模态公式的标准翻译当且仅当它在互模拟下保持不变。
⑤关于单个集合的可定义性问题，参见[2]给出的定理，他证明了每个集合都可以使用无穷模态语言的某个公式来刻画，即对任何集合a，存在无穷模态语言的公式ф使得对任何集合b都有bф当且仅当a=b。
标签：集合论论文; 集合运算论文; 语义分析论文; 命题逻辑论文; 关系模型论文; 集合符号论文; 模态分析论文; 逻辑模型论文; 数学集合论文; 关系逻辑论文;