史璟

本文首先介紹模態(tài)邏輯的集合論語(yǔ)義，我們?cè)诩蟼鬟f閉包上解釋模態(tài)語(yǔ)言。第二部分定義從模態(tài)語(yǔ)言到集合論語(yǔ)言的翻譯，引入集合傳遞閉包之間的互模擬的概念。第三部分討論集合論語(yǔ)言與一階關(guān)系語(yǔ)言之間的一些聯(lián)系，這是第四部分證明刻畫定理的基礎(chǔ)。第四部分，將證明集合論語(yǔ)義下的刻畫定理，即一個(gè)一階集合論公式等價(jià)于某個(gè)模態(tài)公式的集合論翻譯當(dāng)且僅當(dāng)它在集合互模擬關(guān)系下不變。也就是，模態(tài)語(yǔ)言是一階集合論語(yǔ)言的集合互模擬不變片段，它是對(duì)van Benthem 刻畫定理的推廣。

1 模態(tài)邏輯的集合論語(yǔ)義

巴威斯（J.Barwsie）和莫斯（L.Moss）在著作《惡性循環(huán)——非良基現(xiàn)象的數(shù)學(xué)》中引入了模態(tài)語(yǔ)言的集合論語(yǔ)義。（[2]）這種語(yǔ)義在集合上解釋模態(tài)公式。令ML(◇,Φ)是基本模態(tài)語(yǔ)言，其中Φ 可數(shù)命題變?cè)?，◇是一個(gè)一元模態(tài)詞。模態(tài)公式按照如下規(guī)則定義：

公式φ 在集合a 上是真的（記號(hào)：a|=φ）遞歸定義如下：

(1) a|=p ??p ∈a；

(2) a|=?φ ??a/|=φ；

(3) a|=φ∧ψ ??a|=φ 且a|=ψ；

(4) a|=◇φ ??存在集合b ∈a 使得b|=φ。一個(gè)命題變?cè)猵 在a 上真定義為p 屬于a。因此，集合a 中含有的命題變?cè)皇羌弦膊皇穷?，我們把這樣的元素稱為本元，本文使用的本元僅指命題變?cè)?；其次，公式◇?在集合a 上是真的，定義為存在a 中是集合的元素b 滿足φ。我們僅僅在集合上計(jì)算公式的真值，而在本元或命題變?cè)喜挥?jì)算公式的真值。

另一個(gè)重要問題是，如上遞歸定義中使用的集合包括非良基集合。在經(jīng)典集合論ZF 中有一條公理稱為正則公理或良基公理，它是說每個(gè)非空集合都有屬于關(guān)系的極小元。因此不存在無窮下降的屬于關(guān)系鏈，不存在屬于自身的集合x ∈x，也不存在循環(huán)x ∈y1∈...∈yn∈x。非良基集合允許無窮下降的屬于關(guān)系鏈，因此允許屬于自身的集合，也允許循環(huán)。阿克采爾（P.Aczel）在《非良基集合》這部著作中研究了非良基集合，提出了反基礎(chǔ)公理AFA。（[1]）非良基集合論ZFA，是把ZF 中的基礎(chǔ)公理去掉后再加上反基礎(chǔ)公理AFA 得到的。（[6]）

阿克采爾的基本思想是利用集合與圖的關(guān)系，一個(gè)集合可以按照逆屬于關(guān)系展開為一個(gè)圖，而一個(gè)圖通過裝飾函數(shù)可以轉(zhuǎn)化為一個(gè)集合。一個(gè)圖(G,R)是由結(jié)點(diǎn)集G 和結(jié)點(diǎn)之間的二元邊關(guān)系R 組成的，如果Rwu，那么稱u 是w 的子結(jié)點(diǎn)。一個(gè)裝飾d 是一個(gè)函數(shù)，對(duì)每個(gè)結(jié)點(diǎn)w 指派集合d(w)使得：如果Rwu，那么d(u)∈d(w)。在經(jīng)典集合論ZF 中，Mostowski 坍塌定理說明，每個(gè)良基圖都有惟一的裝飾。每個(gè)良基圖都對(duì)應(yīng)于由它的所有結(jié)點(diǎn)的裝飾組成的集合。但是，如果考慮非良基圖，比如w 是自身的后繼結(jié)點(diǎn)，那么d(w) ∈d(w)，這樣就存在屬于自身的集合。因此，阿克采爾將Mostowski 坍塌定理推廣為：每個(gè)圖都有惟一裝飾。由此引入非良基集合。

在模態(tài)邏輯中，一個(gè)框架F=(W,R)就是一個(gè)圖。如果框架中有循環(huán)結(jié)點(diǎn)，比如自返點(diǎn)、對(duì)稱點(diǎn)等等，那么這個(gè)圖是非良基圖，所對(duì)應(yīng)的集合是非良基集。由于模態(tài)公式在框架基礎(chǔ)上進(jìn)行解釋，所以，在集合上解釋模態(tài)語(yǔ)言，就必須引入非良基集合，以便處理循環(huán)圖。比如模態(tài)公式p→◇p 在任何屬于自身的集合a上是真的。這樣，把集合之間的屬于關(guān)系看作可及關(guān)系，一個(gè)集合就可以看作模態(tài)語(yǔ)言所談?wù)摰年P(guān)系結(jié)構(gòu)。反之，給定一個(gè)關(guān)系結(jié)構(gòu)，也可以通過裝飾函數(shù)把它與一個(gè)集合聯(lián)系起來。

一般地，對(duì)任意非空集合a，它的傳遞閉包TC(a)定義為∩{b : a ?b 并且b 是傳遞的}，即包含集合a 的最小傳遞集合。TC(a)中可以含有本元。對(duì)每個(gè)集合a，令support(a)= TC(a) ∩Φ（Φ 是命題變?cè)＜蟬upport(a) 是與集合a 相關(guān)的本元的集合。如果support(a)= ?，那么稱集合a 為純集合。純集合是不含本元的集合。經(jīng)典集合論的論域中的集合都是純集合。一般地，定義論域Vafa[Φ]= {a : a 是集合并且support(a)?Φ}。Vafa[Φ]是集合類，它不含本元。此外，把Vafa[?]寫成Vafa，它是由所有純集合組成的類。

任給非空集合a，a |= ◇◇p 當(dāng)且僅當(dāng)存在集合b 和c 使得c ∈b ∈a 并且p ∈c。這里集合b 屬于a，但是c 不一定屬于a。為保證a 中所有集合中的集合都在a 中，我們遞歸定義{a}的集合傳遞閉包STC({a})如下：

? T0=a；

? Tn+1=Tn∪{b:b ∈c ∈Tn并且b 是集合}。

那么定義STC({a})=∪Tn:n ≥0。顯然a ∈STC({a})。下面我們?cè)诩蟼鬟f閉包上解釋模態(tài)公式。

定義1.任給非空集合a，如下遞歸定義模態(tài)公式φ 在集合傳遞閉包STC({a})中一個(gè)集合b 上真（記號(hào)：STC({a}),b|=φ）：

(1) STC({a}),b|=p ??p ∈b；

(2) STC({a}),b|=?φ ??STC({a}),b/|=φ；

(3) STC({a}),b|=φ∧ψ ??STC({a}),b|=φ 且STC({a}),b|=ψ；

(4) STC({a}),b|=◇φ ??存在c ∈STC({a})使c ∈b 且STC({a}),c|=φ。

顯然集合傳遞閉包的作用相當(dāng)于關(guān)系語(yǔ)義學(xué)下模型的作用。在集合傳遞閉包上解釋模態(tài)語(yǔ)言，不同于在集合上解釋模態(tài)語(yǔ)言，關(guān)鍵是每次我們從集合中取出的集合都屬于集合傳遞閉包。在后面我們以定義1 提供的模態(tài)邏輯語(yǔ)義為基礎(chǔ)。

2 集合翻譯與互模擬

在這一部分我們引入從模態(tài)語(yǔ)言到集合論語(yǔ)言的翻譯。在集合論語(yǔ)義下，集合上的逆屬于關(guān)系恰好可以看作可及關(guān)系，而集合本身可以看作狀態(tài)。因此，很自然也可以把所有模態(tài)公式翻譯為集合論公式。所使用的集合論語(yǔ)言含如下初始符號(hào)：

(1) 集合變?cè)簒0,x1,...（使用x、y、z 等表示）；

(2) 本元符號(hào)：p0,p1,...（使用p、q、r 等等表示本元）；

(3) 二元屬于關(guān)系符號(hào)：∈；

(4) 邏輯符號(hào)：?、?（量詞），?、∧、∨、→（命題聯(lián)結(jié)詞）。該集合論語(yǔ)言的公式是由如下規(guī)則形成的：

其中p 是本元，本元的集合就是基本模態(tài)語(yǔ)言ML(Φ,◇)的命題變?cè)夕?。其它?lián)結(jié)詞和量詞可以定義出來。

定義2.定義從基本模態(tài)語(yǔ)言到集合論語(yǔ)言的標(biāo)準(zhǔn)集合論翻譯π(φ,x)：

(1) 對(duì)每個(gè)p ∈Φ，π(p,x)=p ∈x

(2) π(?φ,x)=?π(φ,x)

(3) π(φ∧ψ,x)=π(φ,x)∧π(ψ,x)(4) π(◇φ,x)=?y(y ∈x∧π(φ,y))

這里的變?cè)獂 和y 都是集合變?cè)话衙}變?cè)苯臃g為集合的本元。同樣，對(duì)于公式□φ，有如下翻譯：π(□φ,x)=?y(y ∈x→π(φ,y))。在翻譯過程中，如果遇到重疊的模態(tài)詞，由于不同的量詞約束不同的變?cè)?，可以交替使用變?cè)獂 和y。因此，可以把所有模態(tài)公式翻譯到所定義的集合論語(yǔ)言的兩變?cè)瑪?，即只使用兩個(gè)變?cè)募险撜Z(yǔ)言片段。

例3.模態(tài)公式◇◇◇p 的集合論翻譯如下：

定理4.對(duì)任意集合a ∈Vafa[Φ]和模態(tài)公式φ，對(duì)每個(gè)b ∈STC({a})，如下成立：

證明.對(duì)φ 的構(gòu)造歸納證明。只證明φ:=◇ψ 的情況。顯然：

根據(jù)上面定義的標(biāo)準(zhǔn)翻譯，一個(gè)很自然的問題是：是否所有集合論公式都是某個(gè)模態(tài)公式的集合論翻譯？答案是否定的。為證明這一點(diǎn)，首先定義集合傳遞閉包上的互模擬關(guān)系，并且證明所有模態(tài)公式在這個(gè)互模擬概念下不變。

定義5.任給兩個(gè)非空集合a 和b，一個(gè)非空關(guān)系Z ?STC({a})×STC()稱為這兩個(gè)集合傳遞閉包之間的互模擬關(guān)系，如果它滿足如下條件：如果cZd，那么

(1) c ∩Φ=d ∩Φ。

(2) 如果集合s ∈c，那么存在集合t ∈d 使得sZt。

(3) 如果集合t ∈d，那么存在集合s ∈c 使得sZt。

如下圖所示：

這里第一個(gè)條件意思是c 和d 含有相同的命題變?cè)?，因此在集合傳遞閉包中，它們滿足相同的命題變?cè)?。第二個(gè)條件和第三個(gè)條件分別相當(dāng)于基本模態(tài)邏輯中互模擬關(guān)系定義（[5]）中的前進(jìn)條件和后退條件。

命題6.令Z ?STC({a})×STC()是互模擬關(guān)系使得cZd。那么對(duì)任意模態(tài)公式φ，STC({a}),c|=φ 當(dāng)且僅當(dāng)STC(),d|=φ。

證明.對(duì)φ 的構(gòu)造歸納證明。只證φ:=◇ψ 的情況。首先假設(shè)STC({a}),c|=◇ψ。那么存在s ∈c 使STC({a}),s |= ψ。因此存在t ∈d 使sZt。由歸納假設(shè)得STC(),d|=ψ。所以STC(),d|=◇ψ。反之類似證明。

在關(guān)系語(yǔ)義學(xué)中，并非每個(gè)一階公式都等值于某個(gè)模態(tài)公式的標(biāo)準(zhǔn)一階翻譯，一階公式Rxx 就不等值于任何模態(tài)公式的標(biāo)準(zhǔn)一階翻譯（[5]）。那么，在上面給出的集合論翻譯下，利用命題6 的互模擬不變結(jié)果可證如下命題。

命題7.存在一個(gè)集合論公式x ∈x，它不是任何模態(tài)公式的集合論翻譯。

證明.若不然，假設(shè)x ∈x=π(φ,x)?？紤]自然數(shù)上的屬于關(guān)系(ω,∈)。再考慮滿足方程x={x}的集合Ω，令Z={(n,Ω):n ∈ω}是這兩個(gè)集合之間的互模擬關(guān)系使得每個(gè)自然數(shù)n 與集合Ω 互模擬。注意，STC({ω})=ω ∪{ω}=ω+1，并且STC({Ω})=Ω ∪{Ω}。由于Ω= {Ω}，STC({Ω})=Ω ∪Ω=Ω= {Ω}。如下圖所示：

因?yàn)镾TC({Ω}) |= x ∈x[Ω]，所以STC({Ω}) |= π(φ,x)[Ω]。那么根據(jù)定理4，STC({Ω}),Ω|=φ。因?yàn)槊總€(gè)自然數(shù)n 與Ω 互模擬，根據(jù)命題6，STC({ω}),n|=φ。再根據(jù)定理4，STC({ω}),n |= π(φ,x)，所以STC({ω}),n |= x ∈x，但是n/∈n，矛盾。

由于并非所有集合論公式都等價(jià)于某個(gè)模態(tài)公式的標(biāo)準(zhǔn)翻譯，那么一階集合論語(yǔ)言在集合傳遞閉包之間互模擬下不變的片段是否等價(jià)于模態(tài)公式的集合翻譯呢？在第四部分證明該問題的答案是肯定的。下面首先給出一些關(guān)于集合論語(yǔ)言和一階語(yǔ)言之間的關(guān)系的結(jié)論。

3 集合論語(yǔ)言與一階關(guān)系語(yǔ)言

首先我們從模態(tài)語(yǔ)言在集合傳遞閉包上的解釋可以看出，在一個(gè)集合傳遞閉包STC({a}) 中元素之間的屬于關(guān)系相當(dāng)于關(guān)系語(yǔ)義學(xué)下可能世界之間的可及關(guān)系。因此，我們可以使用任意二元關(guān)系R 表示集合上的屬于關(guān)系∈。如下定義集合傳遞閉包STC({a})上的關(guān)系R：

在對(duì)應(yīng)的一階關(guān)系語(yǔ)言中，對(duì)于每一個(gè)命題變?cè)猵，含有一元謂詞符號(hào)P，二元關(guān)系符號(hào)R。對(duì)任何模態(tài)公式φ，定義它的標(biāo)準(zhǔn)翻譯Tr(φ,x)如下：

(1) 對(duì)每個(gè)p ∈Φ，Tr(p,x)=Px

(2) Tr(?φ,x)=?Tr(φ,x)

(3) Tr(φ∧ψ,x)=Tr(φ,x)∧Tr(ψ,x)

(4) Tr(◇φ,x)=?y(Rxy∧Tr(φ,y))

同樣在集合傳遞閉包下也可以解釋上面的公式：任給集合傳遞閉包STC({a})，令σ 是對(duì)變?cè)闹概桑辉^詞解釋P 為STC({a})中含有相應(yīng)的命題變?cè)猵 的子集，二元關(guān)系符號(hào)R 解釋為集合之間的屬于關(guān)系。然后如下解釋一階關(guān)系語(yǔ)言的公式：

(1) STC({a}),σ |=Px ??p ∈σ(x)；

(2) 命題聯(lián)結(jié)詞的解釋與一階邏輯相同；

(3) STC({a}),σ |=?xα ??存在b ∈STC({a})使得STC({a}),σ[b→x]|=?xα這里指派σ[b→x]表示把集合b 指派給變?cè)獂。下面我們表明集合論翻譯和一階翻譯在集合傳遞閉包的語(yǔ)義下是等價(jià)的。

定義8.如下定義從集合論語(yǔ)言到一階關(guān)系語(yǔ)言的翻譯(·)?：

顯然這里定義的翻譯(·)?是一個(gè)雙射。根據(jù)定義，下面這個(gè)命題表明在集合傳遞閉包的語(yǔ)義解釋下，集合翻譯和一階標(biāo)準(zhǔn)翻譯是等價(jià)的。

命題9.對(duì)任何模態(tài)公式φ，集合傳遞閉包STC({a})和其中元素b，如下成立：

為了證明刻畫定理，我們還要引入另一些定義結(jié)論。首先引入超濾擴(kuò)充的概念。任給集合傳遞閉包STC({a})和其中的元素b，前面定義了關(guān)系R，這里定義R[b]={c:c ∈b 并且c 是集合}。任給一個(gè)集合S，令?(S)表示S 的一個(gè)冪集，也就是S 的所有子集的集合。如下定義函數(shù)mR:?(STC({a}))→?(STC({a}))使得：

令lR(X)=STC({a})mR(STC({a}))。

任給集合S，一個(gè)子集族F ??(S)稱為S 上的超濾子，如果它滿足以下條件：

(1) S ∈F；

(2) 如果X,Y ∈F，那么X ∩Y ∈F；

(3) 如果X ∈F 并且X ?Y，那么Y ∈F；

(4) 對(duì)任何X ∈?(S)，X ∈F 當(dāng)且僅當(dāng)SX/∈F。

任給元素x ∈S，由x 生成的超濾子U(x)={X ?S :x ∈X}，即所有含x 的自己組成的集合族。在超濾擴(kuò)充集合中，所有元素都是超濾子，而這些超濾子之間的關(guān)系R#是二元關(guān)系，而不是屬于關(guān)系。

定義10.任給集合傳遞閉包STC({a})，其超濾擴(kuò)充集合為二元組ueSTC({a})=(Uf(STC({a})),R#)：

(1) Uf(STC({a}))是STC({a})上所有超濾子的集合；

(2) 任給兩個(gè)超濾子u 和v，定義R#uv 當(dāng)且僅當(dāng)X ∈v 蘊(yùn)涵mR(X)∈u。

根據(jù)前面的論述，顯然我們可以在任何集合傳遞閉包上定義等價(jià)的模型。任給集合傳遞閉包STC({a})，定義模型M=(STC({a}),R,V)如下：R 關(guān)系即定義(@)；對(duì)任何命題變?cè)猵，集合b ∈V(p)當(dāng)且僅當(dāng)p ∈b。于是很容易得到以下結(jié)論。

命題11.任給集合傳遞閉包STC({a})，令M 是由STC({a})誘導(dǎo)的模型。那么對(duì)所有模態(tài)公式φ 和集合b ∈STC({a})，STC({a}),b|=φ 當(dāng)且僅當(dāng)M,b|=φ。

命題11 建立了模態(tài)語(yǔ)言的關(guān)系語(yǔ)義學(xué)與集合傳遞閉包語(yǔ)義學(xué)之間的聯(lián)系，這一聯(lián)系對(duì)于證明刻畫定理起到了關(guān)鍵作用。

4 刻畫定理

在基本模態(tài)邏輯的關(guān)系語(yǔ)義學(xué)下，van Benthem 刻畫定理（[3,5]）說明，對(duì)于任意一階公式α(x) 邏輯等值于某個(gè)模態(tài)公式的標(biāo)準(zhǔn)翻譯當(dāng)且僅當(dāng)它在互模擬下不變。這條定理對(duì)模態(tài)語(yǔ)言提供了一種刻畫，它使用互模擬不變這個(gè)概念刻畫了基本模態(tài)語(yǔ)言ML 通過標(biāo)準(zhǔn)翻譯嵌入到一階語(yǔ)言FOL 的兩變?cè)蜦OL2：

如下證明van Benthem 刻畫定理對(duì)于集合論語(yǔ)義和集合翻譯是成立的，一階集合論公式α(x)等價(jià)于某個(gè)模態(tài)公式的集合翻譯當(dāng)且僅當(dāng)它在集合互模擬下不變。

根據(jù)基本模態(tài)邏輯的結(jié)論和命題11，如下引理成立。

引理12.任給集合傳遞閉包STC({a})和STC()，令c 和d 分別是這兩個(gè)集合傳遞閉包中的集合，(M,c)和(N,d)分別是那么如下三個(gè)命題等價(jià)：

(1) 對(duì)所有模態(tài)公式φ，STC({a}),c|=φ 當(dāng)且僅當(dāng)STC({a}),d|=φ。

(2) 集合ueSTC({a})與ueSTC({a})之間存在經(jīng)典模態(tài)互模擬關(guān)系。

(3) 存在可數(shù)飽和模型(M?,c?) 和(N?,d?) 使得存在從(M,c) 到(M?,c?) 的初等擴(kuò)張f，并且存在從(N,d) 到(N?,d?) 的初等擴(kuò)張g 使得f(c)= c?，g(d)=d?，并且(M?,c?)與(N?,d?)是互模擬關(guān)系。

稱一個(gè)集合論公式α(x)在集合傳遞閉包之間的互模擬關(guān)系下不變，若對(duì)任何兩個(gè)集合傳遞閉包STC({a})與STC()，如果它們之間存在集合互模擬關(guān)系Z使得cZd，那么STC({a})|=α(x)[c]當(dāng)且僅當(dāng)STC()|=α(x)[d]。

定理13(刻畫定理，[4]).令α(x)是一階集合論公式。那么α(x)在集合互模擬下不變當(dāng)且僅當(dāng)它等價(jià)于某個(gè)模態(tài)公式的集合翻譯。

證明.從右到左的方向容易證明，根據(jù)定理4 和命題6 即得。下面證明從左至右的方向。假設(shè)α(x)在集合互模擬下不變。考慮α(x)的所有為模態(tài)公式的集合翻譯的推論集合Con(α)=π(φ,x):φ 是模態(tài)公式并且α(x)|=π(φ,x)。下面只需要證明：

(*) 如果Con(α)|=α(x)，那么α(x)等價(jià)某個(gè)模態(tài)公式的標(biāo)準(zhǔn)翻譯。

原因如下：假設(shè)Con(α)|=α(x)。根據(jù)緊致性，存在有限集合X ?Con(α)使得X |= α(x)。所以|=∧X→α(x)。顯然|= α(x)→∧X，所以∧X 作為一些模態(tài)公式合取的翻譯，它等價(jià)于α(x)。下面只需要證明Con(α)|=α(x)。

假設(shè)一個(gè)集合傳遞閉包STC({a})|=Con(α)[c]。我們證明STC({a})|=α(x)[c]。構(gòu)造集合T(x)= {π(φ,x) : STC({a}) |= π(φ,x)[c]}。首先證明T(x) ∪α(x)是一致的。假設(shè)它不一致，那么根據(jù)緊致性，存在T(x) 的有窮子集T0(x) 使得|= α(x)→?∧T0(x)。所以?∧T0(x)/∈Con(α)，所以STC({a}) |= ?∧T0(x)[c]，這與STC({a})|=T(x)和T0(x)?T(x)矛盾。

令STC() |= T(x)∪α(x)[d]。如果STC({a}),c |= φ，那么π(φ,x) ∈T(x)，所以STC(),d|=φ。反之，如果STC({a}),c/|=φ，那么STC({a}),c|=?φ，所以STC(),d|=?φ。由此得到：STC({a}),c|=φ 當(dāng)且僅當(dāng)STC(),d|=φ。

假設(shè)(M,c) 是由(STC({a}),c) 誘導(dǎo)的模型，(N,d) 是由(STC(),d) 誘導(dǎo)的模型。所以，M,c |= φ 當(dāng)且僅當(dāng)N,d |= φ。下面分別構(gòu)造(M,c)和(N,d)的初等飽和擴(kuò)張模型(M?,c?)和(N?,d?)。根據(jù)引理12，(M?,c?)與(N?,d?)互模擬，因?yàn)镸,c |= φ 當(dāng)且僅當(dāng)N,d |= φ。由于STC() |= T(x)∪α(x)[d]，所以N |= α(x)[d]。所以由初等飽和擴(kuò)張，N?|= α(x)[d?]。再由互模擬不變條件，M?|=α(x)[c?]。再根據(jù)初等飽和擴(kuò)張，M,c|=α(x)。

5 結(jié)語(yǔ)

模態(tài)邏輯的集合論語(yǔ)義與互模擬不變性是一個(gè)值得研究的重要問題，本文的基本思想是要在模態(tài)邏輯的集合論語(yǔ)義下，定義從模態(tài)語(yǔ)言到集合論語(yǔ)言的翻譯，以及集合傳遞閉包上的互模擬概念，從而研究在集合論語(yǔ)言中對(duì)模態(tài)語(yǔ)言的刻畫，所證明的定理是集合論語(yǔ)義下的van Benthem 刻畫定理。