模態(tài)邏輯的集合論語義與互模擬不變性

史璟

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

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

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

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

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

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

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

(4) a|=◇φ ??存在集合b ∈a 使得b|=φ。一個(gè)命題變元p 在a 上真定義為p 屬于a。因此，集合a 中含有的命題變元不是集合也不是類，我們把這樣的元素稱為本元，本文使用的本元僅指命題變元；其次，公式◇φ 在集合a 上是真的，定義為存在a 中是集合的元素b 滿足φ。我們僅僅在集合上計(jì)算公式的真值，而在本元或命題變元上不計(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ù)，對每個(gè)結(jié)點(diǎn)w 指派集合d(w)使得：如果Rwu，那么d(u)∈d(w)。在經(jīng)典集合論ZF 中，Mostowski 坍塌定理說明，每個(gè)良基圖都有惟一的裝飾。每個(gè)良基圖都對應(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)、對稱點(diǎn)等等，那么這個(gè)圖是非良基圖，所對應(yīng)的集合是非良基集。由于模態(tài)公式在框架基礎(chǔ)上進(jìn)行解釋，所以，在集合上解釋模態(tài)語言，就必須引入非良基集合，以便處理循環(huán)圖。比如模態(tài)公式p→◇p 在任何屬于自身的集合a上是真的。這樣，把集合之間的屬于關(guān)系看作可及關(guān)系，一個(gè)集合就可以看作模態(tài)語言所談?wù)摰年P(guān)系結(jié)構(gòu)。反之，給定一個(gè)關(guān)系結(jié)構(gòu)，也可以通過裝飾函數(shù)把它與一個(gè)集合聯(lián)系起來。

一般地，對任意非空集合a，它的傳遞閉包TC(a)定義為∩{b : a ?b 并且b 是傳遞的}，即包含集合a 的最小傳遞集合。TC(a)中可以含有本元。對每個(gè)集合a，令support(a)= TC(a) ∩Φ（Φ 是命題變元集）。集合support(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})。下面我們在集合傳遞閉包上解釋模態(tài)公式。

定義1.任給非空集合a，如下遞歸定義模態(tài)公式φ 在集合傳遞閉包STC({a})中一個(gè)集合b 上真（記號：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)系語義學(xué)下模型的作用。在集合傳遞閉包上解釋模態(tài)語言，不同于在集合上解釋模態(tài)語言，關(guān)鍵是每次我們從集合中取出的集合都屬于集合傳遞閉包。在后面我們以定義1 提供的模態(tài)邏輯語義為基礎(chǔ)。

2 集合翻譯與互模擬

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

(1) 集合變元：x0,x1,...（使用x、y、z 等表示）；

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

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

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

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

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

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

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

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

這里的變元x 和y 都是集合變元；把命題變元直接翻譯為集合的本元。同樣，對于公式□φ，有如下翻譯：π(□φ,x)=?y(y ∈x→π(φ,y))。在翻譯過程中，如果遇到重疊的模態(tài)詞，由于不同的量詞約束不同的變元，可以交替使用變元x 和y。因此，可以把所有模態(tài)公式翻譯到所定義的集合論語言的兩變元片斷，即只使用兩個(gè)變元的集合論語言片段。

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

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

證明.對φ 的構(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 含有相同的命題變元，因此在集合傳遞閉包中，它們滿足相同的命題變元。第二個(gè)條件和第三個(gè)條件分別相當(dāng)于基本模態(tài)邏輯中互模擬關(guān)系定義（[5]）中的前進(jìn)條件和后退條件。

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

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

在關(guān)系語義學(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)翻譯，那么一階集合論語言在集合傳遞閉包之間互模擬下不變的片段是否等價(jià)于模態(tài)公式的集合翻譯呢？在第四部分證明該問題的答案是肯定的。下面首先給出一些關(guān)于集合論語言和一階語言之間的關(guān)系的結(jié)論。

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

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

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

(1) 對每個(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})，令σ 是對變元的指派，一元謂詞解釋P 為STC({a})中含有相應(yīng)的命題變元p 的子集，二元關(guān)系符號R 解釋為集合之間的屬于關(guān)系。然后如下解釋一階關(guān)系語言的公式：

(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 指派給變元x。下面我們表明集合論翻譯和一階翻譯在集合傳遞閉包的語義下是等價(jià)的。

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

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

命題9.對任何模態(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) 對任何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)系即定義(@)；對任何命題變元p，集合b ∈V(p)當(dāng)且僅當(dāng)p ∈b。于是很容易得到以下結(jié)論。

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

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

4 刻畫定理

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

如下證明van Benthem 刻畫定理對于集合論語義和集合翻譯是成立的，一階集合論公式α(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) 對所有模態(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)系下不變，若對任何兩個(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é)語

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