动态认知逻辑（二）

CS5 上的单代理 (PAL) 的可满足性问题是 NP 完全问题 (Lutz 2006)。

CS5 上的多代理 (PAL) 的可满足性问题是 PSPACE 完全的 (Lutz 2006)。

C 上的 (PAL) 的模型检查问题在 P 中（Kooi 和 van Benthem 2004）。

关于上述 PAL 理论需要注意的一点是，它是在 PAL 友好逻辑 L 上参数化的。因此，“公共公告逻辑”作为一个研究领域实际上涵盖了广泛的家庭个人公共公告逻辑，一个对于 L 的每个实例。除非另有说明，否则我们提出的结果和概念适用于该族中的所有逻辑。

在附录 E 中，我们详细介绍了公共公告逻辑的更多方面：图式有效性、表达性和简洁性、Gerbrandy-Groeneveld 公告、保持一致性的公告和箭头更新逻辑，以及任意公共公告逻辑中对公共公告的量化。

虽然迭代的公共公告似乎是一个需要考虑的自然操作（例如，受到 Muddy Children Puzzle 的推动），但 Miller 和 Moss (2005) 表明，这种语言的逻辑不能被递归公理化。

最后，附录 B 中介绍了基于 PAL 的 Cheryl 生日、Muddy Children 以及 Sum 和 Least Common Multiple 谜题的解决方案。

2.2 群体知识：公共知识和分布式知识

2.2.1 常识

为了推理常识和公共公告，我们将常识运算符 [B*] 添加到每组代理 B⊆A 的语言中。公式[B*]F读作“B组中的常识是F为真”。我们将公知逻辑的语言（？？？）定义如下：

F::=p∣F∧F∣ØF∣[a]F∣[F!]F∣[B*]F

pεP,aεA,B⊆A

这种语言在指向 Kripke 模型上的语义在附录 A 中定义。我们回顾两个关键的定义表达式：

[B]F 表示 ⋀a∈B[a]F —“B 组中的每个人都知道（或相信）F”；

[C]F 表示 [A*]F——“众所周知（或信念）F 是真的。”

为了下文方便起见，我们将在本小节的其余部分中采用对公式的认知（即知识）阅读。特别是，使用语言（PAL+C），我们能够提供一种正式的意义，其中公共公告带来了常识。

定理。对于每个尖 Kripke 模型 (M,w)，我们有：

M,w⊨[p!][C]p 对于每个命题字母 p∈P。

“一封提案信公布后就成为常识。”

如果 F 成功（即 ⊨[F!]F），则 M,w⊨[F!][C]F。

“一个成功的公式公布后就会成为常识。”

现在我们用常识来检验公理化的公告逻辑理论。

公理理论PAL+C。

PAL 理论的公理方案和规则

常识的公理方案：

[B*](F→G)→([B*]F→[B*]G)

“常识在逻辑结果下是封闭的。”

[B*]F↔(F∧[B][B*]F)，“混合公理”

“共同知识相当于真理和共同知识的群体知识。”

[B*](F→[B]F)→(F→[B*]F)，“归纳公理”

“如果存在常识，即真理意味着群体知识并且存在真理，那么就有常识。”

CK必然性规则：从F推导出[B*]F

“每个有效性都有共识。”

公告-CK规则：由H→[F!]G和(H∧F)→[B]H，推导出H→[F!][B*]G

“如果 H 保证 F 公布后 G 的真实性，并且 H 和 F 的联合真实性保证 H 的群体知识，那么 H 保证 F 的公布将导致 G 的共同知识。”

PAL+C 健全性和完整性（Baltag、Moss 和 Solecki 1998、1999；另请参见 van Ditmarsch、van der Hoek 和 Kooi 2007）。 PAL+C 相对于指向 Kripke 模型的集合 C* 来说是健全且完整的，其底层公共公告逻辑 PAL 是健全且完整的。也就是说，对于每个 (PAL+C)-公式 F，我们有 PAL+C⊢F 当且仅当 C*⊨F。

与没有常识的逻辑 PAL 的完整性证明不同，有常识的逻辑 PAL+C 的证明不是通过约简定理进行的。这是因为在语言中添加常识会严格提高表达能力。

定理（Baltag、Moss 和 Solecki 1998、1999；另请参见 van Ditmarsch、van der Hoek 和 Kooi 2007）。在所有指向克里普克模型的类别中，具有公共知识的公告逻辑语言（PAL+C）严格来说比不具有公共知识的语言（PAL）更具表现力。特别是，对于所有尖克里普克模型的类，(PAL+C) 公式 [p!][C]q 不能在 (PAL) 中表示：对于每个 (PAL) 公式 F，都存在一个尖克里普克模型模型 (M,w) 使得 M,w⊭F↔[p!][C]q。

这个结果排除了 PAL+C 约简定理的可能性：我们无法找到每个 (PAL+C) 公式的无公开等价物。这导致 van Benthem、van Eijck 和 Kooi (2006) 开发了一种类似公共知识的算子，对于它来说，归约定理确实成立。结果是二元相对化常识算子 [B*](F|G)，即“F 是 B 组中相对于 G 为真的信息的常识”。相对化常识的语言（？？？）由以下语法给出：

F::=p∣F∧F∣ØF∣[a]F∣[F!]F∣[B*](F|F)

pεP,aεA,B⊆A

而带有公告的相对化常识的语言(？？？)是通过将公告添加到(RCK)来获得的：

F::=p∣F∧F∣ØF∣[a]F∣[F!]F∣[B*](F|F)∣[F!]F

pεP,aεA,B⊆A

(RCK)的语义是(ML)的语义的扩展，并且(RCK+P)的语义是(PAL)的语义的扩展。在每种情况下，扩展都是通过添加以下归纳真值子句来获得的：

M,w⊨[B*](F|G) 成立当且仅当 M,v⊨F 对于每个 v 满足 w(R[G!]B)*v

这里我们回想一下，R[G!]是G公开后得到的函数；也就是说，我们有 xR[G!]ay 当且仅当 x 和 y 在 G 公布后的模型中（即 M,w⊨G 和 M,y⊨G）并且有一个 a 箭头原始模型中的 x 到 y（即 xRay）。关系 R[G!]B 是 B 中那些主体的关系的并集；也就是说，当且仅当存在带有 xR[G!]ay 的 a∈B 时，我们才有 xR[G!]By。最后，(R[G!]B)* 是关系 R[G!]B 的自反传递闭包；也就是说，我们有 x(R[G!]B)*y 当且仅当 x=y 或者存在有限序列

xR[G!]Bz1R[G!]B⋯R[G!]BznR[G!]由

连接 x 到 y 的 R[G!]B 箭头。因此，总而言之，公式 [B*](F|G) 在 w 处为真，当且仅当 F 世界位于从 w 开始的每个有限路径（长度为零或更大）的末尾时，仅包含G 世界，并且仅对 B 中的代理使用箭头。直观地说，如果 B 中的代理通常假设 G 在共同考虑给定事态 w 的可能替代方案时是正确的，那么相对于这个假设，F 是B．人们之间的共同知识

正如 van Benthem、van Eijck 和 Kooi (2006) 所观察到的，相对化的常识与公告后的非相对化的常识不同。例如，在所有指向 Kripke 模型的集合上，以下公式不等价：

Ø[{a,b}*]([a]p∣p) —“事实并非如此，相对于 p，a 和 b 之间的共识是 a 知道 p。”

[p!]-[{a,b}*][a]p —“p 被宣布后，a 知道 p 并不是 a 和 b 之间的共识。”

特别是，在图 1 所示的指向模型 (M,w) 中，公式 Ø[{a,b}*]([a]p∣p) 为真，因为存在一条从 w 开始的路径，仅包含p 世界，仅使用 {a,b} 中的箭头，并以 Ø[a]p 世界 u 结束。

中号

图 1：尖头 Kripke 模型 (M,w)。

然而，公式 [p!]-[{a,b}*][a]p 在 (M,w) 处为假，因为在宣布 p 后，图 2 中所示的模型 M[p!] 获得：该模型中的所有世界都是 [a]p 世界。事实上，只要 p 为真，公式 [p!]Ø[{a,b}*][a]p 总是假：在 p 宣布后，剩下的都是 p 世界，因此每个世界都是一个p世界。

中号[p!]

图 2：尖头 Kripke 模型 (M[p!],w)。

有或没有公开公告的相对化常识的公理化理论以及相应语言的表达结果详见附录 F。

我们现在陈述本小节的语言的两个复杂性结果。

(PAL+C) 和 (RCK) 复杂性。令 C 为所有 Kripke 模型的类。令 CS5 为 Kripke 模型的类，使得每个二元可访问性关系都是自反、传递和对称的。

CS5 上的 (PAL+C) 和 (RCK) 的可满足性问题都是 EXPTIME 完全的 (Lutz 2006)。

C 上的 (PAL+C) 和 (RCK) 的模型检查问题在 P 中（Kooi 和 van Benthem 2004）。

在本文的其余部分中，除非另有说明，否则我们通常假设我们正在使用不包含常识或相对化常识的语言。

2.2.2 分布式知识

群体知识的另一个概念是分布式知识（Fagin et al. 1995）。直观地讲，一组 B 代理拥有分布式知识，即 F 为真，当且仅当他们将他们所知道的所有信息集中在一起时，他们就会知道 F。例如，如果代理 a 和 b 将要访问一个共同的网站，那么他们将知道 F。朋友，a 知道朋友在家或在工作，b 知道朋友在工作或在咖啡馆，那么 a 和 b 就分发了朋友在工作的知识：将他们所知道的信息汇总在一起后，他们都会知道朋友的位置。 Wáng 和 Ågotnes (2011) 对分布式知识和公共公告进行了研究。与此相关的是研究群体知识的概念（例如分布式知识）是否满足群体已知的事物可以通过通信而建立的属性；详情请参见 Roelofsen (2007)。

2.3 摩尔句子

似乎公开声明总是“成功”，这意味着在宣布某件事后，我们可以保证它是真实的。毕竟，这通常是公告的目的：通过发布公告，我们希望告知所有人其真相。然而，不难发现，发布时是真实的，发布后却是虚假的；也就是说，并非所有的公告都会成功。以下是一些简单英语的日常示例。

首次来阿姆斯特丹的A探员在阿姆斯特丹史基浦机场下飞机后如实表示，“A从未在阿姆斯特丹发表过声明”。

这是不成功的，因为它是“自欺欺人的”：它排除了过去的各种陈述，但它本身就是被排除在外的人之一，因此该公告违反了它所说的话。

一个不知道正在下雨的特工，被告知：“正在下雨，但一个不知道”。

这是摩尔公式的一个示例，它是“ p为真”的句子，但代理A不知道p。”在语言（ML）中，摩尔公式具有p p∧[a] p的形式。摩尔公式的宣布是不成功的，因为在公告后，代理人知道了第一个相关的P（示例中的“正在下雨”的说法），因此伪造了第二个conjunct- [a] p（语句“说明”一个示例中不知道它正在下雨。

不成功的公式的对立面是“成功”的公式：这些是宣布之后的公式。在这里，应该区分“表演公告”，从而通过其发生的真相（例如，法官说，反对意见被否决了”，这具有使异议推翻的效果）和“信息性公告”，这些公告只是简单地告知他们的公告真理的听众（例如，我们的共同朋友说：“我住在207街上”，这可以通知我们已经是真实的事情）。使用事实变化，最好在动态的认知逻辑环境中解决表演公告，这是附录G中讨论的主题。现在，我们的关注是信息通知。

Hintikka（1962）早期就注意到了（联合国）成功的现象，但直到动态认识论逻辑出现之前，才详细研究。在DEL中，公开公告的明确语言提供了（联合国）成功性的显式句法定义。

（联合国）成功的公式（Van Ditmarsch和Kooi 2006；另请参见Gerbrandy 1999）。让F成为具有公开公告的语言的公式。

说f成功意味着⊨[f！] f。

“成功的公式是宣布之后始终是真实的。”

说F是不成功的，这意味着FIS不成功（即⊭[F！] F）。

“一个不成功的公式是宣布后可能是错误的。”

如我们所见，摩尔公式

p∧[a] p

是不成功的：如果（MF）是正确的，则其公告消除了所有¬p-worlds，从而伪造¬[a] p（因为¬[a] p的真相要求存在一个a-arrow，导致一个箭-世界）。

成功公式的一个例子是命题字母p。特别是，在宣布P之后，很明显，P仍然存在（因为命题估值没有改变）；也就是说，[p！] p。此外，正如读者可以轻松验证的那样，公式[a] p也是成功的。

在考虑（联合国）成功的公式时，出现了一个自然的问题：我们可以提供（联合国）成功的公式的句法表征吗？也就是说，有没有办法让我们知道一个公式（联合国）是否仅通过查看其形式而成功？建立在Visser等人的工作中。 （1994年）和Andréka，Németi和Van Benthem（1998），van Ditmarsch和Kooi（2006）提供了一些成功（PAL+C） - 成符号的特征。

定理（Van Ditmarsch和Kooi 2006）。保留的公式由以下语法形成。

f :: = p的p right [a] f f∨[a] f fim [b ∗] f

p∈P，a∈A，b⊆a

每个保留的公式都是成功的。

使用稍有不同的成功概念，其中forula f被认为是成功的，并且只有当我们具有m，w⊨f∧⟨a⟩f表示m [f！]，对于每个尖头的kripke模型（m） ，w）来自给定C类，Holliday和Icard（2010）提供了（联合国）对单人S5 Kripke模型的（联合国）的全面分析，并且在单代理KD45 Kripke模型类别。特别是，它们在这些类别的Kripke模型上提供了成功公式的句法表征。 Saraf and Sourabh（2012）将该分析部分扩展到了多代理设置。这些作品的高度技术细节超出了本文的范围。

有关摩尔句子的更多信息，我们将读者推荐给斯坦福大学的第5.3节，《认知悖论哲学哲学条目》（Sorensen 2011）。

3。复杂的认知相互作用

在上一节中，我们专注于一种模型转换行动：公开公告。在本节中，我们研究了由于Baltag，Moss和Solecki（Baltag，Moss和Solecki 1998）而引起的公开公告的流行“行动模型”概括，共同称为“ BMS”。动作模型是简单的关系结构，可用于描述各种信息行动，从公开公告到可能包含隐私，误导，欺骗和怀疑程度的更微妙的通信，仅举几个可能性。

3.1动作模型描述了复杂的信息场景

首先，让我们考虑一个更复杂的交流行动的具体示例：一个完全私人的公告。这一行动的想法是，一个代理，让我们称她为A，是在完全隐私中收到一条消息。因此，没有其他代理商不得学习此消息的内容，此外，没有其他代理人首先考虑代理A收到消息的可能性。 （想一想一个未注意到秘密和安全的位置的代理商，查找和阅读编码的消息，只能解码，然后破坏消息。）考虑此操作的一种方法如下：可能发生的事件。其中之一，让我们称之为事件E，是p为真实的公告。这是给a的秘密信息。另一个事件，我们称之为f，是宣布命题常数⊤事实是真实的，这一行动没有传达新的命题信息（因为⊤是重言式）。代理A应该知道消息是P，因此实际上发生的事件是e。所有其他代理都应该错误地认为，众所周知，信息是⊤，甚至没有考虑消息为p的可能性。因此，其他代理人应该考虑事件，唯一的可能性，并且错误地认为这是常识。我们想象图3中此设置的图表表示。

Pria（P）

图3：尖锐的动作模型（PRIA（p），e），以完全私人向代理A公告。

在图中，我们的两个事件E和F被描绘为矩形（将它们与Kripke模型的圆形世界区分开来）。事件发生时宣布的事件矩形内出现的公式。因此，事件E代表P的宣布，事件F代表宣布⊤。实际发生的事件（称为“点”）使用双矩形表示；在这种情况下，重点是e。 A唯一可以考虑的事件是E，因为唯一的A-arrow将E循环直接回到e。但是，我们代理商中的所有代理都设定了一个除错误将替代事件f视为唯一可能性的可能性：所有非A-Arrows都将E点为f。此外，从事件F的角度来看，众所周知，事件F（及其对⊤的宣布）是唯一发生的事件：每个代理都完全有一个箭头离开f，并且该箭头循环直接回到f。因此，上图所示的结构描述了以下操作：p要宣布，代理A是要知道的，并且所有其他代理商都会错误地认为宣布⊤的常识是宣布。如图3中所示的结构称为动作模型。

动作模型（Baltag，Moss和Solecki 1998，1999；另请参见Baltag和Moss 2004）。文献中的其他名称：“事件模型”或“更新模型”。给定一组公式L和有限的非代理集a，动作模型是一种结构

a =（e，r，pre）

由

可能发生的可能发生的交流事件的非空置集合

一个函数r：a→p（w×w），分配给每个代理A∈

一个函数pre：e→l，分配给每个事件e∈Ea先验公式pre（e）∈L。直观地，当事件E发生时宣布前提条件（e）。

符号：如果A是动作模型，则使用{E，r，pre}中的符号添加superscript a来表示三重组成部分，该组成部分以某种方式（EA，RA，PREA）（EA，RA，PREA） = a。我们将尖头的动作模型（有时也称为动作）定义为由动作模型A和事件e∈E组成的对（A，E），称为点。在绘制动作模型中，将事件绘制为矩形，并用双矩形指示点（如果有）。我们将许多相同的图纸和术语约定用于用于（尖）Kripke模型的动作模型（请参阅附录A）。