混合公开宣告逻辑

何键枫 王轶

1 引言

认知逻辑（[7,10,11]）及其简单动态扩充——公开宣告逻辑（[6,12]）在过去数十年间得到了广泛关注。上述框架可以模拟主体在公开宣告前后知识或信念的变化。现实生活中的人们在制定计划、计算得失并作出决定之前，往往会考虑尽量多的情形，将其中不可能的情形加以排除则是常见的获取知识或信念的做法。基于认知逻辑考察知识、信念与宣告时，也不可避免地运用到可能情形（在不同场合中也常被称为状态、可能性或可能世界等）这一概念。本文尝试在公开宣告逻辑的框架下突出对可能情形的刻画，允许在语言中直接诉说可能情形，由此得到一种混合逻辑（[1,3,5,13]）。

混合公开宣告逻辑并不是公开宣告逻辑和混合逻辑的简单结合，这方面的研究也不是堆砌式的技术工作。公开宣告逻辑的语义通过删除可能情形来实现对知识更新的模拟，而这在语言中包含了用于表示可能情形的常元（在混合逻辑中称为专名）之后就出现了问题。例如在公开宣告逻辑中，公式[φ]i（“公式φ被公开宣告之后，i是现实情形”）中的算子[φ]（“φ被公开宣告”）被解释为在模型中删除一切非φ的可能情形，其中或许已包括情形i，这将导致专名i在更新后的模型中失去定义。通过允许专名指称空集，[9]在技术上回避了上述问题。然而这样的处理方法允许专名没有指称，并不合理，至少会令“专名”这一称呼不再贴切。更有甚者，采用[9]中的定义将允许公式@i(φ ∨¬φ)（“在情形i中，φ或者非φ”）为假。

本文坚持按照经典混合逻辑的做法将每个专名都解释为单一的可能情形，并采用[8,第5.2.1 节]中提出的“删链”语义学，将[φ]解释为删除全部指向非φ情形的链接（但不在模型中删除那些情形）。这样既实现对不可能情形的排除，又保证了专名都有指称。然而缺点是，由链接所表示的二元关系将不必具有自反性与持续性。因此这一做法对知识模型S5 和信念模型KD45 并不适用。本文采用信念逻辑K45，并在此基础上探讨公开宣告逻辑的混合化。

混合公开宣告逻辑可以表达直接公开宣告之外的行动。有时需要表达在某一情形下作出了宣告（但在其他情形中可能并未作出），本文称之为间接公开宣告。公式[φ]xψ读作“当φ在情形x中被宣告后，ψ（在现实情形中）为真”。这样的语言在技术上也有优势，具体见第5.2–5.3 节。

文章结构如下：第2 节介绍基于信念模型的混合逻辑。第3 节对本文将探讨的逻辑进行梳理。第4 节中考察允许进行假宣告的混合公开宣告逻辑，而在第5节中则仅允许真宣告。第5.1–5.3 节探讨语言中带算子↓的扩充，在第5.4 节则转向不带该算子的逻辑。第6 节将对全文进行总结。

2 背景：基于信念模型的混合逻辑

信念模型是满足如下条件的三元组(W,R,V)：（1）W为非空的可能情形集；（2）R为每个主体赋予W上的一个具有传递性和欧性的二元关系；（3）赋值函数V为每个命题赋予一集可能情形。如此定义的信念模型也称为K45模型，它不一定满足持续性（要求满足持续性的信念模型通常称为KD45 模型）。

混合逻辑通过在模态语言中增加专名（用于表达可能情形的常元）以及其他混合算子（如@和↓等）扩充而成。其中只添加专名的混合语言以H表示。在H的基础上继续添加的其他算子在括号内标注，例如H(@)、H(↓)和H(@,↓)等都是混合语言。本文只关注H(@)和H(@,↓)这两个常用混合语言：前者在标准语义下能得到一个理想的、可判定的混合逻辑；后者得到的逻辑虽然不可判定，却拥有接近一阶逻辑的表达能力。

本文预设一个非空的有穷主体集Ag，以及可数无穷的命题变元集Pr、专名集Nom 和变名集Var。语言H(@)和H(@,↓)由以下语法给出（其中p ∈Pr，a ∈Ag，i ∈Nom 且s ∈Var）：

专名i和变名s都是公式，分别为指称可能情形的常元和变元。@iφ和@sφ分别表示在i和s所指称的情形中φ成立，而↓sφ表示将现实情形命名为s时φ成立。Baφ表示主体a相信φ。Ba的对偶算子记为，即代表¬Ba¬φ。命题联结词→、∨和↔等采用通常方式定义。

混合的信念模型（简称为模型）通过修改信念模型得到，使得每个专名都指称模型里的一个可能情形。准确地说，在模型(W,R,V)中，赋值函数V的定义域为Pr∪Nom，值域为℘(W)∪W，满足将命题变元都映射为一集可能情形（W的某个子集），并且将专名都映射为一个可能情形（W的某个元素）。结合指派g:Var→W以及现实情形w ∈W，可以得到所谓的点模型，并根据以下递归定义计算任意公式的真值（其中除=w外与g相同；其他经典信念逻辑公式如常定义，可参考[6]）：

有效式与逻辑后承等概念类似于经典模态逻辑加以定义。当语言中不含算子↓时则无需考虑指派g。

语言H(@)和H(@,↓)采用上述语义解释得到的逻辑分别记为H@和H@↓。图1 中给出了逻辑H@和H@↓可靠且强完全的公理系统K45@和K45@↓。两个系统的可靠性和完全性证明不妨参考[1]。

3 概览

在公开宣告逻辑中，宣告公式φ（被宣告的公式必须在现实情形中为真）意味着排除所有φ不为真的可能情形。尽管宣告可以反复进行，宣告的内容也可以不断变化，仅仅通过宣告却依然无法保证在最后消除所有不确定性以找出真实情形，更不用说找出宣告是在哪个情形中作出的。1信念模型中的可能情形对所有公式的真假都可断言，任意公式在其中或为真、或为假，而日常语言中的情形则常常代表了一类“可能情形”。“情形”一词在两者之间有所出入。使用足以刻画可能情形的语言是本文在公开宣告逻辑中引入专名的一个主要动机。

图1:公理系统K45@与K45@↓

引言中已经解释过，在混合语言下解释公开宣告时，排除不可能情形可以像[9]那样处理为将不可能情形直接删除，但这会引发较多问题。本文采用公开宣告的“删链”语义学（[8]），将其适当修改后用于混合公开宣告逻辑。这种处理方式不会导致可能情形被删除后专名失去指称，而且还使得对宣告假公式的解释成为可能。文章将探讨如下的两种语义设定：（1）作出的宣告可真也可假（宣告可假），（2）作出的宣告必须为真（宣告须真）。

本文将混合语言H(@)和H(@,↓)扩充以直接宣告算子和（或）间接宣告算子。直接宣告算子即经典公开宣告逻辑中的宣告算子；间接宣告算子以[φ]x（x为专名或变名）表示，读作“当φ在x所指称的情形下被公开宣告后，ψ在现实情形中为真”。简言之，间接宣告允许在某个可能情形中进行，而不像直接宣告那样仅限于在现实情形中进行。由此带来了三个混合宣告语言，H([],@)、H([],@,↓)和H([]x,@,↓)（本文不考虑语言H([]x,@)以免陷入太多组合）；考虑到行文的简洁，分别将它们简记为L1、L2和L3。这三个语言和上一段提到的两种语义设定将带来五个逻辑（本文不考虑语言L3配以宣告可假的语义，L3将主要用于辅助其他逻辑所涉及的证明，参见第5.2–5.3 节）。

文章将对比五个逻辑和两个基本混合语言的表达能力，并给出五个逻辑的可靠且完全的公理系统，为方便查找，将相关语言、语义设定以及对应的逻辑及其公理系统整理汇总至表1。

接下来第4 节首先探讨宣告可假的两个逻辑L1u 和L2u，然后到第5 节再采用宣告须真的语义设定。

表1:逻辑与公理系统的记法

4 宣告可假的逻辑

本节将会探讨在宣告可以为假的语义设定下的两个混合公开宣告逻辑L1u 和L2u，并给出它们的公理系统L1u 和L2u。这两个系统通过归约方法分别由第2节中介绍的混合信念逻辑的公理系统K45@和K45@↓得到。

4.1 逻辑L1u

在混合语言H(@)中增加经典公开宣告算子，由此得到的语言H([],@)简记为L1。

定义1(语言L1).L1公式由以下规则递归定义：

其中a ∈Ag，p ∈Pr 且i ∈Nom。命题联结词如常定义，与⟨φ⟩分别为Ba与[φ]的对偶算子。

宣告可假意味着公式φ被宣告无需先决条件，具体语义定义如下。

定义2(L1u 语义).任给模型M=(W,R,V)和可能情形w ∈W，原子公式、布尔公式和认知公式的语义解释如常定义（不妨参见[6]），混合公式的语义解释参见第2 节。形如[φ]ψ的公式的语义解释如下：

其中更新模型Mφ=(W,RM,φ,V)满足任给主体a，

即Mφ是将M中所有指向φ为假的情形的链接删除后得到的模型。

需要注意的是，即使M是持续模型，更新模型Mφ也可能不再具有持续性。这是本文不要求模型具有持续性的技术性原因。不难验证Mφ依然满足传递性和欧性。以欧性为例。如果成立而不成立，则有M,tφ。此时可得不成立，矛盾。上述更新方式保持传递性和欧性，因此适用于基于信念模型K45 的混合模型。

由所有有效公式（即在所有模型的所有可能情形下都为真的公式）组成的集合视为语言L1在上述语义下的逻辑，记为L1u。下面给出L1u 的一些有效式，证明较为简单，故略去。以这些有效式作为归约原则，可以将所有L1公式转化为与之等值的不含宣告算子的公式（即转化为等值的H(@)公式）。

命题3.任给L1公式φ、ψ和χ，命题变元p，主体a和专名i，如下公式都是L1u的有效式：

将上述命题中的有效式作为归约公理添加到逻辑H@ 的公理系统K45@ 中就可以得到L1u 的公理系统L1u，如图2 所示。

图2:公理系统L1u

定理4(L1u 可靠性).L1u 是可靠的，即如果⊢L1uφ则有|=L1uφ。

由K45@的可靠性和命题3 不难得到上述可靠性定理。反过来，要证明L1u的完全性，需要证明公式集Φ 的所有语义后承φ都可在L1u 中以Φ 为前提推演得到。任给L1公式φ，存在H(@)公式φ′满足⊢L1uφ ↔φ′。由L1u 的可靠性得知，φ′同样是Φ 的语义后承。由K45@的完全性可知Φ⊢K45@φ′。由于L1u 是K45@的扩充，Φ⊢L1uφ′，再通过分离规则即可推演出φ。因此，L1u 完全性证明的核心任务是找到L1公式的H(@)翻译，而这恰恰是归约公理的用途。

定义5(L1到H(@)的翻译).递归定义t:L1→H(@)如下：

为了证明⊢L1uφ ↔t(φ)，定义复杂度函数c:L1→N 如下：

引理6.任给L1公式φ、ψ和χ，命题变元p，主体a和专名i，

引理7.任给L1公式φ，都有⊢L1uφ ↔t(φ)。

定理8(L1u 完全性). 对任意L1公式集Φ 和公式φ，如果。证明.假设。以t(Φ)表示{t(ψ)|ψ ∈Φ}，则；因为否则存在Φ 的有穷子集Ψ 满足，此时根据引理7 可得，矛盾。由K45@ 的完全性可得。故有模型M及其中的可能情形w使得对于任意t(ψ)∈t(Φ)均有M,且。由于定义5中翻译t是保真的（根据引理7 以及L1u 的可靠性），对于任意公式ψ ∈Φ 均有M,，即。

4.2 逻辑L2u

在混合语言H(@,↓)中添加经典宣告算子，所得语言H([],@)简记为L2。

定义9(语言L2).L2公式由以下规则递归定义：

其中a ∈Ag，p ∈Pr，i ∈Nom 且s ∈Var。相关约定与定义1 中相似。

L2在宣告可假的语义设定下所得逻辑记为L2u。

定义10(L2u 语义).任给模型M=(W,R,V)、指派g和可能情形w ∈W，原子公式、布尔公式和认知公式的语义解释如常定义，混合公式的语义解释与前文相同。形如[φ]ψ的公式的语义解释如下：

其中更新模型Mg,φ=(W,RM,g,φ,V)使得对任意主体a，

语言L2中含有变名，对其处理类似于一阶逻辑中的变元，而↓算子则类似于量词，由此可以定义公式中变名的自由出现。将公式φ中的所有自由变名的集合记为Free(φ)。

下面的命题说明了公式[φ]↓sψ ↔↓s[φ]ψ（其中s/∈Free(φ)）是关于宣告和↓算子的有效归约原则。

命题11.任给L2公式φ和ψ，以及变名s/∈Free(φ)，公式[φ]↓sψ ↔↓s[φ]ψ是有效的。

证明.任给模型M、指派g和可能情形w使得。由语义定义可得。假设，则，因此。由于，不难验证故，矛盾。相反方向可类似证得。

由此可以得到图3 所示的公理系统L2u。可以采用与证明L1u 完全性类似的

图3:公理系统L2u

方法将L2u 归约为K45@↓，从而得到系统的完全性。在使用公理“公开宣告与↓”进行归约时需要考虑边际条件。如果变名s在公式φ中自由出现，则可能需要首先将约束变名s易字以实现归约；采用类似于一阶逻辑中的前束范式方法可以解决这个问题。相关细节此处从略。

5 宣告须真的逻辑

本节探讨在宣告必须为真的语义设定下的混合公开宣告逻辑。语言L1和L2在该语义设定下的逻辑分别记为L1t 和L2t。形如[φ]@aψ的公式无法找到将宣告消去的归约原则，使得寻找公理系统的难度增加。

将专名引入语言后，很自然地会考虑到间接宣告这一概念。公式[φ]xψ读作“当φ在x所指称的情形下被宣告后，ψ（在现实情形中）为真”。将L2中经典宣告算子（称为直接宣告算子）替换为间接宣告算子[φ]x后得到的语言即L3，该语言下的逻辑记为L3t。逻辑L3t 可以带来技术上的便利。文章将证明逻辑L2t 和L3t 具有相同的表达能力。通过找到后者的可靠且完全的公理系统，就可以得到前者的对应结果。

本节最后第5.4 节中将讨论技术上更复杂的逻辑L1t。

5.1 逻辑L2t

下面给出语言L2（见定义9）在宣告须真设定下的语义定义。

定义12(L2t 语义).任给模型M=(W,R,V)、指派g和可能情形w ∈W，公式[φ]ψ的语义解释如下：

其中Mg,φ=(W,RM,g,φ,V)与定义10 中相同，其他类型公式的语义解释也与定义10 相同。

由此得到的逻辑记为L2t。公式φ中所有自由变名的集合仍然记为Free(φ)。以下结果值得讨论。

命题13.|=L2t@iBa¬φ →[φ]@iBaψ

上述命题中的有效式可以读作“如果主体在某种情况下相信非φ，则当φ在该情形中被宣告后，主体将相信一切”。在L2t 语义中，假设φ在主体相信其为假的情况实际上是真的，则φ被宣告后将导致主体产生冲突信念，从而令主体相信一切。

命题14.任给φ,ψ ∈L2，x ∈Nom ∪Var和s ∈Var使得s/∈Free(φ)，如下结论成立：

根据上述结果，倘若公式[φ]↓sψ中不含@算子且s/∈Free(φ)，则该公式可归约为不含宣告算子的公式。不过由于宣告与@的归约原则的缺失，不足以形成L2t 逻辑的完整归约原则。因此难以通过归约的方法得到L2t 逻辑的公理系统。为解决这一问题，下面首先引入逻辑L3t 并在第5.3 节重新探讨L2t 的公理化。

5.2 逻辑L3t

尽管未能为宣告和@找到归约原则，这却并不意味着L2t 的表达能力严格强于H@↓。本节使用间接宣告算子替换直接宣告算子，并考察两者之间的关系，最后给出混合间接公开宣告逻辑的公理系统。

将语言L2中的直接宣告算子替换为间接宣告算子，得到的语言记为L3。其准确定义如下：

定义15(语言L3).L3公式由以下规则给出：

其中a ∈Ag，p ∈Pr，i ∈Nom 且s ∈Var。语言中的约定如前。

当考虑L3公式中变名的自由或约束时，[φ]s算子不构成对s的约束。公式φ中自由变名的集合仍然记为Free(φ)。

语言L3在宣告须真设定下的语义定义如下：

定义16(L3t 语义).任给模型M=(W,R,V)、指派g和可能情形w ∈W，只需要补充形如[φ]iψ和[φ]sψ公式的语义解释（其他同定义12）：

其中Mg,φ=(W,RM,g,φ,V)与定义10 中相同。由此得到的逻辑记为L3t。

命题17.令x为一专名或变名，且变名s/∈Free(φ′)∪Free(ψ′)∪{x}。如果L2公式φ和ψ分别与L3公式φ′和ψ′逻辑等值，则：

1.[φ]ψ与↓s[φ′]sψ′逻辑等值；

2.[φ′]xψ′与↓s@x[φ]@sψ逻辑等值。

由上述命题很容易得到如下推论。

推论18.L2t 与L3t 具有相同表达能力。即，

1.任给L2公式φ，存在L3公式φ′使得对所有模型M、指派g和可能情形w，M,g,w |=L2tφ当且仅当M,g,w |=L3tφ′；

2.任给L3公式φ，存在L2公式φ′使得对所有模型M、指派g和可能情形w，M,g,w |=L3tφ当且仅当M,g,w |=L2tφ′。

逻辑L3t 中可以得到完整的归约原则。

命题19.任给L3公式φ、ψ和θ，主体a，命题变元p和x,y ∈Nom ∪Var。令且s/∈Free(φ)。则如下公式都是L3t 的有效式：

下面给出L3t 的其他一些有效式，有助于更好地理解该逻辑。

命题20.任给L3公式φ，主体a，专名或变名x和y。则，

对于第一条有效式，宣告真实情形将所有其他（虚假）情形全都排除，这样的宣告起到的效果是真实信息全都被相信。至于第二条有效式，首先，@x的跳转使得间接宣告算子[@xφ]y中的y不起作用；其次，@xφ如果在某个可能情形下为真，则在所有可能情形下都为真，在宣告须真语义设定下不会引起模型更新。

将命题19 中的归约原则添加至H@↓的公理系统K45@↓（图1），就得到了L3t 的公理系统L3t，如图4 所示。

图4:公理系统L3t（其中sx 且sFree(φ)）

命题21(L3t 可靠性).L3t 是可靠的，即由⊢L3tφ可得|=L3tφ。

证明公理系统L3t 完全性的途径是将其归约为已知可靠且完全的系统K45@↓。具体方法类似于第4.1 和4.2 节的完全性证明。下面列出关键的定义与引理，但省略具体细节。

定义22(L3到H(@,↓)的翻译).定义t:L3→H(@,↓)如下（其中a ∈Ag，p ∈Pr，x ∈Nom∪Var 且s ∈Var 使得且Free(φ)）：

定义23.复杂度函数c:L3→N 递归定义如下：

引理24.任给L3公式φ、ψ和θ，命题变元p，主体a，专名或变名x和y以及变名s使得且s/∈Free(φ)。则，

引理25.对任意L3公式φ，均有⊢L3tφ ↔t(φ)。

定理26(L3t 完全性).任给L3公式集Φ 和公式φ，如果Φ|=L3tφ，则有Φ⊢L3tφ。

5.3 逻辑L2t 的公理系统

在上节给出L3t 的公理系统后，本节重新探讨逻辑L2t 的公理系统。思路是利用命题17 将公理系统L3t 使用语言L2加以改写。

定义27.翻译τ:L2→L3定义如下（其中s为不出现于[φ]ψ中的某个变名）：

任给L2公式φ，τ(φ)是它在语言L3中的改写。类似地可以定义从L3到L2的改写函数ρ。然而，ρ必须被小心处理。简单地说，任给某个L3公式，其所有形如[φ]xψ的子公式都必须被替换为↓t@x[φ]@tψ，其中t是未在该公式内自由出现的新变名。下面给出具体定义。

定义28.翻译ρ:L3→L2定义如下：

其中s是不在[φ]xψ中出现的某个变名，t是新的变名。

需要注意的是，上面定义的ρ翻译实际使用过程中最好从极小子公式开始逐步进行改写，而不是从公式最外层开始，否则机械地来讲可能会出现违背t是新变名要求的情况。

命题29.任给L2公式φ,|=L2tφ ↔ρ(τ(φ))。

使用改写规则可以将公理系统L3t 转化为L2t 的公理系统L2t（图5）。

图5:公理系统L2t

L2t 的可靠性与强完全性可以通过改写技巧证得。这里省略具体细节，仅通过图6 说明证明的过程（注意需要从左上方经过下方迂回到达右上方）。

5.4 逻辑L1t

图6:L2t 完全性证明流程图

最后回到语言L1，在宣告须真的语义设定下加以考察，具体语义定义同定义12，由此得到的逻辑记为L1t。第4 节已经证明了逻辑L1u 与逻辑H@具有相同的表达能力，然而那是在宣告可假的语义设定下。要求宣告须真时，未能为宣告与@算子找到归约原则。至于L1u 的表达能力是否严格强于H@也尚未明朗。本节将致力于给出一个可靠且完全的公理系统。

下面是L1t 的一些有效式，他们的相似版本此前在其他逻辑中已有讨论（参见命题13 和20）。

命题30.如下L1公式都是L1t 的有效式：

L1t 的公理系统L1t 可在公理系统K45@的基础上增加额外公理和规则得到。为使行文简介，将缩写为，并将缩写为。L1t 的额外公理与规则列举如下：

上述公理系统中的某些公理可以使用更简单的公理替代。例如Agree′可以换成Agree（图1），通过Agree、NA、K[]、N@和K@可以推出Agree′。

L1t 的可靠性不难验证。L1t 的强完全性可以通过修改K45@的完全性证明以包含宣告算子的情形而加以证明。类似于将[4,第7.3 节]和[2]中的方法相叠加，具体证明过于枯燥和烦复，本文从略。

6 结语

本文探讨了混合公开宣告逻辑，这并不是公开宣告逻辑和混合逻辑的简单拼凑。在此逻辑中可以选择宣告须真和宣告可假两种语义设定，且易于探讨直接宣告和间接宣告这两种行动。文章采用了有别于文献[9]中的处理方法，并相信这一做法更好地遵守了公开宣告逻辑和混合逻辑各自的传统。

文章讨论了三个语言L1、L2和L3，其中L3源于引入间接宣告这一概念。依据是否允许进行假宣告，文章选择性地考察了五个逻辑，即L1u、L2u、L1t、L2t和L3t，分别给出它们的公理系统。此外，文中虽未准确定义，但已经在很大程度上对比了有关逻辑的表达能力。具体结果如下图所示，其中：(1)三横线（含实线和虚线）所连接的两个逻辑表达能力相同；(2)箭头（含实线箭头和虚线箭头）所指向的逻辑其表达能力强于箭头出发处的逻辑；(3)实线所连接的两个逻辑的表达能力对比由直接结论（主要是归约原则）得到，而虚线表示作为推论得到；(4)标有问号的箭头表示相应的表达能力对比关系尚未得到证明，这些将留待未来加以完成。

细心的读者已经发现，本文仅选择探讨了五个混合公开宣告逻辑（表1）。未加讨论的有逻辑L3u、语言H([]x,@)及其在两种语义设定下的逻辑，它们分别又有什么特点？本文并未选择穷尽所有这些逻辑，探讨逻辑L3t 主要是为了将其公理系统改写为逻辑L2t 的公理系统。间接宣告算子[φ]x值得进行更多的研究，我们已将其作为后续工作。

本文只考虑了个体信念，在此基础上考察群体信念是值得在未来去尝试的工作。文献[9]中所采用的方法，即通过删除可能情形来解释宣告的做法可能更适合于模拟S5 知识。探讨基于知识模型的混合动态认知逻辑将是后续任务之一。