模态逻辑的集合论语义与互模拟不变性

史璟

本文首先介绍模态逻辑的集合论语义，我们在集合传递闭包上解释模态语言。第二部分定义从模态语言到集合论语言的翻译，引入集合传递闭包之间的互模拟的概念。第三部分讨论集合论语言与一阶关系语言之间的一些联系，这是第四部分证明刻画定理的基础。第四部分，将证明集合论语义下的刻画定理，即一个一阶集合论公式等价于某个模态公式的集合论翻译当且仅当它在集合互模拟关系下不变。也就是，模态语言是一阶集合论语言的集合互模拟不变片段，它是对van Benthem 刻画定理的推广。

1 模态逻辑的集合论语义

巴威斯（J.Barwsie）和莫斯（L.Moss）在著作《恶性循环——非良基现象的数学》中引入了模态语言的集合论语义。（[2]）这种语义在集合上解释模态公式。令ML(◇,Φ)是基本模态语言，其中Φ 可数命题变元集合，◇是一个一元模态词。模态公式按照如下规则定义：

公式φ 在集合a 上是真的（记号：a|=φ）递归定义如下：

(1) a|=p ⇐⇒p ∈a；

(2) a|=¬φ ⇐⇒a/|=φ；

(3) a|=φ∧ψ ⇐⇒a|=φ 且a|=ψ；

(4) a|=◇φ ⇐⇒存在集合b ∈a 使得b|=φ。一个命题变元p 在a 上真定义为p 属于a。因此，集合a 中含有的命题变元不是集合也不是类，我们把这样的元素称为本元，本文使用的本元仅指命题变元；其次，公式◇φ 在集合a 上是真的，定义为存在a 中是集合的元素b 满足φ。我们仅仅在集合上计算公式的真值，而在本元或命题变元上不计算公式的真值。

另一个重要问题是，如上递归定义中使用的集合包括非良基集合。在经典集合论ZF 中有一条公理称为正则公理或良基公理，它是说每个非空集合都有属于关系的极小元。……