姚從軍

(湖南科技學院思政部，湖南永州 425100)

雙模擬與模態(tài)邏輯

姚從軍

(湖南科技學院思政部，湖南永州 425100)

首先基于模型上的模擬概念定義了模型上的雙模擬概念，并給出雙模擬模態(tài)不變性和模態(tài)等價性的定義。在此基礎(chǔ)上，討論了模態(tài)邏輯與雙模擬之間的關(guān)系;進一步分別在語言ML(τ，Φ)和ML∞(τ，Φ)中分析了模態(tài)等價性與雙模擬不變性之間的關(guān)系;最后證明了正存在模態(tài)公式與雙模擬之間的關(guān)系，并把正存在模態(tài)公式刻畫為一階公式雙模擬不變部分。

模擬;雙模擬;模態(tài)邏輯;正存在模態(tài)公式;雙模擬不變性

一、基礎(chǔ)知識

定義1.1 基本模態(tài)語言ML(◇，Φ)是由一個命題變項的集合Φ和一元模態(tài)算子◇組成的。其中Φ的元素通常被記作p，q，r等等。基本模態(tài)語言的合式公式φ由下面的規(guī)則給出

φ∷=p|⊥|﹁φ|φ∨ψ|◇φ，其中p∈Φ。

在BML中，如果將∨換為∨(允許無窮)得到無窮模態(tài)語言ML∞。

定義1.2 一個模態(tài)相似型是一個對τ=(0，ρ)，其中0是一個非空集，并且ρ是一個從0到N的函數(shù)，即ρ:0→N。0的元素被稱為模態(tài)算子，我們用Δ，Δ1，Δ2，…表示0中的元素，函數(shù)ρ給每一個算子 Δ∈0指定一個自然數(shù)，表示 Δ的元數(shù)。

為了與定義1.1一致，我們把一元三角Δ1稱作菱形，并且把它們記作或〈a〉，其中的a取自某個標號集。有時，我們假設算子的元數(shù)是已知的，因此，不區(qū)別τ和0。

定義1.3 一個模態(tài)語言ML(τ，Φ)是由一個模態(tài)相似型τ=(0，ρ)和一個命題變項的集合Φ構(gòu)成的。τ和Φ上的模態(tài)公式的集合Form(τ，Φ)由下面的規(guī)則給出

φ∷=p|⊥|﹁φ|φ∨ψ|Δ(φ1，…，φρ(Δ)，其中p∈Φ。

同樣，在ML(τ，Φ)中，如果將∨換為∨(允許無窮)得到無窮模態(tài)語言ML∞(τ，Φ)。

基本模態(tài)語言 ML(◇，Φ)是模態(tài)語言ML(τ，Φ)的一個特例，這里τ只包含一個一元模態(tài)詞。

定義1.4 令τ是一個模態(tài)相似型，一個τ－模型是一個三元組M=(W，{RΔ|Δ∈τ}，V)。這里W是一個非空集;對τ中的每個n(n≥0)元模態(tài)詞Δ，RΔ是W上的n+1元關(guān)系;V是賦值函數(shù)，其定義域為模態(tài)語言ML(τ，Φ)的命題變元集Φ，值域為P(W)。當τ={◇}時，則得到基本模態(tài)語言的模型M=(W，R，V)。

定義1.5 令τ是一個模態(tài)相似型，M=(W，{RΔ|Δ∈τ}，V)是一個τ－模型，如果對M的每一個狀態(tài)w和每一個關(guān)系RΔ(Δ∈τ)，集合{(v1，…，vn)|RΔwv1…vn}是有窮的，則稱M是像有窮的。

二、模型上的雙模擬概念

先給出模型上的模擬定義:

定義2.1 令τ是一個模態(tài)相似型，令M=(W，{RΔ|Δ∈τ}，V)和M'=(W'，{RΔ'|Δ∈τ}，V')是兩個τ－模型，如果Z?W×W'是一個滿足下面的條件二元關(guān)系:對于任意的w∈W，w'∈W'，Δ∈τ，wZw'當且僅當

(i)對所有命題字母p，如果w∈V(p)，那么w'∈V'(p);

(ii)對于所有的v1，…，vn，如果RΔwv1…vn，那么存在v1'，…，vn'∈W'使得RΔ'w'v1'…vn'且對所有的i(1≤i≤n)，viZvi'。

則Z被稱為從M到M'的一個模擬。

對于基本的模態(tài)語言而言，即τ是一個基本模態(tài)相似型，第二條就變?yōu)?

(ii)'對于所有的v∈W，如果Rwv，那么存在v'∈W'使得R'w'v'，并且vZv'［1］110。

如果從M到M'存在一個模擬關(guān)系Z，使得wZw'，那么我們說w'模擬w，或者說Z是w到w'的模擬關(guān)系，也可以記作w →w'。如果M=M'，我們稱Z為M上的一個模擬。

定義2.2 令τ是一個模態(tài)相似性，M=(W，{RΔ|Δ∈τ}，V)和M'=(W'，{RΔ'|Δ∈τ}，V')是兩個τ－模型。如果Z?W×W'是一個滿足下面的條件的二元關(guān)系:對于任意的w∈W，w'∈W'，a∈A，如果wZw'當且僅當

(i)對所有命題字母p，w∈V(p)當且僅當w'∈V'(p);

(ii)存在LTS到LTS'一個模擬關(guān)系為Z1，使得對于所有的v1，…，vn(W，如果RΔwv1…vn，那么存在v1'，…，vn'∈W'使得RΔ'w'v1'…vn'，并且對所有的i(1≤i≤n)，viZ1vi';

(iii)存在LTS到LTS'一個關(guān)系為Z2，且滿足是LTS'到LTS的模擬關(guān)系，使得對于所有的v1'，…，vn'∈W'，如果RΔ'w'v1'…vn'，那么存在v1，…，vn∈W使得RΔwv1…vn，并且對所有的i(1≤i≤n)，viZ2vi'。

則Z?W×W'被稱為從M到M'的一個雙模擬。

如果M的狀態(tài)w和M'的狀態(tài)w'是雙模擬的，那么我們記作Z:(M，w)←→(M'，w')，或者簡寫為(M，w)←→(M'，w')，并且說w'和w互相模擬對方。

對于基本模態(tài)語言，后兩條變?yōu)?

(ii)'存在LTS到LTS'一個模擬關(guān)系為Z1，使得對于所有的v∈W，如果Rwv，那么在W'中存在一個v'使得R'w'v'，并且vZ1v';

(iii)'存在LTS到LTS'一個關(guān)系為Z2，且滿足是LTS'到LTS的模擬關(guān)系，使得對于所有的v'∈W'，如果R'w'v'，那么在W中存在一個v使得Rwv，并且vZ2v'。

在定義2.2中，如果Z1=Z2=Z，則Z就是從M到M'的一種特殊的雙模擬——互模擬［2］。

三、有關(guān)雙模擬的一些事實

定義3.1 M和M'是上述的兩個τ－模型，Z是從M到M'的一個雙模擬，如果下面的兩個條件成立，我們稱 M和 M'是雙模擬等價的，記作MΞM':

對于每個w∈W，存在w'∈W'，并且wZw';

對于每個w'∈W'，存在w∈W，并且wZw'。

定義3.2 M和M'是任意兩個τ－模型，如果下面的條件成立，我們稱τ－模型的一個性質(zhì)φ是雙模擬不變的:

如果(M，w)←→(M'，w')并且M，w╞φ，那么M'，w'╞φ。

事實1 模態(tài)邏輯不具有雙模擬不變性。

也就是說對于非互模擬的雙模擬狀態(tài)來說，我們只要找到模態(tài)公式把它們區(qū)分開來就足夠了，如圖1［3］。P1和Q1是雙模擬的，很顯然P1滿足◇□(p∧﹁p)，而Q1不滿足◇□(p∧﹁p)，所以這個模態(tài)公式不具有雙模擬不變性，并因此模態(tài)邏輯不具有雙模擬不變性。

圖1 進程間的雙模擬關(guān)系

事實2 雙模擬不必然蘊涵模態(tài)等價性。

也就是說，我們可以找到兩個狀態(tài)是雙模擬的，但是它們不具有相同的模態(tài)理論。這個事實和事實1是同一的，其論證也是相同的。

事實3 在ML(τ，Φ)中，模態(tài)等價性不蘊涵雙模擬。

對于模態(tài)語言ML(τ，Φ)來說，如果對模型不加限制，就有可能出現(xiàn)非雙模擬的模態(tài)等價性模型，如圖2［4］:

圖2 非雙模擬的模態(tài)等價模型

在上面的兩個模型中，對每個n∈N，w一個長度為n的分支，w'除了具有w所有分支外，還有一個無窮分支。很容易證明這兩個模型不是“根雙模擬”的:雖然w'可模擬w，但w不可模擬w'，因為w'有一個無窮分支，w沒有這樣的分支。但是在模態(tài)邏輯ML(τ，Φ)里，如果假定每個狀態(tài)滿足相同的原子命題，也不難證明它們是模態(tài)等價的，即具有相同的模態(tài)理論。

在無窮模態(tài)邏輯ML∞(τ，Φ)中，我們就可以有下面的定理:

定理3.1 在ML∞(τ，Φ)中，模態(tài)等價性蘊涵雙模擬。

這個論證是不足道的。我們知道，在ML∞(τ，Φ)中，兩個狀態(tài)(模型)是模態(tài)等價的，它們一定是互模擬的，而互模擬蘊涵雙模擬，所以在ML∞(τ，Φ)中模態(tài)等價蘊涵雙模擬。

四、正存在模態(tài)公式的雙模擬不變性

雖然模態(tài)邏輯不具有雙模擬不變性，是否有一部分模態(tài)公式具有雙模擬不變性呢?答案是肯定的，為此我們先給出下面的定義。

定義4.1 如果一個公式是僅僅使用∧、∨和存在模態(tài)算子△從命題字母生成的公式，那么該公式被稱為正存在模態(tài)公式。為將來證明的方便我們把正存在模態(tài)公式以及與某一正存在模態(tài)公式等價的模態(tài)公式統(tǒng)稱為正存在模態(tài)公式，用MPE表示這一類模態(tài)公式。

定義4.2 對于任意的正存在模態(tài)公式φ∈MPE，任意的模型M和M'及其任意的狀態(tài)w和w'，如果M，w╞φ?M'，w'╞φ，那么稱w和w'是正存在模態(tài)等價的。

定理4.1 正存在模態(tài)公式是雙模擬不變的。

我們只對基本模態(tài)語言證明這一結(jié)論。

證明:令φ∈MPE是任一正存在模態(tài)公式，M和M'是任意的兩個模型，w和w'它們的任意狀態(tài)，且滿足存在一個雙模擬關(guān)系Z使得wZw'?，F(xiàn)在我們用歸納法證明M，w╞φ?M'，w'╞φ。

當φ=p(命題字母)，由雙模擬的定義可知M，w╞p?M'，w'╞p。

當φ=φ∨ψ時，M，w╞φ∨ψ?M，w╞φ∨M，w╞ψ，由歸納假設M，w╞φ∨M，w╞ψ?M'，w'╞φ∨M'，w'╞φ?M'，w'╞φ∨ψ。

當φ=φ∧ψ時，M，w╞φ∧ψ?M，w╞ψ∧M，w╞ψ，由歸納假設M，w╞φ∧ M，w╞φ? M'，w'╞φ∧M'，w'╞φ?M'，w'╞φ∨ψ。

當φ=◇φ時。假設M，w╞◇φ，那么存在一個w的后繼v使得M，v╞φ。因為w和w'是雙模擬的，所以存在從M到M'的模擬關(guān)系Z1使得wZ1w'，再根據(jù)模擬的定義可知存在w'的后繼v'使得vZ1v'，并因此M'，v'╞φ。所以M'，w'╞◇φ。另一個方向的證明與此相同。

筆者把此定理稱之為雙模擬不變性定理。此定理只是說明正存在模態(tài)公式是雙模擬不變的，但是此定理的逆定理是否成立呢?答案是肯定的。在證明此結(jié)論之前，先引入一些概念和定理。

定義4.3 令M=(W，R，V)是一個基本模態(tài)相似型的模型，X是W的一個子集，φ是一個模態(tài)公式集。如果對所有的公式φ∈∑，存在一個狀態(tài)x∈X使得M，x╞φ，我們稱∑在集合X里是可滿足的。如果∑的每個有窮子集在集合X里是可滿足的，我們就稱∑在集合X里是有窮可滿足的。對每個狀態(tài)w∈W和每個模態(tài)公式集∑，如果∑在w的后繼集是有窮可滿足的，那么∑在w的后繼集是可滿足的，我們稱M是m－飽和的。

對任意的模態(tài)相似型來說，m－飽和性定義如下:令τ是一個模態(tài)相似型，M是一個τ－模型。對M的每一個狀態(tài)w，每個n元模態(tài)算子Δ∈τ和模態(tài)公式集序列∑1，…，∑2，如果對每個有窮子集序列Δ1?∑1，…，Δn?∑n，存在狀態(tài)v1，…，vn滿足Rwv1…vn并且v1╞Δ1，…，vn╞Δn，那么在M中存在狀態(tài)v1'，…，vn'滿足Rwv1'…vn'并且v1'╟∑1，…，vn'╞∑n。我們稱M是m－飽和的。

定理4.2 令τ是一個模態(tài)相似型。那么m－飽和的τ模型具有Hennessy-Milner性質(zhì)。這里Hennessy-Milner性質(zhì)的模型類是指互模擬與模態(tài)等價一致的模型類。

證明:見Blackburn《模態(tài)邏輯》第92頁命題2.54的證明［1］。

如何構(gòu)造m－飽和的模型呢?通過超濾子擴張。在定義超濾子擴張時需要用到一個框架的冪集代數(shù)上的運算，現(xiàn)在我們給出其定義。

定義4.4 令τ是一個模態(tài)相似型，F(xiàn)=(W，{RΔ|Δ∈τ})是一個τ－框架，對每個n+1元關(guān)系我們定義W的冪集P(W)上的兩種運算和mΔ。

mΔ(X1，…，Xn)={w∈W|存在w1，…，wn滿足RΔww1…wn并且對所有的i∈n，wi∈Xi}

在基本模態(tài)語言中，m◇(X)是可及X的某個狀態(tài)的點集(X)是只可及X的狀態(tài)的點集，因此可得對任意的模型M，

V(◇φ)=m◇(Vφ))和V(□φ)=mδ◇(V(φ))

另外，超濾子擴張中還涉及到一個模型上的超濾子概念，所以我們先給出濾子和超濾子的定義。

定義4.5 令W是一個非空集，W上的一個濾子F是滿足下列條件的一個集合F?P(W):

(i)W∈F;

(ii)如果X，Y∈F，那么X∩Y∈F;

(iii)如果X∈F，并且X?Z?W，那么Z∈F。

明顯地，P(W)本身就是一個濾子。不同于P(W)的濾子被稱為真濾子。W上的超濾子是W上的極大真濾子，也就是一個真濾子U且滿足對所有的X∈P(W)，X∈U當且僅當WX?U。

定義4.6 令W是一個非空集，對于任意元素w∈W，由w生成的主要超濾子是由單元素集{w}生成的W上的濾子πw，即πw={X?W|w∈X}

定義 4.7 令 τ是一個模態(tài)相似型，F(xiàn)=(W，RΔ)Δ∈τ是一個τ－框架。F的超濾子擴張ueF被定義為框架(Uf(W)，{|Δ∈τ})。這里Uf (W)是W上的超濾子集;成立當且僅當對于W上的超濾子n－元組u0，…，un，所有的i (1≤i≤n)，如果Xi∈ui，那么mΔ(X1，…，Xn)∈u0。

一個τ－模型M=(F，V)的超濾子擴張是一個模型ueM=(ueF，Vue)，這里Vue(pi)是包含元素V(pi)的所有W上的超濾子集合，也就是Vue(pi)={u|V(pi)∈u且u是W上的超濾子}。

定理4.3 令τ是一個模態(tài)相似型，令M是一個τ－模型。那么對任意的公式φ，W上的任意超濾子u，V(φ)∈u，當且僅當ueM，u╞φ。因此，對M的每個狀態(tài)w，我們有(M，w)≈(ueM，πw)。

證明:見Blackburn《模態(tài)邏輯》第96頁命題2.59的證明［1］。

定理4.4 令τ是一個模態(tài)相似型，令M是一個τ－模型。那么ueM是m－飽和的。

證明:見Blackburn《模態(tài)邏輯》第99頁命題2.61的證明［1］。

有了這些定義和定理，就可以證明下面的雙模擬不變性定理。

定理4.5 令τ是一個模態(tài)相似型，φ是一個τ公式。那么φ是雙模擬不變的當且僅當φ是一個正存在模態(tài)公式。

證明:正存在模態(tài)公式在雙模擬下是不變的，見定理3.1。相反，假定φ在雙模擬下是不變的，并且考慮φ的正存在模態(tài)后承的集合:

MPEC(φ)={ψ|ψ是正存在模態(tài)公式，且φ╞ψ}

我們先證明MPEC(φ)╞φ。假設M，w╞MPEC(φ)，我們需要證明M，w╞φ。令

Γ={﹁ψ|ψ是正存在模態(tài)公式，且M，w╞/ ψ}。

首先我們斷定集合{φ}∪Γ是一致的。因為，假定它不一致，則存在公式﹁ψ1，…，﹁ψn∈Γ，使得╞φ→﹁(﹁ψ1∧…∧﹁ψn)，即φ╞ψ1∨…∨ψn。根據(jù)定義，每個公式ψi是一個正存在模態(tài)公式，因此，ψ1∨…∨ψn也是一個正存在模態(tài)公式。據(jù)MPEC(φ)的定義，ψ1∨…∨ψnn∈MPEC(φ)。又根據(jù)假設，M，w╞ψ1∨…∨ψn，由此可得出，對某個i(1≤i≤n)，M，w╞ψi。這與M，w╞/ψi矛盾。

因為集合{φ}∪Γ是一致的，我們可以找到一個模型N和N中一個狀態(tài)v使得N，v╞φ∧∧Γ。顯然，對于每一個正存在模態(tài)公式ψ，如果N，v╞ψ，則M，w╞ψ。這是因為:N，v╞∧Γ?N，v╞Γ，由Γ定義可知，對每一個正存在模態(tài)公式ψ，如果M，w╞/ψ，那么﹁ψ∈Γ，所以N，v╞﹁ψ，即N，v╞/ψ?？梢詮亩ɡ?.3推出，對于超濾子擴張ueM和ueN，我們有同樣的關(guān)系:對每個正存在公式ψ，如果ueN，πv╞ψ，則ueM，πw╞ψ(假設ueN，πv╞ψ，由定理3.3可得N，v╞ψ，由上面的結(jié)論M，w╞ψ，再由定理3.3可得ueM，πw╞ψ)。據(jù)定理3.4，超濾子擴張是m－飽合的，可證這個關(guān)系實際上是一個從ueN，πv到ueM，πw的模擬。

現(xiàn)在證明M，w╞φ。因為N，v╞φ，由定理3.3可得ueN，πv╞φ。因為φ在雙模擬下不變的，所以φ在模擬下是保持的，我們得到ueM，πw╞φ。再次根據(jù)定理3.3，我們得出結(jié)論M，w╞φ。再根據(jù)假設M，w╞MPEC(φ)，可得MPEC (φ)╞φ。根據(jù)緊致性可知，存在MPEC(φ)的有窮個元素φ1，…，φn，使得{φ1，…，φn}╞φ，即φ1∧…∧φn╞φ。由φ1，…φn是正存在公式知φ1∧…∧φn也是正存在公式并且 φ1∧…∧φn∈(MPEC(φ)，根據(jù)MPEC(φ)的定義可知φ╞φ1∧…∧φn，因此╞φ?φ1∧…∧φn。

五、正存在模態(tài)公式的對應定理

由范本特姆刻畫定理，我們知道模態(tài)邏輯對應了一階邏輯互模擬不變的部分，那么正存在模態(tài)公式對應了一階邏輯的哪一部分呢?為此，我們首先要引入一系列概念和定理。

定義5.1 令τ是一個模態(tài)相似型，Φ是一個命題字母的收集。令L1τ(Φ)是一個含有等詞的一階語言，它由與Φ的命題字母p0，p1，p2，…相對應的一元謂詞符號P1，P2，P3，…和τ中的每個n元模態(tài)詞Δ相對應的n+1元關(guān)系符號RΔ構(gòu)成。我們用α(x)表示只有一個自由變元x的一階公式。

定義5.2 令x是一階變元，標準翻譯STx是從模態(tài)公式到L1τ(Φ)中一階公式的一個映射，定義如下:

這里y1，…，yn是新變元(也就是至今在翻譯中還沒使用的變元)。如果使用基本的模態(tài)語言，那么最后一個條件化歸為:

這里R是R◇的簡寫。

定理5.1 固定一個模態(tài)相似型τ，令φ是一個τ－公式。那么:

(i)對所有的模型M和M中的所有狀態(tài)w，M，w╞φ?M╞STx(φ)［w］。

(ii)對所有的模型M:M╞φ當且僅當M╞?xSTx(φ)。

證明:通過φ上的歸納進行證明，這里略。

定義5.3 令α是一個自然數(shù)或ω，M是一個模型，如果對基數(shù)小于α的每個子集A?W，M的擴張MA滿足每個與MA的一階理論一致的L1［A］－公式集Γ(x)，那么模型M就是α－飽和的。一個ω－飽和的模型通常被稱為可數(shù)飽和的［5］。

定理5.2 令τ是一個模態(tài)相似型，任意可數(shù)飽和的τ－模型都是m－飽和的。

證明:見Blackburn《模態(tài)邏輯》第102頁命題2.65的證明［1］。

定義5.4 令M和N兩個模型，其中M的狀態(tài)集(個體域)為A，N的狀態(tài)集(個體域)為B，M到N的一個初等嵌入是一個映射f:A→B(記作: f:M≤N)，且滿足:對所有的公式α(x1，…，xn)和n元組a1，…，an∈A，M╞α(a1，…，an)當且僅當N╞α(f(a1)，…，f(an))。

定理5.3 令τ是一個模態(tài)相似型，并且令M和N是τ－模型，w是M中的狀態(tài)，v是N中的狀態(tài)。那么下面是等價的:

(i)對所有的模態(tài)公式φ:M，w╟φ當且僅當N，v╟φ。

(ii)存在一個互模擬 Z:ueM，πw←→ueN，πv。

(iii)存在可數(shù)的飽和模型M*，w*和N*，v*，及初等嵌入f:M≤M*和g:N≤N*滿足:

(a)f(w)=w*和g(v)=v*

(b)M*，w*←→N*，v*。

這個定理也叫 Detour引理，定理的證明見Blackburn《模態(tài)邏輯》第 102頁命題 2.66的證明［1］。

定義5.5 令α(x)是語言L1τ(Φ)的一個一階公式，如果對任意模型M和N，M中的任意狀態(tài)w，N中的狀態(tài)任意狀態(tài)v及M和N之間的雙模擬Z使得wZv，我們有M╞α(x)［w］當且僅當N╞α(x)［v］，那么我們稱α(x)是雙模擬不變的。

有了這些定義和定理，就可以證明下面的正存在模態(tài)公式對應定理:

定理5.4 令α(x)是L1τ(Φ)的一個一階公式，α(x)是雙模擬不變的當且僅當它(等價于)一個正存在模態(tài)τ－公式的標準翻譯［6］。

證明:從右到左的方向的證明很簡單，如果α (x)等價于一個正存在模態(tài)τ－公式φ的標準翻譯，因為正存在模態(tài)公式是雙模擬不變的，所以α (x)也是雙模擬不變的。

為了證明從左到右的方向，假設α(x)是雙模擬不變的，并且考慮α的正存在模態(tài)后承的標準翻譯集:

STx［MPEC(α)］={STx(φ)|φ是一正存在模態(tài)公式，并且α(x)╞STx(φ)}。

我們首先證明STx［MPEC(α)］╞α(x)。假定M╞STx［MPEC(α)］［w］，我們需要證明M╞α(x)［w］。

令Γ(x)={STx(﹁ψ)|ψ是正存在模態(tài)公式，且M，w╞/ψ}={﹁STx(ψ)|ψ是正存在模態(tài)公式，且M，w╞/ψ}。

現(xiàn)在我們證明Γ(x)∪{α(x)}是一致的。假定它不一致，則存在公式﹁STx(ψ1)，…，﹁STx(ψn)∈Γ (x)使得α(x)╞﹁(﹁STx(ψ1)∧…∧﹁STx(ψn))，即α(x)╞STx(ψ1)∨…∨STx(ψn)。所以對某個ψi(1≤i≤n)，α(x)╞STx(ψi)。由于ψi是一個正存在模態(tài)公式，根據(jù)STx［MPEC(α)］的定義可知，STx(ψi)∈STx［MPEC(α)］。由假設可知，M╞STx(ψi)［w］，根據(jù)定理4.1，M，w╞ψi，這與﹁STx(ψi)∈Γ(x)矛盾。

因為集合Γ(x)∪{α(x)}是一致的，我們可以找到一個模型N和N中一個狀態(tài)v使得N╞(∧T(x)∧α(x))［v］。顯然，對于每一個正存在模態(tài)公式ψ，如果N，v╞ψ，則M，w╞ψ。這是因為:M，w╞/ψ當且僅當﹁STx(ψ)∈Γ(x)，因此N╞﹁STx(ψ)［v］，即N╞STx(﹁ψ)［v］，N，v╞﹁ψ，即N，v╞/ψ。

我們可以部分使用Detour引理來證明我們的結(jié)論。由定理4.3知，存在兩個可數(shù)飽和模型M *，w*(初等嵌入f:M≤M*)和N*，v*(初等嵌入f:N≤N*)，并且對所有的正存在模態(tài)公式ψ，如果N*，v*╞ψ，那么M*，w*╞ψ。因為可數(shù)飽和模型是m－飽和的，可證這個關(guān)系實際上是一個從N*，v* 到M*，w*的模擬。

現(xiàn)在我們來證明M╞α(x)［w］。因為N╞α(x)［v］，根據(jù)初等嵌入，所以N*╞α(x)［v *］，因為α(x)是雙模擬不變的，所以是模擬保持的，于是M*╞α(x)［w*］。再根據(jù)初等嵌入的性質(zhì)，所以M╞α(x)［w］。所以STx［MPEC(α)］╞α(x)。

現(xiàn)在證明α(x)等價于某個正存在模態(tài)公式的翻譯。因為STx［MPEC(α)］╞α(x)，根據(jù)一階邏輯的緊致性定理，對于STx［MPEC(α)］的有窮子集X，我們有X╞α(x)。所以╞∧X→α(x)。不足道地╞α(x)→∧X，因此╞∧X?α((x)。因為每一個β∈X是某個正存在模態(tài)公式的翻譯，所以∧X也是正存在模態(tài)公式的翻譯。

［1］Blackburn P，De Rijke M，Venema Y.Modal Logic［M］.New York:Cambridge University，2001:64－112.

［2］李娜，姚從軍.互模擬的一些基本性質(zhì)［J］.云南師范大學學報，2010(5):70－71.

［3］Sangiorgi.Bisimulation and coinduction:behavious，fixedpoints［M］.unpublished manuscript，2009:15.

［4］姚從軍.走進模態(tài)邏輯的互模擬［J］.科學技術(shù)哲學研究，2010(3):38－39.

［5］王世強.模型論基礎(chǔ)［M］.北京:科學出版社，1984: 145－146.

［6］姚從軍.互模擬理論的邏輯研究［D］.天津:南開大學哲學院，2011.

Two-Way Simulation and Modal Logic

YAO Cong-jun
(Department of politics Hunan University of Sicence and Engineering，Yongzhou 425100，China)

The author defines the concept of two-way simulation on the basis of simulation in kripkle model，and gives the definition of two-way simulational modal invariability and modal equivalence，and discusses on the relationship between the modal logics and two-way simulation;Futhermore，the autuor analyses the relations between the modal equivalence and two-way simulational modal invariability with respect to ML(τ，Φ)and ML∞(τ，Φ);Finally，the autuor proves the relation between the positive existential modal formulas and two-way simulation，and characterize the positive existential modal formulas as the two-way simulational invariable first-order formulas.

simulation;two-way simulation;modal logic;positive existential modal formula;twoway simulational modal invariability

B81

A

1674－8425(2011)08－0077－06

2011－06－06

國家社科基金“超集、互模擬以及在模態(tài)邏輯、計算機科學中的作用研究”(08BZX049)資助項目。

姚從軍(1971—)，男，湖北隨州人，哲學博士，湖南科技學院思政部講師，中國社會科學院哲學所博士后，研究方向:現(xiàn)代邏輯、語言邏輯。

(責任編輯 魏艷君)