STIT 邏輯的能力片段初探

何鍵楓

1 引言

STIT（Seeing To It That）理論提出于20 世紀(jì)80 年代，它是研究主體與其行動(dòng)所致結(jié)果之間關(guān)系的一類行動(dòng)邏輯（[2,3,11,15,16]）。有別于其它以動(dòng)態(tài)邏輯為基礎(chǔ)的行動(dòng)邏輯，STIT 理論并不討論主體的行動(dòng)本身，而是聚焦于發(fā)揮能動(dòng)作用的主體之上。形式地說(shuō)，STIT 理論一般情況下是在命題邏輯的基礎(chǔ)上擴(kuò)充以STIT 算子與歷史必然算子而得到的一類模態(tài)邏輯。出于不同的分析需求，文獻(xiàn)中存在不同的STIT 算子（[3,6,7,10]）。以語(yǔ)義最為簡(jiǎn)單的CSTIT 算子為例，公式[i:cstit]φ 的讀法為：主體i 的當(dāng)前行動(dòng)確保φ 的成立。利用歷史可能算子，我們甚至能在STIT 理論的框架下討論主體的能力問(wèn)題：公式的讀法為主體i 能夠確保φ 的成立，其中◇是歷史必然算子□的對(duì)偶。另一方面，得益于STIT 理論的語(yǔ)義模型特點(diǎn)，我們能夠以一種非常自然的方式將個(gè)體STIT 算子推廣為群體STIT 算子（[9]），群體的共同行動(dòng)（joint action）乃至群體的能力亦能在STIT 理論下得到刻畫(huà)。

盡管個(gè)體STIT 算子能夠被非常自然地推廣為群體STIT 算子，關(guān)于個(gè)體STIT 算子的技術(shù)結(jié)果，如邏輯的可判定性、可靠完全的公理系統(tǒng)等（[21,22]），卻未能在群體STIT 算子中得以保留。文獻(xiàn)[8]將群體STIT 邏輯的公式可滿足問(wèn)題歸約為乘積邏輯S5n的公式可滿足問(wèn)題，從而證明了當(dāng)主體集的基數(shù)大于等于3 時(shí)，群體STIT 邏輯不可判定且無(wú)法有窮公理化。面對(duì)上述群體STIT 邏輯的否定性結(jié)果，一個(gè)自然的思路是放棄整個(gè)群體STIT 邏輯，轉(zhuǎn)而考慮STIT邏輯的特殊片段：文獻(xiàn)[13]通過(guò)嚴(yán)格限制公式的構(gòu)造，尤其是歷史必然算子與群體STIT 算子的疊置，從而得到了群體STIT 邏輯的一個(gè)可判定片段以及相應(yīng)的公理系統(tǒng)；文獻(xiàn)[18]則定義了一類由群體構(gòu)成的格，并且將群體STIT 算子的構(gòu)造限制在格點(diǎn)上，從而得到了群體STIT 邏輯的又一可判定片段與相應(yīng)的公理系統(tǒng)；文獻(xiàn)[5]討論了STIT 理論的一個(gè)基于時(shí)態(tài)邏輯的擴(kuò)充，其中代替CSTIT 算子而新引入的XSTIT 算子（可視作的縮寫(xiě)，其中X 是表示下一刻的明日算子）由于不滿足交集性質(zhì)，同樣得到了有窮的公理系統(tǒng)并保持了可判定性；文獻(xiàn)[23]通過(guò)弱化群組CSTIT 算子的交集性質(zhì)，得到了基于Z 型STIT 框架且含有直到算子與自從算子的可判定片段。

本文的結(jié)構(gòu)如下：在第2 節(jié)中，我們將重點(diǎn)放在STIT 邏輯包含個(gè)體的能力片段上，并證明如果只考慮能力片段，每個(gè)STIT 模型都存在等價(jià)的鄰域模型。以此為基礎(chǔ)，本文給出一個(gè)公理系統(tǒng)，并通過(guò)逐步構(gòu)造法證明其完全性。對(duì)STIT 邏輯包含群體的能力片段的討論則是第3 節(jié)的任務(wù)，我們利用類似的方法證明包含群體的能力片段的完全性。最后，我們?cè)诘? 節(jié)中對(duì)本文的工作進(jìn)行總結(jié)，并簡(jiǎn)單討論將來(lái)的研究思路。

2 個(gè)體STIT 理論的能力片段

本節(jié)討論STIT 理論中只含個(gè)體的能力片段。我們先介紹STIT 理論經(jīng)典的BT+AC 模型，并證明只考慮能力片段時(shí)，每個(gè)BT+AC 模型都對(duì)應(yīng)于一個(gè)等價(jià)的鄰域模型。因此，當(dāng)考慮完全性證明時(shí)，本文的策略是為每個(gè)一致公式集構(gòu)造相應(yīng)的鄰域模型。

2.1 語(yǔ)言與語(yǔ)義

預(yù)設(shè)可數(shù)命題變?cè)疨ROP 與有窮的非空主體集AGT，并考慮語(yǔ)義最為簡(jiǎn)單的CSTIT 算子與歷史可能算子。下面給出公式的定義：

定義1(公式).公式由以下BNF 遞歸定義得到：

將上面定義構(gòu)造的公式稱為個(gè)體STIT 邏輯的能力片段，本節(jié)中公式均為個(gè)體STIT 理論的能力片段公式。值得一提的是，當(dāng)時(shí)，歷史必然算子□是冗余的，即□φ 邏輯等值于，其中i,j 為不同主體（[1]）。因此，本文處理的其實(shí)是形如的公式。

下面給出STIT 理論的形式語(yǔ)義，STIT 理論的語(yǔ)義框架BT+AC 由兩部分構(gòu)成。其中，BT 是分支時(shí)間理論的縮寫(xiě)（[17,19,20]）。分支時(shí)間理論以類樹(shù)結(jié)構(gòu)表示非決定的世界：向前可分支表示將來(lái)未定，向后不分支表示過(guò)去唯一。歷史是類樹(shù)結(jié)構(gòu)中的極大鏈，直觀意義為世界的一種可能的完整演變進(jìn)程。

定義2(分支時(shí)間).分支時(shí)間結(jié)構(gòu)T=(W,＜)是滿足下面條件的二元組：

· W 為非空時(shí)刻集，＜是W 上嚴(yán)格偏序，表示狀態(tài)的先后關(guān)系；

· ＜滿足樹(shù)狀性：對(duì)于任意w1與w2，如果w1＜w3且w2＜w3，那么w1=w2或w1＜w2或w2＜w1成立；

· ＜滿足歷史關(guān)聯(lián)性：對(duì)于任意w1與w2，存在w0滿足w0≤w1且w0≤w2，其中≤為＜的自反閉包。

給定分支時(shí)間結(jié)構(gòu)T=(W,＜)，將歷史定義為W 中關(guān)于嚴(yán)格偏序＜的極大子集h，即任取w,v ∈h 均是關(guān)于＜可比較的且不存在h 的真超集滿足前面條件。將所有歷史的集合記作HT并用Hw表示所有穿過(guò)狀態(tài)w 的歷史集合，w ∈h 的直觀意義為世界在歷史h 中曾演變?yōu)闋顟B(tài)w。給定歷史h1,h2∈Hw，如果存在w ＜w′滿足，則稱h1與h2在狀態(tài)w 中未分離。給定歷史h與狀態(tài)w，如果w ∈h，則稱序?qū)?w,h)為索引。

STIT 模型的第二部分AC 是將每個(gè)主體i 映射到相應(yīng)選擇的Choice 函數(shù)，Choice 函數(shù)規(guī)定了主體在世界中能夠作出的選擇。Choice 函數(shù)的數(shù)學(xué)定義如下：給定狀態(tài)w 與主體i，是Hw的分劃，主體i 在狀態(tài)w 的選擇正是分劃中對(duì)應(yīng)的等價(jià)類。上述處理的背后直觀為：當(dāng)世界演變至狀態(tài)w 時(shí)，主體i 的選擇c 將會(huì)使某些可能的演變進(jìn)程不再可能，主體i 在狀態(tài)w 作出選擇c的結(jié)果是世界之后的演變將局限于c 對(duì)應(yīng)的等價(jià)類中。STIT 理論正是將選擇帶來(lái)的結(jié)果等同于選擇本身。特別地，Choice 函數(shù)還需滿足兩個(gè)額外條件：首先，要保證未分離歷史是不可區(qū)分的，即如果h1與h2在w 上未分離，h1與h2屬于中的相同等價(jià)類。其次，要保證主體之間是相互獨(dú)立的，即對(duì)于所有狀態(tài)w、所有主體i 與對(duì)應(yīng)選擇，均有并非空集。其中，是中等價(jià)類，即主體i 在時(shí)刻w 中可作的選擇。

定義3(經(jīng)典STIT 模型).經(jīng)典STIT 模型M=(W,＜,Choice,V)是滿足下列條件的四元組：

下面給出基于經(jīng)典STIT 模型的形式語(yǔ)義。需注意對(duì)應(yīng)的點(diǎn)模型是索引，而非分支時(shí)間結(jié)構(gòu)中的狀態(tài)。

定義4(滿足).給定模型M=(W,＜,Choice,V)與索引(w,h)，稱(w,h)滿足φ當(dāng)且僅當(dāng)：

定義5(鄰域STIT 模型).鄰域STIT 模型是滿足條件的三元組(W,{σi:i ∈AGT},V)：

· W 是非空狀態(tài)集；

-對(duì)于任意w,v ∈W 均有σi(w)=σi(v)2之所以要求所有點(diǎn)都必須具有相同的i 鄰域，是因?yàn)閕 鄰域?qū)?yīng)主體i 能作出的選擇。；

-對(duì)于任意w ∈W 均有σi(w)是W 上的分劃；

在鄰域STIT 模型中遞歸定義公式的滿足，特別地對(duì)于公式，定義當(dāng)且僅當(dāng)存在滿足任意u ∈U 均有成立。值得一提的是，本文采用的鄰域語(yǔ)義與經(jīng)典鄰域語(yǔ)義存在細(xì)微區(qū)別：經(jīng)典鄰域語(yǔ)義只有在鄰域框架滿足單調(diào)性時(shí)，語(yǔ)義才具備存在-任意特點(diǎn)。另一方面，注意到這個(gè)定義與經(jīng)典STIT 模型下定義的相似之處，事實(shí)上，我們有以下結(jié)果：

命題1.公式在經(jīng)典STIT 模型上可滿足當(dāng)且僅當(dāng)其在鄰域STIT 模型上可滿足。

推論1.個(gè)體STIT 理論的能力片段是可判定的。

同樣地，容易得到個(gè)體STIT 理論能力片段的復(fù)雜度上限：已知不含時(shí)態(tài)算子的個(gè)體STIT 理論在時(shí)是NEXPTIME 完全的（[1]），相同條件下個(gè)體STIT 理論能力片段的可滿足問(wèn)題最壞是在確定型圖靈機(jī)中指數(shù)時(shí)間內(nèi)可檢驗(yàn)的。最后，我們?cè)谙旅娼o出個(gè)體STIT 理論能力片段的一個(gè)公理系統(tǒng)。

定義6.表1 與表2 的公理模式與推理規(guī)則構(gòu)成希爾伯特式公理系統(tǒng)ABI.I。

表1:ABI.I 的公理模式

表2:ABI.I 的推理規(guī)則

命題2(可靠性).公理系統(tǒng)ABI.I 是可靠的。

2.2 完全性結(jié)果

我們證明上節(jié)給出的公理系統(tǒng)的完全性，即證明一致的公式集都是可滿足的。具體的思路是為一致公式集構(gòu)造出滿足的鄰域STIT 模型。由于典范模型無(wú)法保證典范鄰域函數(shù)恰好給出論域的分劃（關(guān)于鄰域語(yǔ)義的典范模型可參考文獻(xiàn)[14]），本文的策略為通過(guò)逐步構(gòu)造進(jìn)行逼近，從而在極限條件下得到所需模型。逐步構(gòu)造法中使用的概念如網(wǎng)絡(luò)、融貫性與飽和性等，參考文獻(xiàn)[4]。

預(yù)設(shè)AGT={1,...,k}并給出網(wǎng)絡(luò)的定義，其中關(guān)于極大一致集的定義與性質(zhì)可參考文獻(xiàn)[4]。

定義7(網(wǎng)絡(luò)).網(wǎng)絡(luò)是三元組，滿足以下條件：

· 標(biāo)簽函數(shù)ρ 將任意s ∈S 映射到某個(gè)極大一致集。

定義8(融貫性).網(wǎng)絡(luò)μ=(S,{σi:0 ≤i ≤k},ρ)是融貫的當(dāng)且僅當(dāng)3不難發(fā)現(xiàn)，條件C1-3 分別對(duì)應(yīng)鄰域STIT 框架的相關(guān)條件，條件C4 則對(duì)應(yīng)鄰域STIT 模型上的語(yǔ)義特點(diǎn)，即：存在s 滿足M,= 當(dāng)且僅當(dāng)對(duì)于任意s 均有M,s|=。：

當(dāng)網(wǎng)絡(luò)μ 滿足融貫條件C1 時(shí)，μ 的可數(shù)性將保證μ 擁有可數(shù)鄰域。

定義9(飽和性).網(wǎng)絡(luò)是飽和的當(dāng)且僅當(dāng)對(duì)于任意公式φ，如果存在s ∈S 與i 符合0 ≤i ≤k 滿足，則對(duì)于任意均存在u ∈U 滿足φ ∈ρ(u)。

如果網(wǎng)絡(luò)是融貫飽和的，稱該網(wǎng)絡(luò)是完美的。給定一個(gè)完美網(wǎng)絡(luò)μ，定義賦值函數(shù)并稱對(duì)應(yīng)模型Mμ為網(wǎng)絡(luò)μ 生成的模型。施歸納于公式的結(jié)構(gòu)容易證明下面引理。

引理1(真值引理).令μ 為可數(shù)無(wú)窮的完美網(wǎng)絡(luò)，對(duì)于任意公式φ 與任意s ∈S，滿足：Mμ,s|=φ 當(dāng)且僅當(dāng)φ ∈ρ(s)。

根據(jù)上面引理，給定一致公式集φ 并將其擴(kuò)充為極大一致集，只需要構(gòu)造完美網(wǎng)絡(luò)滿足存在s ∈S 使得Φ ?ρ(s)，我們便能得到相應(yīng)的模型。另一方面，完美網(wǎng)絡(luò)可以在融貫網(wǎng)絡(luò)的基礎(chǔ)上，通過(guò)逐步移除融貫網(wǎng)絡(luò)中不滿足飽和要求的反例，從而在極限條件下定義出來(lái)。

定義10(缺陷).令為融貫網(wǎng)絡(luò)，公式為μ 中缺陷當(dāng)且僅當(dāng)存在s ∈S 與U ∈σi(s)滿足任意u ∈U 均有φρ(u)。

給定融貫網(wǎng)絡(luò)μ 與μ 中缺陷D，我們可以通過(guò)擴(kuò)充網(wǎng)絡(luò)的方式修補(bǔ)缺陷。但是，由于任意地向鄰域添加元素可能會(huì)破壞融貫條件C5，我們引入基于網(wǎng)絡(luò)μ 與公式集Γ 的輔助函數(shù)λ。下面給出輔助函數(shù)λ 與網(wǎng)絡(luò)擴(kuò)充的嚴(yán)格定義：

定義11(輔助函數(shù)).λ 是基于與Γ 的輔助函數(shù)當(dāng)且僅當(dāng)：

定義12(擴(kuò)充).給定網(wǎng)絡(luò)稱μ′是μ 的擴(kuò)充當(dāng)且僅當(dāng)：

引理2.令Φ 為極大一致集，存在融貫網(wǎng)絡(luò)與基于μ以及的輔助函數(shù)λ，其中存在s ∈S 且ρ(s)=Φ。特別地，μ 是可數(shù)網(wǎng)絡(luò)。

將{0,...,j-1}記作AGT′，將AGT′關(guān)于的補(bǔ)集記作AGT′′，對(duì)于任意i ∈AGT′，輔助函數(shù)λjn保證了存在單射非滿射函數(shù)為相應(yīng)能力公式指派證據(jù)鄰域。令。盡管W 在嚴(yán)格意義上并非子集，它顯然唯一對(duì)應(yīng)于的某個(gè)子集，因此不會(huì)引起混淆。將記作V。

給定序?qū)?w1,w2)∈W，它對(duì)應(yīng)于某個(gè)合取。我們?cè)谇懊嬉呀?jīng)驗(yàn)證過(guò)∪ 的一致性，將其擴(kuò)充為極大一致集并記作Γ(w1)。引入個(gè)新點(diǎn)并將這些新點(diǎn)標(biāo)簽為Γ(w1)。即，對(duì)于任意，引入新點(diǎn)s(w1,w2)并將其標(biāo)簽為Γ(w1)。將引入的新點(diǎn)集記作S(w1)并注意到。對(duì)于任意并非空集當(dāng)且僅當(dāng)。

其中，

現(xiàn)在驗(yàn)證μjn+1是否為滿足C1-C4 的可數(shù)網(wǎng)絡(luò)。根據(jù)選擇公理可知可數(shù)個(gè)可數(shù)集合的并集依然可數(shù)，故S′可數(shù)且對(duì)于i≠j 有。此外，依然可數(shù)。令為新構(gòu)造的鄰域，則U為的證據(jù)。任取，則顯然存在與x 一一對(duì)應(yīng)。如果，顯然有∩并非空集。如果x′∈V，則存在使得，再次得到∩并非空集。

由上可知我們完成了對(duì)μjn+1的定義，我們還需要定義輔助函數(shù)λjn+1。然而，λjn+1的定義是顯然的：對(duì)于任意i 符合0 ≤i ≤j-1 以及，定義為在μjn+1中的擴(kuò)充；對(duì)于任意，定義；令中新增鄰域，定義。上面的構(gòu)造保證了我們對(duì)λjn+1的定義是成功的且相對(duì)于λjn合適。

對(duì)于任意i 符合0 ≤i ≤k，稱Sj+1的子集構(gòu)成的可數(shù)序列{An:n ∈ω}是關(guān)于i的鄰域鏈，如果該序列滿足：第一，{An:n ∈ω}是非降序列；第二，存在m ∈ω滿足任意n ∈ω 均有4特別地，如果m=0，此時(shí)默認(rèn)Sjm-1為空集。；第三，如果則相交為空。定義為：

不難驗(yàn)證μ 是滿足C1-C4 的可數(shù)網(wǎng)絡(luò)：S 是可數(shù)個(gè)可數(shù)集合的并，因此是可數(shù)的；對(duì)于融貫性，只驗(yàn)證融貫條件C1，假設(shè)s′∈S 則存在最小的n 滿足s′∈Sjn。注意到是對(duì)Sjn的分劃，因此存在滿足。不難找到鄰域鏈I 滿足。另一方面，容易驗(yàn)證給定關(guān)于j的鄰域鏈I,I′，則有∪I=∪I′當(dāng)且僅當(dāng)I=I′。因此是Sj+1上分劃。

現(xiàn)在只剩下定義出滿足條件的基于μj+1與的輔助函數(shù)λj+1。對(duì)于任意i 符合，定義為包含的關(guān)于i 的鄰域鏈的并集，輔助函數(shù)序列λj0,...,λjn,...保證了任意均有成立；對(duì)于任意n ∈ω，定義為包含的關(guān)于j 的鄰域鏈的并集。輔助函數(shù)序列λj0,...,λjn,...保證了任意均有成立。關(guān)于輔助函數(shù)的其他要求顯然滿足。

因此，我們成功定義了滿足條件的網(wǎng)絡(luò)μj+1與輔助函數(shù)λj+1。注意到AGT 是有窮的，只需要將以上的步驟重復(fù)有窮多次，便可得到一個(gè)可數(shù)融貫網(wǎng)絡(luò)以及基于μ 以及的輔助函數(shù)λ，其中。

引理3(修補(bǔ)引理).令為可數(shù)融貫網(wǎng)絡(luò)且λ 為基于μ以及的輔助函數(shù)，其中s ∈S 成立。假設(shè)D 為μ 中缺陷。存在μ 的一個(gè)可數(shù)融貫擴(kuò)充且基于μ′的輔助函數(shù)λ′滿足λ′相對(duì)于λ 合適。特別地，D 并非μ′中缺陷。

其中，

不難驗(yàn)證μ′是μ 的可數(shù)融貫擴(kuò)充，并非其中缺陷。μ′并沒(méi)有增加鄰域，而我們對(duì)原有鄰域中新增的點(diǎn)并不會(huì)破壞融貫條件C5。對(duì)于輔助函數(shù)λ′的定義是顯然的：對(duì)于任意i 符合0 ≤i ≤k 以及，只需定義為λ在μ′的擴(kuò)充。λ′顯然是相對(duì)于λ 合適的。

命題3(完全性).一致公式集都是可滿足的。

對(duì)于任意i 符合0 ≤i ≤k，σi的定義類似前面。稱S 的子集構(gòu)成的可數(shù)序列{An:n ∈ω}為關(guān)于i 的鄰域鏈，如果{An:n ∈ω}滿足下面條件：第一，{An:n ∈ω}是非降序列；第二，對(duì)于任意n ∈ω 均有An∈(s)成立，其中是μn中關(guān)于i 的鄰域函數(shù)。根據(jù)我們對(duì)μn的定義，必然存在關(guān)于i 的鄰域鏈。定義σi(s)如下：

類似引理2 容易證明μ 是可數(shù)融貫網(wǎng)絡(luò)且容易定義出相應(yīng)的輔助函數(shù)λ。

現(xiàn)在驗(yàn)證μ 是飽和網(wǎng)絡(luò)。如果D=Dk是μ 中某個(gè)缺陷，則存在μn使得Dk在其中是缺陷。注意到D 最壞也是μn+k的最優(yōu)先缺陷。故并非μn+k+1中缺陷。注意到任取均有對(duì)應(yīng)的(s)是其子集，故U 中存在的證據(jù)，矛盾。

推論2(緊致性).對(duì)于任意公式集Θ，Θ 是可滿足的當(dāng)且僅當(dāng)每個(gè)有窮子集都是可滿足的。

3 群體STIT 理論的能力片段

本節(jié)討論STIT 理論中包含群體的能力片段。我們首先介紹群體STIT 算子的語(yǔ)義推廣，并給出當(dāng)只考慮群體能力片段時(shí)，經(jīng)典BT+AC 模型與鄰域STIT 模型的等價(jià)性。在后者的基礎(chǔ)上，本節(jié)證明群體STIT 理論的能力片段具備有窮模型性質(zhì)。

3.1 語(yǔ)言與語(yǔ)義

預(yù)設(shè)可數(shù)命題變?cè)疨ROP、有窮的非空主體集AGT 以及對(duì)應(yīng)的非空群體集GRP，并考慮語(yǔ)義最為簡(jiǎn)單的CSTIT 算子與歷史可能算子。下面給出公式的定義。

定義13(公式).公式由以下BNF 遞歸定義得到：

將上面定義構(gòu)造的公式稱為群體STIT 邏輯的能力片段，本節(jié)中公式均為群體STIT 理論的能力片段公式。

現(xiàn)在說(shuō)明群體STIT 理論將個(gè)體STIT 算子推廣為群體STIT 算子這一處理的背后直觀：個(gè)體i 在狀態(tài)w 的行動(dòng)令世界的演變可能局限于Hw,i，個(gè)體j 在狀態(tài)w 的行動(dòng)令世界的演變可能局限于Hw,j。因此，個(gè)體i 與個(gè)體j 的聯(lián)合行動(dòng)令世界的演變可能局限于，主體的相互獨(dú)立性確保了并非空集。遵循個(gè)體STIT 理論對(duì)能動(dòng)性的刻畫(huà)，交集便是群體{i,j}能夠選擇的行動(dòng)。

定義14(滿足).給定經(jīng)典STIT 模型M 與索引(w,h)，鄰域STIT 模型M′與狀態(tài)w′，分別定義◇[G:cstit]φ 在不同模型上的解釋：

命題4.公式在經(jīng)典STIT 模型上可滿足當(dāng)且僅當(dāng)其在鄰域STIT 模型上可滿足。

下面現(xiàn)在給出群體STIT 理論的能力片段中公式在有窮模型上滿足的充分條件。給定鄰域STIT 模型M 與其中狀態(tài)s 并定義為公式集，用表示前者關(guān)于邏輯等值的商集并用表示公式關(guān)于邏輯等值的等價(jià)類。稱模型M 是關(guān)于語(yǔ)言證據(jù)獨(dú)立的，當(dāng)且僅當(dāng)對(duì)于任意i ∈AGT 均存在單射非滿射函數(shù)滿足：如果是公式的證據(jù)。

定義15(模態(tài)度).函數(shù)deg 遞歸定義如下：

命題5.如果公式在證據(jù)獨(dú)立的模型上是可滿足的，則公式在有窮模型上是可滿足的。

證明.給定公式φ 并假設(shè)存在證據(jù)獨(dú)立的鄰域STIT 模型M,w|=φ 成立。將φ中出現(xiàn)的命題變?cè)獦?gòu)成的集合記作P 并假設(shè)φ 的模態(tài)度為n。如果n=0，命題公式φ 顯然能在有窮模型上滿足，只考慮n ＞0 的情況。在邏輯等值的意義下，模態(tài)度不大于n 且只由P 中命題變?cè)獦?gòu)成的公式僅有窮多個(gè)。給定公式ψ，如果ψ 的模態(tài)度不大于n，其中出現(xiàn)的命題變?cè)霈F(xiàn)在P 中且M,w|=ψ，將其記作P(ψ)。

下面證明對(duì)于模態(tài)度不大于n 且只由P 中命題變?cè)獦?gòu)成的公式ψ 與任意v ∈W′，M,v|=ψ 成立當(dāng)且僅當(dāng)M′,v|=ψ 成立。

因此，如果w ∈W′成立，便能直接得到成立。否則，可以擴(kuò)充W′為W′∪{w}，對(duì)于任意i ∈AGT，將對(duì)應(yīng)的Ri等價(jià)類Xi擴(kuò)充為。將對(duì)應(yīng)模型記作M′′。類似地，可證明對(duì)模態(tài)度不大于n 且只由P 中命題變?cè)獦?gòu)成的公式ψ 與任意成立當(dāng)且僅當(dāng)成立。

因此，只要證明群體STIT 理論的能力片段中每個(gè)公式都是在證據(jù)獨(dú)立的模型上可滿足，就證明了群體STIT 理論的能力片段具備有窮模型性質(zhì)。下面給出群體STIT 理論能力片段的一個(gè)公理系統(tǒng)。

定義16(公理系統(tǒng)).表3 與表4 中公理模式5A7 要求G∩G′ 為空集。與推理規(guī)則構(gòu)成希爾伯特式公理系統(tǒng)ABI.C。

命題6(可靠性).公理系統(tǒng)ABI.C 是可靠的。

表3:ABI.C 的公理模式

表4:ABI.C 的推理規(guī)則

在本節(jié)的最后，我們給出一個(gè)含歷史必然算子□、表示下一刻的明日算子X(jué) 以及表示上一刻的昨日算子Y 的群體能力片段的公理系統(tǒng)，可以證明該系統(tǒng)關(guān)于文獻(xiàn)[12]中離散的關(guān)系STIT 框架可靠完全，思路類似于下節(jié)證明但需作修改，本文略去這一證明。

定義17(公理系統(tǒng)).表5 與表6 中公理模式與推理規(guī)則構(gòu)成希爾伯特式公理系統(tǒng)ABI.CXY。

命題7(可靠性).公理系統(tǒng)ABI.CXY 是可靠的。

3.2 完全性結(jié)果

下面證明上節(jié)給出的公理系統(tǒng)ABI.C 的完全性，具體思路依然是為一致公式集逐步構(gòu)造滿足的鄰域STIT 模型。我們繼續(xù)預(yù)設(shè)AGT={0,...,k}并令GRP 為所有非空群體集。我們直接將簡(jiǎn)記為。令Φ 為公式集，我們用表示公式集，用表示公式集。

定義18(融貫性).網(wǎng)絡(luò)μ=(S,{σi:0 ≤i ≤k},ρ)是融貫的當(dāng)且僅當(dāng)：

表5:ABI.CXY 的公理模式

表6:ABI.CXY 的推理規(guī)則

定義19(飽和性).網(wǎng)絡(luò)是飽和的當(dāng)且僅當(dāng)對(duì)于任意公式φ，如果存在s ∈S 與G ∈GRP 滿足，則對(duì)于任意i ∈G 以及Ui∈σi(s)均存在滿足φ ∈ρ(u)。

關(guān)于完美網(wǎng)絡(luò)、由網(wǎng)絡(luò)生成的模型仿照前面定義，不難驗(yàn)證關(guān)于完美網(wǎng)絡(luò)生成模型的真值引理。

定義20(缺陷).令并令s ∈S，公式為μ中缺陷當(dāng)且僅當(dāng)對(duì)于任意i ∈G 均存在Ui∈σi(s)滿足任意均有。

定義21(輔助函數(shù)族).是基于與Γ 的輔助函數(shù)族當(dāng)且僅當(dāng)：

1.μ 滿足融貫條件C1-C4；

2.存在s ∈S 滿足Γ ?ρ(s)且任意φ ∈Γ 均為形如〈[G]〉cψ 的能力公式；

3.對(duì)于任意i 符合0 ≤i ≤k，λi:Γ-→?(?(S))是部分函數(shù)滿足:

按照第2.2 節(jié)中的方法并進(jìn)行適度調(diào)整，對(duì)于任意極大一致集Σ，我們都可以構(gòu)造一個(gè)可數(shù)網(wǎng)絡(luò)滿足：μ 滿足融貫條件C1-C4且存在s ∈S 有Σ=ρ(s)；存在基于μ 以及的輔助函數(shù)族；對(duì)于任意i 符合0 ≤i ≤k 與公式φ，并非μ 中缺陷。稱滿足上述條件的網(wǎng)絡(luò)μ 是相對(duì)于Σ 的個(gè)體擬完美網(wǎng)絡(luò)。

引理4.給定極大一致集Σ，令μ 為相對(duì)于Σ 的個(gè)體擬完美網(wǎng)絡(luò)且i ≤k} 為對(duì)應(yīng)的輔助函數(shù)族。存在μ 的可數(shù)融貫擴(kuò)充μ*以及基于μ*與的輔助函數(shù)族。特別地，μ*是相對(duì)于Σ 的個(gè)體擬完美網(wǎng)絡(luò)且是相對(duì)于合適的。

最后，對(duì)于任意i ∈G，我們要保證新引入的鄰域Ui滿足融貫條件C3。盡管Ui尚未被定義，我們?cè)谙挛膶?duì)它們的指稱將不會(huì)引起歧義。將記作W，不難發(fā)現(xiàn)任意W 對(duì)應(yīng)于一個(gè)鄰域組合。特別地，對(duì)于i ∈G，需要留意i 分量恰好為Ui的向量。將這樣的向量構(gòu)成的W 的子集記作V。

其中，

對(duì)于任意i 符合0 ≤i ≤k，稱Sj+1的子集構(gòu)成的可數(shù)序列{An:n ∈ω}是關(guān)于i的鄰域鏈，如果該序列滿足：第一，{An:n ∈ω}是非降序列；第二，存在m ∈ω滿足任意n ∈ω 均有；第三，如果An?An+1則An+1An與Sjn+m相交為空。定義為：

類似于引理2，容易驗(yàn)證μj+1是滿足條件的網(wǎng)絡(luò)并由此得到相應(yīng)的輔助函數(shù)族。只需要重復(fù)上述步驟有窮多次，我們便能得到滿足條件的μ*以及相應(yīng)輔助函數(shù)族。

引理5(修補(bǔ)引理).令為可數(shù)融貫網(wǎng)絡(luò)且{λi:0 ≤i ≤k} 為基于μ 以及的輔助函數(shù)族，其中s ∈S 成立。假設(shè)D 為μ 中缺陷。存在μ 的一個(gè)可數(shù)融貫擴(kuò)充以及基于μ′與的輔助函數(shù)族滿足λ′相對(duì)于{λi:0 ≤i ≤k}合適。特別地，D 并非μ′中缺陷。

其中，

容易驗(yàn)證μ′是μ 的可數(shù)融貫擴(kuò)充并定義出相應(yīng)的輔助函數(shù)族特別地，并非μ′中缺陷。

命題8(完全性).一致公式集都是可滿足的。

證明.給定一致公式集Σ，將其擴(kuò)充為極大一致集Σ*，可以得到一個(gè)相對(duì)于Σ*個(gè)體擬完美網(wǎng)絡(luò)μ，再借助引理4 得到可數(shù)融貫網(wǎng)絡(luò)μ*以及相應(yīng)輔助函數(shù)族利用引理5 并參照命題3 的證明，我們最終得到一個(gè)完美網(wǎng)絡(luò)且Σ 在生成模型中可滿足。

推論3(緊致性).對(duì)于任意公式集是可滿足的當(dāng)且僅當(dāng)每個(gè)有窮子集都是可滿足的。

注意到完全性的證明過(guò)程中事實(shí)上為每個(gè)公式構(gòu)造了一個(gè)證據(jù)獨(dú)立的模型，因此一致公式均能在證據(jù)獨(dú)立的模型上滿足，從而可以在有窮模型上滿足。

推論4(有窮模型性).群體STIT 理論的能力片段具備有窮模型性質(zhì)。

4 結(jié)語(yǔ)

本文分別討論了個(gè)體STIT 理論與群體STIT 理論的能力片段，給出了與經(jīng)典STIT 模型等價(jià)的鄰域STIT 模型。我們?yōu)檫@兩個(gè)片段分別提供了希爾伯特式公理系統(tǒng)，并利用鄰域STIT 模型與逐步構(gòu)造法得到了公理系統(tǒng)的完全性。利用群體STIT 理論能力片段的完全性結(jié)果，我們證明了該片段具備有窮模型性質(zhì)。

本文利用個(gè)體STIT 理論的既有結(jié)果得到了個(gè)體STIT 理論能力片段的可判定性與復(fù)雜度上限，但個(gè)體STIT 理論能力片段的算法復(fù)雜度卻依然未明。另一方面，利用群體STIT 理論能力片段的有窮模型性質(zhì)將有望得到群體STIT理論能力片段的可判定性，這有待我們后面的研究。

本文在討論STIT 理論能力片段的時(shí)態(tài)擴(kuò)充時(shí)只簡(jiǎn)單提到了與明日算子X(jué)和昨日算子Y 的結(jié)合，對(duì)能力片段進(jìn)行時(shí)態(tài)擴(kuò)充將是我們的另一目標(biāo)。通過(guò)在語(yǔ)言中增添表示將來(lái)的將來(lái)算子F 與過(guò)去的過(guò)去算子P，我們甚至能討論個(gè)體與群體在過(guò)去、當(dāng)前與將來(lái)的能力。具體的討論也是我們今后的工作方向。