提要：活動類連續行動的特點是其通過重復履行最小的行動單元而構成。例如約翰跑步、麗麗游泳等行動都屬于活動類連續行動。本文中我們將利用STIT邏輯給出活動類連續行動的邏輯刻畫。在簡要說明活動類連續行動的特點以及STIT邏輯主要內容的基礎上，給出刻畫活動類連續行動的STIT邏輯并證明該系統的一些重要元定理。

連續行動（continuous actions）是一類具有時間上持續性（duration）的行動類型，即這類行動的履行是在時間段（time interval）而不是在時間點（point of time）上進行的。連續行動的邏輯刻畫方案眾多，但是這些方案大多將連續行動視為一類特殊的行動類型并進行統一刻畫。然而，由于連續行動還可被細分為具有不同特點的不同類別，所以統一刻畫方案的給出就會伴隨著（在一定程度上的）對不同類別連續行動的不同特點的舍棄。因此，為了保留甚至突出這些特點，我們放棄了給出統一刻畫方案這一路徑，轉而分析連續行動不同類別之間的不同特點，進而以活動類連續行動（continuous actions of activities）的邏輯刻畫為突破口來討論不同類別連續行動的精細刻畫問題。

一、活動類連續行動的特點和已有刻畫方案

我們來看下面的四個語句：

(1)約翰跑步。

(2)麗麗游泳。

(3)張三修理手機。

(4)李四建造一間房子。

上面這四個語句所分別描述的行動都是連續行動，即都發生在一個時間段上而不是像瞬時行動（instantaneous actions）那樣發生在某一個時間點上。雖然這四個語句所描述的連續行動都具有時間上的持續性，但并不完全相同。例如語句(1)和語句(2)所描述的行動實際上分別是由跑步或者游泳這種行動的不斷重復構成的，但是語句(3)和語句(4)所描述的行動則不涉及行動的重復履行問題。語句(3)和語句(4)所描述的行動是要達成某一個目的，但不一定要完成該目的。以語句(3)為例，行動者張三要達成的目的是修好手機，但是就算最后這一目的沒有達成，我們也可以說“張三修理手機”。之所以會存在這種差別是因為上面語句中描述行動的動詞分別屬于不同的體（aspect）。很多語言中的動詞都是具有時態特征的（例如英語）。從亞里士多德開始，很多哲學家就開始研究如何從動詞的時態特征出發，來描述該動詞所表述的行動的時間特征。這方面的理論被稱為動詞的體理論。文德勒（Z. Vendler）所提出的動詞體的四種類別是這一領域中極具代表性的理論之一。（cf. Vendler, pp.143-160）按照文德勒的分類，動詞體可被分為四類，分別是：狀態（states）類、活動（activities）類、完成（accomplishment）類和成就（achievement）類。其中狀態類專指那些描述行動者某種狀態的動詞，例如“擁有”“相信”等；活動類專指那些描述重復性行動的動詞，例如“跑步”“游泳”等；完成類專指那些描述不區分目的是否完成的行動的動詞，例如“畫一幅畫”“修手機”等；成就類專指那些描述完成結果的動詞，例如“找到”“發現”等。當然這種分類并不是一成不變的，特定修飾語的加入也會改變動詞體本應歸屬的類型。

我們將被活動類動詞所描述的連續行動稱為活動類連續行動，將被完成類動詞所描述的連續行動稱為完成類連續行動。由上文中的分析可知，這兩類連續行動所具有的特點是如此不同，以至于如果將這兩類連續行動進行統一刻畫就會在很大程度上丟失他們各自的特點，因此從不同類型連續行動的精細刻畫角度考慮，就需要分別給出不同類型連續行動的不同邏輯刻畫方案。本文將先以活動類連續行動為例來討論其特點以及刻畫方式等問題。筆者認為活動類連續行動具有如下的兩個特點：

（1）時間上的持續性

（2）行動上的重復性

活動類連續行動的履行是在某一個時間段而不是時間點上進行的。除此之外，這類連續行動本身還是由特定行動的重復履行構成的。例如跑步這一行動，雖然是由抬起左腳、放下左腳，然后抬起右腳、放下右腳等發生在特定時間點上的一系列瞬時行動構成的，但是當我們討論跑步這一行動的時候，實際上卻忽略了構成該行動的瞬時行動而將跑步（或者更嚴格地說是跑一步）作為一個基本的或者說最小的行動單元來看待。無論跑步這一行動重復一次還是重復無數次，我們都可以用動詞“跑步”來刻畫這類行動。由上述的兩個特點可知，如果要給出活動類連續行動的一個邏輯刻畫方案，那么這一方案既要能夠刻畫連續行動在時間上的持續性，還要能夠刻畫出行動的重復性。

已有的連續行動刻畫方案可分為兩類：第一類方案是從構成連續行動的瞬時行動出發來進行刻畫，第二類方案則是將連續行動視為一個不可分割的整體來進行刻畫。

在第一類方案中，時間點被選作評價連續行動是否為真的參數，然后再從這一時間點上所發生的瞬時行動出發來給出這一瞬時行動所（要）構成的連續行動的語義解釋。穆勒（T. Müller）(cf. Müller, pp.191-209)、保爾森（J. Broersen）(cf. Broersen, pp.47-59)以及保爾森和赫齊格（A. Herzig）(cf. Broersen and Herzig, pp.137-173)等人的方案都屬于這一類。以穆勒的方案為例，他討論了連續行動正在被履行時應該如何刻畫的問題，其所給出的方案是在某一連續行動正在被履行的某一個時間點（m）上，如果行動者有一個策略使其能夠保證該連續行動的結果為真且該連續行動的結果并不必然為真，那么這一連續行動在當下的時間點（m）上就是真的。在第二類方案中，時間段被選作評價連續行動是否為真的參數，連續行動被視為該時間段上的一個整體來刻畫。貝爾納普（N. Belnap）、佩羅夫（M. Perloff）和徐明（M. Xu）所提出的時間鏈（time chain）理論就屬于這類方案（cf. Belnap, Perloff and Xu, pp.35-40），即用一個包含多個時間點的時間鏈（時間段的另一種稱呼）來作為連續行動的評價參數，而不再涉及構成連續行動的瞬時行動。

第一種方案無法刻畫連續行動時間上的持續性，第二種方案雖然注意到了連續行動時間上的持續性問題，卻因為評價參數過多而顯得過于復雜。除此之外，這兩類方案都沒有討論到行動的重復履行問題。鑒于這些問題的存在，我們才需要構建新的刻畫方案。

我們可以從不同的評價時間出發來討論或者評價活動類連續行動，這種評價時間上的不同也會表現在動詞的時態形式上。例如，如果活動類連續行動已經發生，那么對其進行描述的動詞就會使用過去式時態。本文中，筆者僅將要刻畫的對象限制為那些用一般現在時的動詞所表述的活動類連續行動，正如上文中的語句(1)和(2)。

STIT邏輯是行動理論中的重要一支，上述兩種邏輯刻畫理論也大都通過對STIT邏輯的改進或者修正來刻畫連續行動，因此本文也將在STIT邏輯的基礎上給出自己的活動類連續行動刻畫方案。

二、STIT邏輯簡介

STIT邏輯是一種刻畫主事性（agency）的理論。所謂的主事性就是一種行動者（agent）與事件（event）之間的二元關系，即行動者通過某種行動導致某一結果或者事件為真的關系。正是因為具有主事性，行動才能夠從事件中被區分出來，所以STIT邏輯又被稱為一種行動理論。作為行動理論中的重要一支，STIT邏輯主要被用來刻畫瞬時行動。本小節中，筆者就將簡要介紹STIT邏輯對瞬時行動的刻畫。

STIT是英文“see to it that”的縮寫。“see to it that”可被譯為確保、確定。STIT邏輯通過將stit處理為一個連結行動者和事件的二元算子來刻畫主事性。如果令α表示任意的行動者，A表示任意的語句，那么［α stit: A］就表示行動者α確保事件A為真的行動。這類包含STIT算子的語句也被稱為stit語句。STIT邏輯通過這些stit語句來刻畫主事性以及行動者的行動或者選擇。

STIT邏輯的語言就是在命題邏輯語言的基礎上增加stit語句得到的。STIT邏輯中包含不同的STIT算子（如astit、dstit、cstit等），這些不同的STIT算子分別對應主事性的不同解釋。雖然不同算子的解釋不盡相同，但這些解釋卻都建立在分支時間邏輯（branching time logic）BT的基礎上。BT的框架是一個二元組〈Tree,R〉，其中集合Tree是一個由時間點構成的非空集，我們用m, m1, m2,……來表示集合Tree中任意的時間點；R是集合Tree上的一個二元關系，這一關系滿足向下不分叉性，即對于任意時間點m1,m2而言，都會存在一個時間點m使得mRm1且mRm2。在滿足向下不分叉性的同時，如果R是一偏序關系，那么R關系就可被表示為≤；如果R是一嚴格偏序關系，那么R關系就可被表示為<。對于集合Tree中的任意非空子集，如果其是Tree中的一個極大線性序，那么該子集就被稱為一支歷史（history）。我們可用h,h1,h2,……來表示不同的歷史。對于任意時間點m以及歷史h，如果h經過m，那么就可被表示為m/h，即時間點m屬于歷史h。如果一個時間點m屬于某一支或者多支歷史，那么這個或者這些歷史就構成了集合Hm，即Hm={h|m∈h}。

如果我們將BT框架中的R關系具體化為滿足向下不分叉性的嚴格偏序關系<，那么BT的模型M*就可被表示為一個三元組〈Tree，<,v〉，其中〈Tree，<〉是BT的框架，v是一個賦值函數，其將任意的原子公式映射到一個m/h參數集上。如果令M*為任意的BT模型，m/h為任意的時間點及其所經過的歷史構成的二元組，?和∧分別為命題聯結詞否定和合取，□、◇、P和F分別為通常意義上的模態算子和時態算子，那么對于任意的公式A，就可以給出如下的賦值規則：

(1)如果A是一個原子公式，那么M*,m/h╞A當且僅當m/h∈v(A)；

(2)M*,m/h╞ ?A，當且僅當并非M*,m/h╞A；

(3)M*,m/h╞A∧B，當且僅當M*,m/h╞A并且M*,m/h╞B；

(4)M*,m/h╞□A，當且僅當對于任意的歷史h*∈Hm,M*,m/h*╞A；

(5)M*,m/h╞◇A，當且僅當存在歷史h*∈Hm,使得M*,m/h*╞A；

(6)M*,m/h╞PA，當且僅當存在一個時間點m*使得m*<m且M*,m* h╞A；

(7)M*,m/h╞FA，當且僅當存在一個時間點m*使得m<m*且M*,m* h╞A。

STIT邏輯的框架BT+A+C是一個四元組〈Tree，<,Agents,Choice〉，其中〈Tree，<〉是BT的框架；Agents是由行動者構成的非空集合，我們可以用α,β,……等來表示集合Agents中任意的行動者；Choice是一個函數，其將任意的時間點m和任意的行動者α映射到Hm的一個劃分上去，因此這一函數也可被表示為Choice(α,m)。對于任意的歷史h∈Hm，我們用Choice(α,m)(h)表示歷史h所屬的Choice(α,m)中的唯一元素。除此之外，函數Choice(α,m)還要滿足未分叉無選擇性（no choice between undivided histories）和行動者的獨立性（independent of agents）。所謂的未分叉無選擇性是說對于任意的時間點m以及屬于集合Hm的歷史h0和h1，如果存在一個時間點m0使得m0＞m且m0∈h0∩h1，那么對于Choice(α,m)中任意的元素K，h0∈K當且僅當h1∈K；所謂的行動者的獨立性是指對于任意的時間點m以及任意的函數s（s將任意的行動者α映射到Choice(α,m)中的一個元素上去），∩α∈Agentss(α)≠?。如果將STIT邏輯的模型BT+A+C表示為M，那么M=〈Tree，<,Agents,Choice,v〉，其中〈Tree，<,Agents,Choice〉是一個BT+A+C框架，v為BT模型中的賦值函數。

對于任意的BT+A+C模型M，我們用表示集合{h:M,m/h╞A}。在不會引起歧義的情況下，可被簡寫為‖A‖m。

如果令M為任意的BT+A+C模型，m/h為任意的時間點及其所經過的歷史構成的二元組，那么對于任意的行動者α以及語句A，stit語句［α dstit:A］以及［α cstit:A］的賦值規則可被定義如下：

(1)M,m/h╞［α dstit:A］，當且僅當(i)Choice(α,m)(h)?‖A‖m，（ii)Hm不是‖A‖m的子集；

(2)M,m/h╞［α cstit:A］，當且僅當Choice(α,m)(h)?‖A‖m。

直觀來說，［α dstit:A］就表示結果事件A為真是行動者α的行動或者選擇來保證的且A并不是必然為真的；［α cstit:A］則只要求結果事件A為真是行動者α的行動或者選擇來保證的。

三、系統CAA-STIT的給出

如上文所述，本文希望給出的對活動類連續行動的刻畫應該具有如下兩個特點：時間上的持續性和行動上的重復性。這兩個特點分別對應著句法和語義解釋中的特定處理方式。

在句法方面，我們使用d-act來表示刻畫活動類連續行動的STIT算子。d-act算子仍然是一個連接行動者與事件的二元關系，但是與一般的stit語句不同，在這里我們要對算子d-act所連接的語句A施加一定的限制，即語句A所描述的只能是那些可以作為某一活動類連續行動的最小行動單元的活動類連續行動。因此，我們就可以將活動類連續行動所導致的（事件）結果刻畫為語句A所描述的活動類連續行動的n次重復履行，并將這種行動的重復履行表示為：An（n≥1）。如果令α為任意行動者，A為任意的（施加了上述限制條件的）語句，n為任意大于或者等于1的自然數，那么任意的活動類連續行動就可被表示為［α d-act:An］（n≥1），即行動者α確保語句A所描述的（可以作為最小行動單元的）活動類連續行動的n次重復履行為真。

我們將刻畫活動類連續行動的STIT邏輯稱為CAA-STIT。貝爾納普、佩羅夫和徐明曾給出過一個多主體的dstit系統Ldm。（cf.Belnap, Perloff and Xu）系統CAA-STIT的語言LCAA是在多主體的DSTIT理論Ldm的基礎上僅進行如下修改得到的：

(1)語言LCAA是一個單主體的語言，因此語言LCAA中僅包含一個行動者項α；

(2)語言LCAA中僅包含的STIT算子是d-act，而不是Ldm的語言中僅包含的算子dstit；

(3)語言LCAA中，令H,I,J,……表示任意的語句，令A,B,C,……表示那些表述需要被重復履行的作為最小單元的活動類連續行動的語句；

(4)語言LCAA中，對于任意大于或者等于1的自然數n，An,Bn,Cn,……是合適公式；

(5)語言LCAA中，我們增加一個時間段切割算子C。直觀上來說，對于任意的語句H，CH就表示在將某一時間段切割為其中所包含的時間點之后，存在某一時間點使得語句H為真。

如上所述，對于任意的活動類連續行動，我們可以將其表示為：［α d-act:An］（n≥1）。直觀來說，活動類連續行動［α d-act:An］（n≥1）為真，當且僅當(1)在某一時間段上，行動者α通過自己的行動或者選擇保證A的n次重復履行為真；且(2)（由于主觀或者客觀的原因）在該時間段中的某一個時間點上，行動者α終止對A的履行是可能的。

因此，在語義上，我們首先要刻畫活動類連續行動在時間上的持續性。為了刻畫這種時間上的持續性，就需要使用時間段而不是時間點來作為我們的語義解釋參數。對于任意的兩個時間點m和m*而言，［m,m*］表示一個時間段，當且僅當m<m*，即時間點m和m*之間具有嚴格的偏序關系。由此可見，本文中我們將時間段限制為嚴格的時間段，也正是在這種嚴格的時間段上，我們才會說活動類連續行動具有時間上的持續性。

其次，活動類連續行動具有行動上的重復性，即活動類連續行動都具有最小的行動單元，這些最小行動單元的不斷重復就構成了該活動類連續行動。例如，對于約翰跑步這一活動類連續行動而言，如果其最小的行動單元是“跑一步”這一行動，那么這一最小行動單元的不斷重復就構成了約翰跑步這一行動。這里需要注意的是，由于最小行動單元的不斷重復也包括重復一次這種特殊情況，所以我們需要要求這些最小行動單元也都是活動類連續行動，即僅履行了一次的活動類連續行動。

然而，由此卻會出現一個問題，那就是活動類連續行動的最小行動單元為瞬時行動時應該如何處理。例如對于約翰坐地鐵、約翰乘公交等行動而言，其本應是活動類連續行動，但其最小行動單元卻是瞬時行動，即如果行動者在地鐵或者公交車上待一下，那么這一行動就應該為真。按照上述我們給出的刻畫標準，這類行動的最小行動單元顯然不滿足時間上的持續性。因此，如果其最小行動單元只被履行了一次，那么約翰坐地鐵或者約翰乘公交這種行動就會是瞬時行動。

對于這類最小行動單元為瞬時行動的行動，如果其只是由最小行動單元的一次履行而構成，那么就應將其處理為瞬時行動；如果其是由最小行動單元的多于一次的履行構成的，那么就應將其處理為活動類連續行動。由于在我們對活動類連續行動的刻畫中要求任意活動類連續行動的最小行動單元也都要是活動類連續行動，所以這里特別規定，在將約翰坐地鐵或者約翰乘公交車這類（最小行動單元為瞬時行動的）行動處理為活動類連續行動的情況下，我們將任意嚴格時間段上的該行動的重復履行視為我們所需要的最小行動單元。例如對于約翰坐地鐵這一行動而言，約翰坐5分鐘的地鐵或者10分鐘的地鐵都可被視為活動類連續行動的最小行動單元，即所有的這種活動類連續行動實際上都可被刻畫為最小行動單元的一次履行。

CAA-STIT這一邏輯的語義解釋可被定義如下：

定義1  一個三元組〈Tree，<,I+ (Tree)〉是能夠刻畫時間段的分支時間邏輯的框架Fint，當且僅當下面的條件被滿足：

(1)〈Tree，<〉是BT的框架；

(2)I+ (Tree)是集合Tree中所有的嚴格時間段構成的集合，即I+ (Tree)={［m,m*］|m ∈Tree∧m*∈Tree∧m<m*}。 

對于任意的嚴格時間段［m,m*］以及任意的歷史h，如果［m,m*］?h，那么包含［m,m*］的歷史就可被表示為：h［m,m*］。H［m,m*］=df{h:［m,m*］?h}。

定義2  一個四元組〈Tree，<,I+ (Tree),v*〉是能夠刻畫時間段的分支時間邏輯的模型Mint，當且僅當下面的條件被滿足：

(1)〈Tree，<,I+ (Tree)〉是能夠刻畫時間段的分支時間邏輯的框架Fint；

(2)v*是一個賦值函數，其將任意的原子公式映射到一個由嚴格時間段［m,m*］和歷史h構成的參數集上且［m,m*］?h。

定義3  對于任意的模型Mint、任意的參數［m,m*］/h且［m,m*］?h以及任意的公式H，其賦值規則可被定義如下：

(1)如果H是一個原子公式，那么Mint,［m,m*］/h╞*H當且僅當［m,m*］/h∈v*(H)；

(2)Mint,［m,m*］/h╞*?H當且僅當并非Mint,［m,m*］/h╞*H；

(3)Mint,［m,m*］/h╞*H∧I當且僅當Mint,［m,m*］/h╞*H且Mint,［m,m*］/h╞*I；

(4)Mint,［m,m*］/h╞*□H當且僅當對于任意的歷史h*∈H［m,m*］，Mint,［m,m*］/h*╞*H；

(5)Mint,［m,m*］/h╞*◇H當且僅當存在歷史h*∈H［m,m*］使得Mint,［m,m*］/h*╞*H；

(6)Mint,［m,m*］/h╞*PH，當且僅當存在一個嚴格時間段［m0,m1］使得［m0,m1］<［m,m*］且Mint,［m0,m1］/h╞*H；

(7)Mint,［m,m*］/h╞*FH，當且僅當存在一個嚴格時間段［m0,m1］使得［m,m*］<［m0,m1］且Mint,［m0,m1］/h╞*H；

(8)Mint,［m,m*］/h╞*CH，當且僅當存在時間點m1，m<m1≤m*使得Mint,m1/h╞h。

定義3中，符號“╞*”表示的是以時間段為參數的語義解釋，符號“╞”表示的是以時間點為參數的語義解釋。算子C的作用就是將語義解釋的參數從時間段轉變到時間點上來。這里我們特別規定，條件(8)中的公式H不包含STIT算子疊置的情況。

定義4  一個五元組〈Tree，<,I+ (Tree),Agent,Ch〉是CAA-STIT的框架FCS當且僅當下面的條件被滿足：

(1)〈Tree，<,I+ (Tree)〉是能夠刻畫時間段的分支時間邏輯的框架Fint;

(2)Agent是行動者構成的集合，本文中Agent={α};

(3)Ch是一個函數，其將任意的嚴格時間段［m,m*］和任意的行動者α映射到H［m,m*］的一個劃分上去，因此這一函數也可被表示為Ch(α,［m,m*］)。

對于任意的歷史h∈H［m,m*］，我們用Ch(α,［m,m*］)(h)表示歷史h所屬的Ch(α,［m,m*］)中的唯一元素。除此之外，函數Ch(α,［m,m*］)還要滿足未分叉無選擇性。所謂的未分叉無選擇性是說對于任意的嚴格時間段［m,m*］以及屬于集合H［m,m*］的任意歷史h0和h1，如果存在一個時間點m0使得m0＞［m,m*］且m0∈h0∩h1，那么對于Ch(α,［m,m*］)中任意的元素K，h0∈K當且僅當h1∈K。

定義5  一個七元組〈Tree,<,I+(Tree),Agent,Ch,v*,v〉是CAA-STIT的模型MCS當且僅當下面的條件被滿足：

(1)〈Tree,<,I+(Tree),Agent,Ch〉是CAA-STIT的框架FCS；

(2)〈Tree,<,I+(Tree),v*〉是能夠刻畫時間段的分支時間邏輯的模型Mint。

(3)〈Tree,<,v〉是BT模型M*。

對于任意的CAA-STIT的模型MCS，我們用表示集合{h:MCS,［m,m*］/h╞H}。在不會引起歧義的情況下，可被簡寫為‖H‖［m,m*］。

定義6  對于任意的模型MCS以及任意的參數［m,m*］/h且［m,m*］?h，任意的活動類連續行動［α d-act:An］（n≥1）可被定義如下：

MCS,［m,m*］/h╞*［α d-act:An］，當且僅當(1)Ch(α,［m,m*］)(h)?‖An‖［m,m*］，（2)存在歷史h*以及時間點m1，m<m1≤m*使得Mcs,［m,m1］/ h*╞*C?A。

也就是說，A的重復履行是由行動者α的行動或者選擇所保證的，而且對A的履行不是必然為真的，即A在某一時間點上為假這是可能的。

仿照dstit算子和cstit算子之間的關系，筆者在這里特別給出另一刻畫活動類連續行動的算子c-act的定義，即對于任意的行動者α、任意的命題A以及任意大于或者等于1的自然數n，［α c-act:An］=df［α d-act:An］∨□An。

在此基礎上，系統CAA-STIT的公理和推導規則可被給出如下：

公理：

A1□(H→I)→(□H→□I)

A2□H→H

A3◇H→□◇H

A4［α c-act:(An→Bn)］→(［α c-act:An］→［α c-act:Bn］)（n≥1）

A5［α c-act:An］→An（n≥1）

A6?［α c-act:An］→［α c-act:?［α c-act:An］］（n≥1）

A7C?A??An（n≥1）

A8［α d-act:An］→C?□A（n≥1）

A9［α d-act:An］→?C?A（n≥1）

推導規則：

MP（分離規則）：由H和H→I可得I

RN（必然化規則）：由H可得□H

系統中的公理A1至A3討論了必然算子□和可能算子◇之間的推導關系，公理A4到A6使用c-act算子刻畫了活動類連續行動的特點，公理A7討論了切割算子C的性質問題，公理A8到A9使用d-act算子刻畫了活動類連續行動與切割算子C之間的推導關系。

在CAA-STIT系統中，我們可以推出如下這些內定理：

T1◇H?□◇H

T2［α d-act:An］→［α c-act:An］

T3［α d-act:An］∧［(d-act:Bn］→［α d-act:(An∧Bn)］

T4［α d-act:(An∧Bn)］→［α d-act:Bn］∨□Bn

T5C?A→?［α d-act:An］（n≥1）

T6［α c-act:An］∧?［α d-act:An］→□An

T7□An∧C?A→［α c-act:An］∧?［α d-act:An］

T8［α c-act:An］∧?□An→［α d-act:An］

T9［α d-act:An］→［α c-act:An］∧?C?A

通過這些內定理，我們可以發現d-act和c-act這兩個算子之間的一些關聯性和差異性（如T2、T3）、必然算子或者切割算子與STIT算子之間的聯系（如T4-T9）。這些都能夠幫助我們更精確且全面地理解活動類連續行動。

在STIT邏輯中，像［α dstit:A］這樣的stit語句表示的是做某事（doing something）,拒絕做某事（refraining from doing something）可被表示為：［α dstit:?［α dstit:A］］，拒絕拒絕做某事（refraining from refraining from doing something）可被表示為：［α dstit:?［α dstit:?［α dstit:A］］］。因此拒絕拒絕做某事與做某事之間是什么關系，是否具有雙重否定等于肯定這樣的等價關系就是STIT邏輯中一個值得研究的問題。在系統Ldm中，可得內定理［α dstit:A］?［α dstit:?［α dstit:?［α dstit:A］］］。然而，在我們所構建的系統CAA-STIT中，由于算子d-act語義解釋中否定條件（定義6中的條件(2)）的特殊性使得等式［α d-act:An］?［α d-act:?［α d-act:?［α d-act:An］］］并不成立，甚至這一等式中的任何一個蘊涵方向（從左到右的蘊涵以及從右到左的蘊涵）也都是不成立的。因此，這就導致系統CAA-STIT無法刻畫做某事與拒絕拒絕做某事之間的關系問題。

四、元定理的證明

定義7  對于CAA-STIT的任意模型MCS，時間段[m,m*]以及真包含該時間段的歷史h，如果對于任意的語句A而言，語句A在模型MCS上相對于[m,m*]/h為真，那么就稱語句A在模型MCS上相對于[m,m*]/h是可滿足的，可表示為MCS,[m,m*]/h╞*A；如果A在模型MCS上的任何參數下都是可滿足的，那么就稱A在模型MCS上是可滿足的，可表示為MCS╞*A。對于CAA-STIT的任意框架FCS，如果A在所有在FCS基礎上構建的模型MCS上都可滿足，那么就稱A在框架FCS上是有效的，可表示為FCS╞*A。

定理1（可靠性）對于系統CAA-STIT中可推出的任意公式A，都可得FCS╞*A。

證明：首先要證明系統CAA-STIT中的任意公理都是有效的，然后證明系統中的推導規則保持這種有效性即可。

我們以公理A8的有效性證明為例。

［α d-act:An］→C?□A（n≥1）是有效的，當且僅當對于FCS上的任意模型MCS，MCS中的任意時間段［m,m*］以及任意包含該時間段的歷史h，MCS,［m,m*］/h╞*［α d-act:An］→C?□A（n≥1）。因此如果能證明若MCS,［m,m*］/h╞*［α d-act:An］（n≥1），則MCS,［m,m*］/h╞*C?□A，那么結論成立。假定MCS,［m,m*］/h╞*［α d-act:An］（n≥1），則根據定義6可得，（1)Ch(α,［m,m*］)(h)?‖An‖［m,m*］，（2)存在歷史h*以及時間點m1，m<m1<m*使得MCS,［m,m1］/h*╞*C?A。由(2)和定義3中的(8)可得，MCS,［m,m*］/h╞*C?□A。因此，公理A8是有效的。□

下面我們將使用典范模型的方法，證明系統CAA-STIT的強完全性（strong completeness）和緊致性（compactness）。令V為CAA-STIT中所有一致的公式集所構成的集合，V中的元素可被標示為：v,v1,v2,……。W為CAA-STIT中所有極大一致的公式集構成的集合，W中的元素可被表示為：w,w1,w2,……。S是W與V之間的二元關系，對于W中任意的元素w以及V中任意的元素v，Swv成立，當且僅當{H:CH∈w}?v。R是W中元素上的二元關系且對于W中的任意元素w,w1,Rww1成立，當且僅當{H:□H∈w}?w1。由公理A1-A3以及規則RN可得，R是一個等價關系。令X,X′,……為相對于R關系的任意等價類。對于任意的行動者項α，X上的二元關系Rα成立，當且僅當對于X中任意的元素w和w1，{An:[αc-act:An]∈w}?w1?？芍?，Rα也是一個等價關系。令Eα表示所有Rα等價的集合所構成的集合，Eα中的元素可表示為：e,e1,e2,……。相對于X而言，系統CAA-STIT的典范框架可被表示為：〈X,Rα〉。

引理1  對于任意的二元組〈X,Rα〉，如果其是相對于X而言的，系統CAA-STIT的典范框架，那么這一二元組要滿足下面的性質：

(1)對于X中的任意元素w以及任意的公式H，{□H}∈w當且僅當對于X中任意w1，{H}∈w1當且僅當對于X中任意的元素w1，{□H}∈w1。

(2)對于X中的任意元素w，任意的行動者α以及任意的表示活動類連續行動n次復合的語句An，{[α c-act:An]}∈w當且僅當對于X中任意使得Rαw1w成立的w1有{An}∈w1當且僅當對于X中任意使得Rαw1w成立的w1有{[α c-act:An]}∈w1。

(3)對于X中的任意元素w，任意的行動者α以及任意的表示活動類連續行動n次復合的語句An，{[α d-act:An]}∈w當且僅當對于X中任意使得Rαw1w成立的w1而言，{An}∈w1且存在X中的元素w2以及V中的元素v，使得Sw2v成立且{?A}?v。

證明：由極大一致集的定義以及上文中所給出的R關系和Rα關系的定義可得(1)(2)。由(1)(2)以及T6和A7可得(3)。□

定理2（強完全性）任一CAA-STIT一致的公式集θ在框架FCS上都是有效的。

證明：令θ為任意的CAA-STIT一致的公式集。那么就會存在W中的一個元素w使得{θ}?w。假定X是w所屬于的那個R關系上的等價類，且令〈X,Rα〉為CAA-STIT相對于X的典范框架。那么我們需要做的就是將〈X,Rα〉轉變成框架G(=〈Tree,<,I+ (Tree),Agent,Ch〉)。我們首先令

Tree={V}∪V

<={〈W,w〉:w∈W}∪{〈W,W〉}∪{〈w,w〉:w∈W}

I+ (Tree)={W}∪W

Agents={α}

對于I+ (Tree)中的任意元素w，令hw={X,w}。很明顯，hw是結構〈Tree,<,I+(Tree)〉中包含w的唯一的歷史。并且對于I+(Tree)中任意的w以及〈Tree,<,I+(Tree)〉上的hw而言，存在其間的一一對應。

最后，令Ch(α,X)={H:存在e使得e∈Eα并且{hw:w∈e}}

Ch(α,w)={{hw}}，對于任意的w∈X。

很顯然，Ch([α],X)是HX的一個劃分（partition），因此未分支的歷史沒有選擇（no choice between undivided histories）這一點被滿足。

定義模型M=〈G,J〉使得(1)對于任意行動者項α，J(α)=α，并且(2)對于任意的命題變項p以及G中的任意歷史hw，〈X,hw〉∈J(p)，當且僅當存在w(w∈X并且h=hw)，并且(3)對于任意的行動者項α以及任意的w,w*∈X,hw≡xαhw*當且僅當存在e∈Eα[w,w*∈e]當且僅當wRαw*。由此遞歸可得對于任意的公式A，M,X/hw╞A當且僅當對于任意的w∈X，A∈w(由引理1可得)。□

定理3（緊致性）對于任意的語句集θ，如果θ的每一個有窮子集都有一個MCS模型，那么θ也有一個MCS模型。

證明：由定理2可得。□

五、結語

本文給出了一個刻畫活動類連續行動的STIT邏輯CAA-STIT。由該系統的句法和語義可知，這一系統能夠對活動類連續行動這一特殊的連續行動進行更為細致的刻畫，即準確地體現出該類行動時間上的持續性和行動上的重復性。然而，為了這種精細刻畫我們也丟失掉了一些邏輯上的特點，例如做某事與拒絕拒絕做某事之間的聯系完全無法在系統中得到刻畫。因此，如何平衡精細化方案與保留邏輯表達力的問題就是一個值得我們在研究中注意的問題。

另外，由于CAA-STIT目前所能刻畫的只有活動類連續行動，所以這就會使得系統CAA-STIT稍顯特設性。因此，在未來的工作中，我們的首要任務就是對另一類連續行動，即完成類連續行動進行深入的研究和刻畫，并在對這兩類活動類連續行動都有細致的了解和刻畫之后，再探索能夠同時刻畫活動類連續行動和完成類連續行動的邏輯方案。

【參考文獻】

[1]Belnap, N., Perloff, M. and Xu, M., 2001, Facing the Future: Agents and Choices in Our Indeterminist World, New York: Oxford University Press.

[2]Broersen, J. ,2009, “A Complete STIT Logic for Knowledge and Action, and Some of Its Applications”， in M.Baldoni, et al. (eds.)， DALT 2008, LNAI 5397, Berlin, Heidelderg: Springer-Verlag.

[3]Broersen, J. and Herzig, A.,2015,“Using STIT Theory to Talk about Strategies”， in van J.Benthem, et al. (eds.)， Models of Strategic Reasoning: Logics, Games, and Communities, Berlin, Heidelderg: Springer-Verlag.

[4]Müller, T.,2005,“On the Formal Structure of Continuous Action”， in R.Schmidt, et al. (eds.)， Advances in Modal Logic， Vol.5, London: King's College Publications.

[5]Vendler, Z.,1957, “Verds and Times”， in The Philosophical Review 66(2).

原載：《哲學研究》2022年第6期

來源：“哲學研究”微信公眾號2022.8.12