提要：活动类连续行动的特点是其通过重复履行最小的行动单元而构成。例如约翰跑步、丽丽游泳等行动都属于活动类连续行动。本文中我们将利用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