Page 122 - 《软件学报》2020年第12期

3788 Journal of Software 软件学报 Vol.31, No.12, December 2020

相关模型检测技术 [8−11] .我国学者吴立军、苏开乐、骆翔宇等在发展时态认知逻辑的模型检测方面也做出了一
些贡献 [12−14] .
完美回忆(perfect recall)是指主体记得自己先前的知识.TEL 中,用公理“K i Oϕ→OK i ϕ”对此进行刻画,它由文
献[2]给出,读作“如果主体 i 知道下一刻ϕ成立,那么下一刻 i 知道ϕ”,可以理解为主体能够完美回忆自己在前一
时刻关于当前时刻的认识.文献[2]同时强调,公式“K i ϕ→OK i ϕ”不是有效式,即主体当前时刻的知识不一定是他
在下一时刻的知识.这意味着命题的真值会随着时间的变化而变化.例如,某人在当前时刻不知道 p,根据负内省
公理可知:在当前时刻他知道自己不知道 p,但下一时刻他完全有可能知道 p,即下一时刻他知道自己不知道 p 可
能不再成立.
我们认为,理性主体可以记得自己先前的认知状态是一种认知规律.例如,某人在今天不知道 p 的真假(并且
他也不知道明天自己能否知道 p 的真假),但是明天他一定可以回忆起他在今天不知道 p.换句话说,即使主体当
前的认知状态中不含有关于下一刻会怎样的认识,到了下一刻主体仍旧可以回忆自己先前的认知状态.假定主
体具有完美回忆在社会实践中具有重要意义,如法官在判断某人是否犯有窝藏包庇罪时,需要当事人完美回忆
自己在过去的具体时间点上知道什么和不知道什么;再比如,重复博弈中需要假定参与者能够完美回忆博弈过
去的历史(如之前选择了诚实还是欺骗).公理“K i Oϕ→OK i ϕ”没有考虑主体先前所有的认知状态,因此无法对上
述认知规律进行逻辑刻画.
文献[2]否定公式“K i ϕ→OK i ϕ”是有效式意味着命题的真值会随着时间发生变化,其哲学基础是可疑的.按
照现代逻辑创始人 Frege 的观点,逻辑对于符号组合有从涵义进到意谓的要求 [15] .Frege 认为:句子的涵义是它的
思想,句子的意谓是它的真值.因为思想是没有时间性的,所以句子的真值不受时间影响,即命题的真值不会随
时间发生变化.Quine 则认为:时间是与空间等同的是非本质的东西,可以用“时间量词”,如“现在”、“在 t 之前”等
来取代句子中的时态动词,从而使得一个句子的真值得到固定 [16] .除此之外,原子命题的真值不随时间发生变
化,是逻辑中的一种常见假设,如动态认知逻辑(dynamic epistemic logic,简称为 DEL)中的模型更新和公开宣告
逻辑(public announcement logic,简称为 PAL)中的删减模型,在技术上都需要定义原子命题的真值在更新前后
(模型删减前后)保持不变.
其实,文献[1]已经给出了一种刻画完美回忆的方法,只是这种方法被人们忽视了.文献[1]曾给出公理系统
KT5,其基本形式语言包括原子命题集{p,q,...}、主体集{O,S 1 ,S 2 ,...}和对应正整数集的时间集{t 1 ,t 2 ,t 3 ,...},其中,主
体集中的“O”表示一个特殊个体“傻瓜”.合式公式递归定义为“ϕ::=p|⊥|ϕ⊃ϕ|[St]ϕ”,公式“[St]ϕ”结合了时态与认
知,读作“S 在 t 时刻知道ϕ”.显然,KT5 系统将时态与认知融合进同一个算子,并且其形式语言没有涉及群体知识.
内定理“[St]ϕ⊃[Su]ϕ,t≤u”直接表达完美回忆,读作“如果 S 在 t 时刻知道ϕ并且 t 早于 u,那么 S 在 u 时刻知道ϕ”.
不难发现 , 此内定理成立依赖于命题的真值永远不会发生变化 . 由上述内定理结合负内省公理
“¬[St]ϕ⊃[St]¬[St]ϕ”可以得到另外两条间接表述完美回忆的内定理:“[St]ϕ⊃[Su][St]ϕ,t≤u”,读作“如果 S 在 t 时
刻知道ϕ并且 t 早于 u,那么 S 在 u 时刻知道 S 在 t 时刻知道ϕ”;“¬[St]ϕ⊃[Su]¬[St]ϕ,t≤u”,读作“如果 S 在 t 时刻
不知道ϕ并且 t 早于 u,那么 S 在 u 时刻知道 S 在 t 时刻不知道ϕ”.后述两条内定理说明主体都可以完美回忆自己
在先前所有时刻的认知状态,即知道自己认知状态的变化过程.
既然个体知识可以被人们完美回忆,那么公共知识(common knowledge)能否被群体完美回忆?答案是肯定
的.文献[2]曾用公理“COϕ→OCϕ”表达群体关于公共知识的完美回忆,读作“如果下一刻ϕ成立是当前的公共知
识,那么下一刻时ϕ是公共知识”.这跟表述个体完美回忆存在相同的弊端,不能表达群体完美回忆先前的所有的
公共知识.文献[1]没有给出刻画完美回忆公共知识的公式,但在 KT5 系统中,傻瓜的知识一定是其他人的知识,
这是早期公共知识的雏形,因此可以看做是一点前期工作.文献[17]曾将被时间标记的傻瓜知识“[Ot]ϕ”修
T
改为被时间标记的公共知识“ C ϕ ”(在 T 时刻,ϕ是群体 G 的公共知识),但他们并未给出相关的形式系统,这是一
G
点遗憾.
本文的目标是在文献[1]的基础上构造一个可以刻画对公共知识进行完美回忆的新系统,然后证明新系统
的可靠性和完全性.由于目标系统的形式语言、公理、推理规则等与 S5C 系统 [18] 的非常相似,故将新系统取名