史璟

本文首先介紹模態(tài)邏輯的集合論語義，我們在集合傳遞閉包上解釋模態(tài)語言。第二部分定義從模態(tài)語言到集合論語言的翻譯，引入集合傳遞閉包之間的互模擬的概念。第三部分討論集合論語言與一階關(guān)系語言之間的一些聯(lián)系，這是第四部分證明刻畫定理的基礎(chǔ)。第四部分，將證明集合論語義下的刻畫定理，即一個一階集合論公式等價于某個模態(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ù)命題變元集合，◇是一個一元模態(tài)詞。模態(tài)公式按照如下規(guī)則定義：

公式φ 在集合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 滿足φ。我們僅僅在集合上計算公式的真值，而在本元或命題變元上不計算公式的真值。

另一個重要問題是，如上遞歸定義中使用的集合包括非良基集合。在經(jīng)典集合論ZF 中有一條公理稱為正則公理或良基公理，它是說每個非空集合都有屬于關(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)系，一個集合可以按照逆屬于關(guān)系展開為一個圖，而一個圖通過裝飾函數(shù)可以轉(zhuǎn)化為一個集合。一個圖(G,R)是由結(jié)點集G 和結(jié)點之間的二元邊關(guān)系R 組成的，如果Rwu，那么稱u 是w 的子結(jié)點。一個裝飾d 是一個函數(shù)，對每個結(jié)點w 指派集合d(w)使得：如果Rwu，那么d(u)∈d(w)。在經(jīng)典集合論ZF 中，Mostowski 坍塌定理說明，每個良基圖都有惟一的裝飾。每個良基圖都對應(yīng)于由它的所有結(jié)點的裝飾組成的集合。但是，如果考慮非良基圖，比如w 是自身的后繼結(jié)點，那么d(w) ∈d(w)，這樣就存在屬于自身的集合。因此，阿克采爾將Mostowski 坍塌定理推廣為：每個圖都有惟一裝飾。由此引入非良基集合。

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

一般地，對任意非空集合a，它的傳遞閉包TC(a)定義為∩{b : a ?b 并且b 是傳遞的}，即包含集合a 的最小傳遞集合。TC(a)中可以含有本元。對每個集合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})中一個集合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)準集合論翻譯π(φ,x)：

(1) 對每個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)公式翻譯到所定義的集合論語言的兩變元片斷，即只使用兩個變元的集合論語言片段。

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

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

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

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

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

(1) c ∩Φ=d ∩Φ。

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

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

如下圖所示：

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

命題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é)中，并非每個一階公式都等值于某個模態(tài)公式的標(biāo)準一階翻譯，一階公式Rxx 就不等值于任何模態(tài)公式的標(biāo)準一階翻譯（[5]）。那么，在上面給出的集合論翻譯下，利用命題6 的互模擬不變結(jié)果可證如下命題。

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

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

因為STC({Ω}) |= x ∈x[Ω]，所以STC({Ω}) |= π(φ,x)[Ω]。那么根據(jù)定理4，STC({Ω}),Ω|=φ。因為每個自然數(shù)n 與Ω 互模擬，根據(jù)命題6，STC({ω}),n|=φ。再根據(jù)定理4，STC({ω}),n |= π(φ,x)，所以STC({ω}),n |= x ∈x，但是n/∈n，矛盾。

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

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

首先我們從模態(tài)語言在集合傳遞閉包上的解釋可以看出，在一個集合傳遞閉包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)系語言中，對于每一個命題變元p，含有一元謂詞符號P，二元關(guān)系符號R。對任何模態(tài)公式φ，定義它的標(biāo)準翻譯Tr(φ,x)如下：

(1) 對每個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。下面我們表明集合論翻譯和一階翻譯在集合傳遞閉包的語義下是等價的。

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

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

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

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

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

任給集合S，一個子集族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 的自己組成的集合族。在超濾擴充集合中，所有元素都是超濾子，而這些超濾子之間的關(guān)系R#是二元關(guān)系，而不是屬于關(guān)系。

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

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

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

根據(jù)前面的論述，顯然我們可以在任何集合傳遞閉包上定義等價的模型。任給集合傳遞閉包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) 邏輯等值于某個模態(tài)公式的標(biāo)準翻譯當(dāng)且僅當(dāng)它在互模擬下不變。這條定理對模態(tài)語言提供了一種刻畫，它使用互模擬不變這個概念刻畫了基本模態(tài)語言ML 通過標(biāo)準翻譯嵌入到一階語言FOL 的兩變元片段FOL2：

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

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

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

(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?) 的初等擴張f，并且存在從(N,d) 到(N?,d?) 的初等擴張g 使得f(c)= c?，g(d)=d?，并且(M?,c?)與(N?,d?)是互模擬關(guān)系。

稱一個集合論公式α(x)在集合傳遞閉包之間的互模擬關(guān)系下不變，若對任何兩個集合傳遞閉包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)它等價于某個模態(tài)公式的集合翻譯。

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

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

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

假設(shè)一個集合傳遞閉包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)的初等飽和擴張模型(M?,c?)和(N?,d?)。根據(jù)引理12，(M?,c?)與(N?,d?)互模擬，因為M,c |= φ 當(dāng)且僅當(dāng)N,d |= φ。由于STC() |= T(x)∪α(x)[d]，所以N |= α(x)[d]。所以由初等飽和擴張，N?|= α(x)[d?]。再由互模擬不變條件，M?|=α(x)[c?]。再根據(jù)初等飽和擴張，M,c|=α(x)。

5 結(jié)語

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