图博弈的设计与模态逻辑的发展

约翰·范本特姆    刘奋荣[1]

转自：Tsinghua哲学系

如涉版权请加编辑微信iwish89联系

哲学园鸣谢

摘要：图博弈是一种主体间互动的场景，可以使用模态逻辑的语言描述。模态词用来描述博弈玩家的行为，博弈的均衡和玩家的必胜策略则通常用模态逻辑的公式刻画，这些公式具有特定的模式。取决于博弈目标的设定、对玩家互动机制的设计，图博弈有着各种不同的版本。与之对应，模态逻辑的语言不断发展和扩展，新的逻辑系统也呈现不同的性质。逻辑学一方面作为分析现有图博弈的一种方法，另一方面，逻辑学也是设计新博弈的灵感来源。图博弈与逻辑学之间的相互渗透为研究博弈提供了新的视角，也是对博弈论和计算理论方法的重要补充。

关键词：图博弈；必胜策略；蓄意破坏博弈；博弈逻辑；模态逻辑

基金项目：国家社科基金重大项目“基于社交网络的信息流逻辑研究”（17ZDA026）；清华大学自主科研计划项目“博弈视域中的社交网络逻辑”（2017THZWYX08）

作者简介：约翰·范本特姆 (Johan van Benthem)，斯坦福大学哲学系，阿姆斯特丹大学逻辑、语言和计算研究所,清华大学金岳霖逻辑学讲席教授；刘奋荣，清华大学哲学系、清华大学-阿姆斯特丹大学逻辑学联合研究中心（北京 100084） 

一、图博弈与模态逻辑

图博弈指的是在有向图或无向图上展开的博弈。其中，图中的顶点可以有标注，顶点之间的边可以是各种各样的关系。这种博弈应用非常广泛，常常用来模拟计算、辩论、信息交流、社交网络、战争情境等。例如，就社交网络而言，图中的顶点可以是主体，顶点之间的边可以表示社会关系，也可以是主体之间信息交互的通道。[2]就论辩而言，图中的顶点是论证（argument），顶点之间的关系是论证之间的攻击关系。换句话说，图博弈能够在理论上为社交网络或论辩提供一个模型。[3]在图博弈的研究中，均衡（equilibrium）、必胜策略（winning strategy）等概念常常被用来研究玩家的推理和行为。另一方面，逻辑学作为研究主体推理的一门重要学科，通过形式语言、语义、公理化等手段对其展开研究。模态逻辑是20世纪60年代开始兴起的一门新的逻辑学分支，克里普克的可能世界语义学的模型与图博弈有着非常多的相似点，每个顶点是一个可能世界，可能世界之间是基于主体认知的可及关系。这一部分，我们将通过两个实例和现有的研究成果展示图博弈与模态逻辑之间的密切关系。

（一）旅行博弈

我们先介绍一个图上的旅行博弈。如下图所示，两名玩家A和E中的一位从图G的某个顶点开始沿着G的边旅行到另一个顶点，另一位玩家接着从新顶点出发旅行，如此轮流。如果轮到某个玩家，但没有边可以移动，那么该玩家就输了博弈。如果博弈可以无限进行下去，则玩家E赢。

具体而言，我们假设玩家A先出发。考虑图中左边的部分。玩家A 从顶点1出发，从1旅行到 3，玩家 E接着旅行到 4，因为从4出发没有边了，A输。当然，若E选择移动到1，然后A旅行到3，如此不断重复，博弈一直进行下去，E赢得博弈。有趣的是，A 在这个图博弈中有一个必胜策略：A从1出发先旅行到 2，然后E 旅行到3，而这时，A 旅行到4，这样可以确保E无路可走，A赢得博弈。如果旅行的出发点在其它顶点，我们可以采用类似的方法进行分析。

接下来，我们考虑图中右边的部分。请注意边的细微变化，即，顶点2上有一个自返的边。这就意味着，玩家在顶点2的地方可以在原地旅行。我们仍然考虑玩家A从顶点1开始旅行，则在这个博弈中，E 有一个必胜策略。我们考虑可能的几种情形：首先，假如A从1旅行到 3，E 可以不停地回到1，从而获得胜利。其次，如果A旅行到 2，E走自返的边、停留在顶点2。最后，如果A想要防止 E 通过自返的边无限地停留在 2而获胜，他必须移动到 3，随后E可以移动到4而获胜。

旅行博弈可以有其他的变种。譬如，获胜的条件可能不同于上面的例子，我们将在本文的后面进一步探讨。就目前的旅行博弈版本而言，  根据盖尔-斯图尔特定理 (Gale-Stewart Theorem)，旅行博弈是 “可确定的 (determined)”。这就是说，给定任意的图G和起始位置s，记作 (G, s)，或者玩家 A或者玩家 E 一定有一个必胜的策略。这样的形式结果能够帮助我们更好地理解图博弈中主体的行为规律、博弈的结果趋向。

对逻辑学而言，旅行博弈有太多的启发意义。正如上面所提到的，图与模态逻辑的可能世界语义学有着惊人的相似性：图上的旅行是逻辑学家们立即辨认出的可能世界之间的可及关系，完全可以用模态算子 (modality) 来刻画。具体来说，玩家 E 的必胜策略通常涉及到一个迭代的全称-存在模态算子 □◇，它的意思是，对于A的任何选择E 都有一个相应的移动策略。形式化而言，E 在图博弈中的获胜位置可以由下面的模态µ-演算公式刻画：

νp•□◇p

这个不动点公式刻画了图中顶点的最大子集P。它的意思是，不论玩家A如何旅行，玩家E都可以一直在P集中移动。[4]

也就是说，关于旅行博弈的基本逻辑理论都包含在模态逻辑的理论中。由此，我们可以直接利用模态逻辑的相关结果得到一些关于旅行博弈的推论。譬如，我们可以在多项式时间内完成图的模态性质的模型检测（model checking）。模态语言对于博弈所使用的图是互模拟 (bisimulation) 不变的，这就使得通常的模态逻辑结论在图的变化下保持不变。还有，旅行博弈的模态逻辑的有效式是可判定的。

（二）蓄意破坏博弈

蓄意破坏博弈有两个玩家，一个是旅行者，一个是恶魔。旅行者从图 G中的某一顶点s出发开始旅行，一次沿着一条边进行。恶魔D 每次可以切断图中任何一条边。二者轮流进行。当旅行者达到目标顶点或目标区域时，他赢得博弈；当旅行者在某个点无法移动时，他就输了博弈；当没有边可以切断时，恶魔输了博弈。与前面的旅行博弈最大的不同在于，在蓄意破坏博弈中，由于恶魔不断切断边，初始的图会随着博弈的进行而发生变化。

我们看下面一个具体的博弈。假设旅行者从顶点1出发，希望到达目标顶点4。

在这个博弈中，恶魔有必胜策略：他首先切断3和4之间一条边，之后适当回应旅行者的移动就可以赢得博弈。这里需要注意的是，恶魔的能力是全局性的，他可以切断图中任何一条边。如果我们规定恶魔只能切断旅行者所在点连接的边，那么他就没有必胜的策略了。这些不难看出，我们不再赘述。

同样，蓄意破坏博弈可以对很多有意义的情境进行建模。譬如，受干扰情况下的计算或信息获取过程，或迫使玩家进入图的某一子目标区域的学习过程。蓄意破坏博弈也满足盖尔-斯图尔特定理的条件，即，此类博弈是可确定的。因此，或者旅行者或者恶魔总是有必胜策略的。

        就模态逻辑而言，范本特姆及其合作者们给出了新的模态逻辑对蓄意破环博弈中主体的行为进行研究。[5]这个逻辑在基本的模态逻辑之上添加了新的非标准模态算子■来刻画图的更改，即，描述当一条边 (一个有序对 (x, y)) 从当前的可达关系中被删除后，在当前点上哪些句子为真。旅行者的必胜策略与下面的模态算子模式相关

■◇■◇...

具有这种模式的句子的意思是，无论恶魔怎么切边，旅行者都可以继续旅行。要想刻画旅行者在图博弈中的获胜位置，仍然需要进一步扩展逻辑的语言，把算子■加入到模态µ-演算中。例如，假设蓄意破坏博弈的目标区域是所有满足公式γ 的顶点的集合，我们可以用下面这个公式刻画旅行者的获胜位置：

  νp•(γ∨ (◇Τ∧■◇p))

与旅行博弈不同的是，蓄意破坏博弈的模态理论没有那么简单，相反，有一些让人吃惊的结果。基本的蓄意破坏模态逻辑的模型检测复杂度是多项式空间 (Pspace) 而非多项式时间 (Ptime)。这意味着，在包含干扰的博弈算法中出现了复杂性的跳跃。此外，虽然这类模态逻辑仍可以有效地翻译为一阶逻辑，但它不是可判定的；尽管原则上它是可公理化的，比如说使用适当修改的表列系统 (tableaux)方法，但简单的公理化结果仍然没有找到。对于蓄意破坏µ-演算，情况更为复杂。对不动点逼近的估值很可能需要跨越不同的图。这里存在很多开放的问题需要进一步研究。

我们希望通过上面的两个例子说明图博弈与模态逻辑之间的关系。图博弈的规则可以不同，图本身可以发生变化，相应的，在逻辑学领域，我们可以利用基本模态逻辑或其扩展去刻画博弈中主体的行为，必胜策略，并研究与博弈相关其他问题和规律。逻辑学与博弈之间的这种关联也是本文要重点讨论的，我们主要讨论这种关联如何成为可能，能给我们提供什么样的思考和启发。

Johanvan Benthem (范丙申)：斯坦福大学Henry Waldgrave Stuart教授、阿姆斯特丹大学的大学教授（荣休）、荷兰皇家科学院院士、美国科学院院士、欧洲科学院院士、国际哲学学院院士。1996年获荷兰国家级斯宾诺莎奖 (荷兰在自然科学和社会科学领域的最高奖项)。先后受聘清华大学伟伦特聘教授、教育部海外名师、长江学者讲座教授。

二、博弈的本地化

这一节我们考虑上面博弈的几个具体变种，讨论与之匹配的逻辑理论。

（一）旅行博弈的本地化和占位博弈

首先，我们考虑在旅行博弈中两个玩家本地化的情形。所谓本地化，指的是两个玩家都在图中旅行，有自己的出发点和路线。也就是说，博弈的起始位置由  (G, s, t) 刻画，其中G是博弈图，s 是玩家A的起点，t 是玩家E的起点。我们可以让A先旅行，也可以让两个玩家同时旅行。这里我们考虑前者，即所谓的序列博弈，一个玩家旅行一步之后另一个玩家也旅行一步，二者轮流进行。[6]  此外，我们规定获胜条件或设定一个目标。假定两个玩家的目标都是永远移动下去。这样的博弈不再是零和博弈了，因为两个玩家都能无限移动的结果是平局。尽管虽然我们会说，当一个玩家被卡住而另一个仍可以继续移动，则前一个玩家就输了。

这样的简单修改颠覆了旅行博弈的博弈特性，因为玩家的行为不再直接影响到其对手。当然，从长远的角度看，两位玩家的行为还是互相影响的。即便如此，与模态逻辑的联系仍然存在。此时，模态逻辑的模型是图 (G, s, t) ，其中s和t是两个不同的顶点；模态语言则是“二维的”，而命题变元在单个顶点上为真。我们需要添加下面两个“旅行模态算子” (travel modalities)：

(G, s, t) ╞φ   iff   存在点s‘，Rss’ 且 (G, s’, t) ╞ φ

(G, s, t) ╞φ   iff   存在点t‘，Rtt’ 且 (G, s, t’) ╞ φ

利用这两个模态算子，我们能够更严格地表述前面的一些结果。比如，在起始位置为 (s, t) 的有限图中，如果存在自然数k使得 [left]k 在s上为真，且 [right]k 在t上为假，则第一个玩家就会输掉博弈。[7]此外，玩家的无限移动路径的存在性也可以用µ-演算公式 νp•◇p来刻画。[8]二维模型的基本模态逻辑仍然是可判定的，它与标准的极小模态逻辑没有太大的差别。这是因为这个新的模态语言可以翻译到只包含两个变元的一阶逻辑片段，而这个片段是可判定的。

与上述情景稍有不同，我们可以给两个玩家设定各自所要到达的不同目标区域。这个版本的博弈有一个问题，就是图上的两个玩家是否能够真正互动？一个玩家的行为会必然改变或限制其他玩家的行为么？这涉及到我们对博弈中主体之间互动如何理解的问题。下面的这个例子更能体现这一问题。

我们每个人小时候都玩过捉迷藏的游戏，这里考虑只有两个玩家的情形。事实上，博弈的输赢直接与玩家之间的接触或互动有关。当藏起来的那个玩家听到他的对手说“我找到你啦”的时候，这就意味着后者已经赢得了博弈。在很多国家，类似的游戏也很常见。譬如，有一个叫做”追捕游戏” (games of ‘Catch’)，两个玩家A和E在同一点相遇，则A赢得博弈。这种博弈所对应的逻辑可以像前面一样使用二维模型和模态算子。不过，要表达这种博弈的目标，我们需要特别引入一个新的命题常元I，

M, s, t ╞ I  iff    s = t

换句话说，常元I 表示图G上的等同关系。下面的逻辑公式刻画的是E的获胜位置：

[right]¬ I

我们相信，添加常元后的二维模态逻辑仍然是可判定的。但是，目前尚不清楚如何将上述语言翻译到只含两个变元的一阶逻辑片段，最主要的问题在于我们需要在三个点上作比较：初始点 s和t，以及到达的目标点 s’。[9]

下面，我们接着讨论另外一种博弈，叫做占位博弈 (occupation game) ，玩家在图上要占据某个部分。我们可以设定“玩家到达各自所指定的目标区域” 为决胜条件，考虑下面的具体例子：

假设玩家A从顶点1开始移动。三步后A可以达到他的目标点4，但这样会给玩家 E 足够的时间到达他的目标点10。所以，即使不是A到达其目标点的最短路径，A 应该先移动到5，从而使E 不能到达到他的目标点10。

为了刻画一步步的占位产生的动态变化，我们需要在相应的逻辑语言中增加至少一个动态模态算子

[+p]

这个算子可以用来刻画了当我们使得原子公式p在当前点上为真时，在当前点上成立的所有公式：

M, s ╞[+p] φ   iff    M (p在s 为真), s ╞  φ  

这里的动态算子事实上是一种本地赋值，即让某一原子公式在当前位置上变成真的。以上逻辑语言的扩展看起来非常简单，但是可以证明，这个逻辑可以嵌入到已知的不可判定(undecidable)混合逻辑 (hybrid logic)中去。[10]因此，加入 [+p] 模态算子的模态逻辑是不可判定的。

与占位游戏类似的还有许多十分流行的棋盘游戏，比如 "卡坦岛拓荒 (Settlers of Catan)"。每个玩家都有自己独特的颜色，如果玩家所在的某个点还没有被着色，他会用自己的颜色来着色这个点。当玩家到达一个其它玩家着色的点时，他就输了。还有，已有文献中所讨论的"投毒博弈 (poison game)"也与着色非常像。[11]今年来，不少学者也开始从逻辑学的角度对投毒博弈展开了研究。[12]

（二）蓄意破坏博弈的新版本

我们可以看到，在上一节讨论的蓄意破坏博弈中，两个玩家的能力非常不对称。旅行者只是在图上，只能沿着图上的点和路行走，即所谓的“本地化”。但恶魔的能力却是 “全局的”，因为他可以在图的任何地方实施破坏、切断旅行路线。而在现实中，容易想象旅行博弈中两个玩家的能力对称的情形。譬如，在战争博弈中，旅行者代表战争的一方，恶魔代表他的敌人。恶魔只能在任何旅行者所在的位置上进行破坏——当然恶魔也可以在图上移动，到达某一位置再进行破坏。下面我们考虑几个具体的情境：

例   本地化的双目标蓄意破坏博弈

考虑第一节中最初的蓄意破坏博弈的四点图。现在，玩家 T  和 D在不同的初始位置，T的目标点在右下角，D的目标点在左上角。我们首先要规定哪些行为是允许。具体而言，我们采取 “移动-切除”模式：玩家先沿着某条边移动，然后，如果他愿意的话，切断某条边。

有趣的是，无论允许什么样的行为，这一设定显然会产生输赢之外的更为细化的目标：两个玩家自然都希望到达自己的目标区域而对方没有到达，稍差一点的是他们都到达各自的目标区域，更差一点的是他们都没有到达各自的目标区域，最坏的情况则是对方到达他的目标区域，而自己没有。而在博弈论中，通常的做法是使用效益函数对这几个目标达成的不同程度进行刻画，通过两个玩家获得的效益体现。在研究玩家的推理和选择时，最常用的一个概念是逆向归纳法 (Backward Induction)。假设每个主体都是理性的，即，他们会选择自己获得的效益最高的策略。这样，自然，我们可以利用纳什均衡 (Nash equilibria)的概念找到博弈的解决方案（solution）。

这里，同样有一个图博弈和逻辑匹配的理论问题。什么样的逻辑可以分析这里提到的不同程度的目标达成，以及主体在博弈中的选择等问题呢？考虑玩家的选择自然可以使用偏好逻辑，而且，若目标都可以在逻辑语言中表述的话，可以使用基于优先性的偏好逻辑。[13]当然，我们也可以提出新的博弈逻辑语言，直接在逻辑语言中使用特别的常元表示目标点等，在那样的博弈逻辑中研究博弈，同时也研究新的逻辑的语言和语义等问题。[14]用逻辑学研究最大的优点在于，我们可以考虑主体的高阶推理，一个玩家的选择是基于他自己的知识、他对对手选择的判断，等等。逻辑学的形式语言为研究这样的推理提供了非常方便的工具。这里提到的技术细节，我们留给感兴趣的读者去探讨。

三、图博弈设计的参数

在讨论了图博弈和一些新版本之后，让我们在这一节稍作一个总结，主要针对图博弈的一些结构特点。因为图博弈的结构特点直接影响到博弈本身的设计，也影响到对应的逻辑的提出。[15]图博弈可以从两方面进行分类：博弈的一般结构 (移动、回合、目标) ，以及图的结构——即博弈所在的棋盘的结构。

第一、玩家移动的方式。在选择图博弈的移动方式时，一般的区分是本地移动和全局移动。换句话说，就是玩家在图中是否被本地化的问题。具体而言，玩家是像蓄意破坏博弈的旅行者只能在图中移动，还是像恶魔一样可以全局随意地切断路线。第二种区分是，玩家的每一步移动是任意的，还是可定义的。到目前位置，我们讨论的恶魔切断图中的边，是完全随意的。但是，我们完全可以想象，要切断的边需要满足逻辑语言所定义的性质。与这种区分相关的进一步的问题是，一旦确定要切断的边的性质，恶魔是一次切断一条边，还是一次切断满足性质的所有的边？这些不同的选择直接影响到博弈的不同玩法，同时影响到不同逻辑的语言和性质。[16]

第二、输赢条件的设定。在简单的图博弈中，玩家的目标点可以规定好，因此可以说是能独立定义的顶点。根据定义，玩家要么必须避开某个或某些点，或者需要进入图中的一个区域。然而，在类似捉迷藏的博弈中，玩家的目标常常相互影响。在这类博弈中，藏起来的一方一旦被发现，他就输了，同时，他的对手赢得了博弈。这类目标不再是旅行者或恶魔的独立定义的目标或其布尔组合，而是他们的位置之间的一种二元关系。此外，我们还可以做出更细致的规定，从而影响玩家输赢的条件。譬如，玩家不能两次访问相同的顶点。在占位博弈中，一个玩家不能访问他对手已经访问过的路径。目标的设定是否足够一般化，也直接影响到我们能否采用逆向归纳法或其它方法来求得纳什均衡。

第三、博弈棋盘的设定。到目前位置，我们讨论的图博弈，顾名思义，是在图上展开的博弈。博弈的图就像其他室内博弈的棋盘。但是，除了单纯的顶点和边外，博弈的进行需要更多的关于图的结构的信息。当玩家在图上移动时，我们至少需要显示玩家的周边环境；在更复杂的占位博弈中，我们需要在节点上添加更多的用命题描述的信息，从而可以讨论这些节点是否已被访问过，甚至访问有多频繁等问题。一般而言，博弈的棋盘不仅仅是图，而是带很多“标注”的图。

对这些博弈设计参数的讨论，引发了一系列的理论问题。在第二节中，我们讨论了如何将博弈本地化的问题。我们看到，那样的改变直接影响到玩家在博弈中新的游戏方式。问题是，我们能否对所有可能的改变方式有更好的理解？譬如，能否建立一个标准，用它来衡量这些改变对博弈带来的影响。譬如，在计算复杂性方面，哪些设计的改变会对复杂性产生影响？另一方面，博弈的逻辑性质有没有随着博弈参数的变化还能以某种方式保持的性质？例如，获胜条件通常是 “单调的”：当我们扩大目标区域，之前某个玩家的获胜条件仍然是他的获胜条件。还有没有类似的性质？

还有一个问题设计到不同博弈之间的关系。我们一直在讨论通过各种方式改变博弈，问题是：新博弈的设计背后有隐藏的归约吗？真正称得上不同博弈的到底有多少种？两个图博弈何时等价？  这些问题都涉及到博弈之间关系的研究，特别是，对博弈之间等价的概念如何界定和理解的问题。已有文献对类似的问题有过一些讨论，但是需要拓展到本文研究的不同博弈中来。

四、图博弈的逻辑谱系

了解了设计图博弈的各种设计选择后，接下来我们着重讨论与它们相匹配的逻辑语言和逻辑系统。

首先讨论模态逻辑。我们已经看到，模态逻辑的语言具有足够的表达力，可以描述简单的博弈。前面我们提到，可以把基本的模态逻辑扩张成二维模态逻辑，从而可以表示两个玩家在图博弈中从不同的点出发的情形。然而，并非所有这些表达力更好的新逻辑语言都是标准的逻辑，这就为逻辑学本身的发展提出许多具有挑战性的开问题。图博弈的逻辑基本上都包含基本的模态算子，需要重点理解的是其动态模态算子。然而，在有些情况下，动态模态算子的表达力往往可以通过静态的混合模态逻辑来实现。[17]更极端地说，一阶逻辑本身就能被用于刻画图的变化。当前已知的模态语言还不能一般地刻画博弈论的某些概念，比如说获胜的位置，因此我们不得不求助于不动点模态语言，比如说 μ-演算。最后，当目标变得比输赢更复杂时，博弈论真正关心的是均衡问题，而我们对图的逻辑的强调就达到了它的极限。

此外，我们也可以用标准的 “博弈逻辑”来分析博弈结构，从而刻画图博弈。这种语言表达力丰富，可以刻画玩家在图中的移动，他们的偏好和他们所能采取的策略。这种语言的表达式通常可以在博弈中被解释，无论是其扩展型博弈还是策略型博弈。在某些情况下，这些表达式也可以在刻画博弈玩家能力的相关模型中进行解释。[18]评价博弈逻辑的标准是看它们是否可以刻画标准的博弈论求解方案，比如逆向归纳法或重复删除严格受限策略法(Iterated Removal of Strictly DominatedStrategies)。我们相信，具有复杂偏好的图博弈最终需要使用博弈逻辑来进行研究。本文的目的不在于给出图博弈的模态逻辑或博弈逻辑的所有技术问题，但是，我们的讨论确实可以激发这两个领域联手合作，从而一方面设计出具有趣味性的博弈，另一方面，给出理论上具有挑战性的逻辑语言和系统。

使用逻辑学的手段描述博弈具有很多优势。逻辑学可以描述博弈所刻画的交互式情景中主体的推理模式。我们还可以使用模型检测等技术手段来验证博弈是否具有某些特定的性质。而对于逻辑学家而言，也许更有挑战的是推动博弈论领域的学者研究相关的问题。譬如，其中一个问题是关于图博弈的一般策略：在博弈中，是开场的玩家还是回应的玩家具有绝对的优势？对于很多博弈，我们都可以问这样的问题。下面我们用更为精确的方法表述。

在蓄意破坏博弈中，随着有限图趋于无穷大，玩家的获胜位置会发生什么变化？这个问题与逻辑学密切相关。一阶逻辑的 “零一律 (Zero-One Law)” 告诉我们，当图趋于无穷大时，每个包含二元关系的一阶句子为真的概率变为0或1。给定一个公式，我们甚至可以能行地判定是两种选择中的哪一种。零一律已经被推广到带不动点算子的一阶逻辑（LFP  (FO)）中。[19]前面的讨论表明，我们已经能够在蓄意破坏 μ-演算中描述蓄意破坏博弈的获胜位置，而这样的描述也可以翻译到LFP (FO)。因此，能够用这种语言描述的任何内容都符合“零一律”。这个结果还不能立即应用于获胜位置，因为这些描述一般涉及包含特定点的图，而不仅仅是一般的图。对于前者， “零一律” 是失效的。然而，基于LFP (FO) ，我们仍然可以得到如下论断：两个玩家都有获胜的位置，旅行者的每一个获胜位置必须与他的另外的获胜位置中的至少一个相连。我们相信，这个例子提供了一个全新的视角，也是到目前为止关于图博弈的逻辑研究尚未涉略的问题。

当然，需要说明的是，我们并非在声称逻辑学的每一个属性都能立即导入图博弈的讨论中去。举个例子，虽然对逻辑学家而言，逻辑系统的计算复杂性是很重要的问题。但是，就图博弈而言，这仅仅告诉我们某些图博弈的理论可能很复杂，而不是解决这些博弈的算法很复杂。[20]

从博弈到逻辑学的方向上，一个显然的问题是：是否存在自动方法将前面那些图博弈的定义转换为与之相匹配的逻辑？从前面的讨论可以看出，我们有一个系统方法来创建这样的匹配，但还没有看到更为普遍的一般性结果。从逻辑学到博弈这一方向上，则有着非常悠久的历史，有为各种逻辑概念或推理而设计博弈的传统。这种传统可以追溯到20世纪50年代的数理逻辑，还有根植于几个世纪之前逻辑的对话辩论传统中。[21]

一般而言，“博弈的逻辑” 和 “逻辑作为博弈” 这两种观点的联系十分微妙，其中还有许多未解的问题。[22]从第一节中我们就已经注意到，图博弈对这两种观点都有所涉及，一方面图博弈可以很好地用逻辑学的语言进行刻画，而对这些逻辑学本身的评估又可以使用图博弈。这是下面这个一般性问题的特例：当我们追求 “博弈，博弈的逻辑，博弈的逻辑的博弈”或者 “逻辑，逻辑的博弈，逻辑的博弈的逻辑” 之类的循环时，究竟会得到什么？这种循环不一定能趋于稳定，但它们一旦稳定下来，图博弈很可能是一个很有吸引力的研究平台。我们希望将图博弈看作是博弈逻辑和逻辑博弈之间的张力消失的一个自然场所。

五、结语

本文重点研究了图博弈，将其看作时博弈与逻辑交汇的一个自然选择。文章的贡献在于提供一种全新的思考方式。当然，我们知道，图博弈在其他领域，譬如博弈论、计算机科学等领域都有研究。我们企图表明，逻辑学能够提供独特的研究视角。为了支持这样的思维方式，我们讨论了一系列的博弈实例，并分析了可能的图博弈的设计变化。与之平行，我们讨论了如何使用模态逻辑及其扩展表达图博弈的一些性质。这种博弈和逻辑学之间的平行观点不仅给我们带来了新的启发，帮助我们设计新的有趣的博弈。另一方面，由于新的博弈的新特点，也为逻辑学的表达力和推理等提出了挑战性的理论。我们在讨论了一般的博弈与逻辑学的联系后，最终认为图博弈是理想的工具，既可以作为逻辑学的研究对象，又可以作为评估逻辑学的工具手段。

这个文章的研究才刚刚起步，我们已经在前面提出了很多开放的问题。这里只给出几个未经提及的问题，希望有兴趣的读者可以继续讨论和研究。本文假设的博弈都是所谓的完全信息条件下的博弈，即，我们假设玩家掌握博弈的所有信息。而更为有趣的是存在不确定性的情形。用专业的术语说，就是在不完全信息条件下的博弈。这时，主体的推理依赖他们的信念，不完全信息博弈的均衡一般是概率的，并涉及到混合策略。在逻辑学的层面我们需要使用认知逻辑、概率推理对博弈进行研究。或者，可以从玩家的视域出发进行研究。[23]另外，社会实际上是一个大型实验室，其中新的博弈一直在被设计出来。对本文讨论的一个自然补充和挑战是把理论上的博弈和真实世界的博弈联系在一起。真实世界的博弈显然不像我们所描述的博弈那样，因为实际的博弈往往是在固定的平台上进行的，其中的变化来自于其它的因素，比如偶然移动或玩家的认知局限等。但这并不意味着它们之间没有联系，只是现阶段的研究还没有讨论到此类问题罢了。

Interaction Between Graph Game Design and Modal Logics

Johan van Benthem and Fenrong Liu

Graph games are interactive scenarios with a widerange of applications. This position paper discusses old and new graph games intandem with matching logics, and identifies general questions behind thismatch. Throughout, we pursue two strands: logic as a way of analyzing existinggames, and logic as an inspiration for designing new games. Our aim is modest:we propose a style of thinking that complements existing game-theoretic andcomputational ones, we raise questions, make observations, and suggest researchdirections. Technical results are left to future work.

[1]本文的部分内容在清华大学、牛津大学和斯坦福大学报告过，感谢听众给予的宝贵意见。特别感谢Julian Gutierrez、David Grossi、 Valentin Granko、Rineke Verbrugge、Mike Wooldridge、李大柱和陈钰提出的建议和意见。十分感谢邢锟将论文的英文早期版本翻译成中文。

[2] Fenrong Liu, Patrick Girard and Jeremy Seligman, Logical Dynamicsof Belief Change in the Community, Synthese,191(11): 2403-2431, 2014.

[3]参见最早的文献Phan Minh Dung, On the Acceptability of Arguments and its FundamentalRole in Nonmonotonic Reasoning, Logic Programming, and n–person Games. Artificial Intelligence. 77 (2): 321–357,1995；本期同一栏目下的另一篇论文也是以论辩逻辑为形式工具对社交网络中的实践推理展开研究：廖备水，余喆，莱恩∙范德托：关于规范、价值和偏好的实践推理。

[4]这里实际上涉及“稳定性”的概念，譬如，社交网络中主体的行为在什么条件下能够达到稳定状态。最新的讨论，见论文：刘奋荣, 谢立民，关于社交网络中主体行为的推理和预测,《暨南大学学报》，2018，即将发表。

[5] Guillaume Aucher, Johan van Benthem and Davide Grossi, Modal Logicsof Sabotage Revisited, Logic andComputation, 28(2): 269–303, 2017.

[6]序列博弈（sequential games）是玩家选择策略有时间先后的博弈形式。与之相对的是两个玩家同时选择策略，叫作共时博弈（simultaneous games）。

[7] Krister Segerberg, Two-Dimensional Modal Logic, Journal of Philosophical Logic, 2(1): 77-96, 1973.

[8]然而，在基本模态语言中，甚至在模态µ-演算中，似乎没有一个公式可以表达首先到达目标这样的性质。

[9]相遇博弈 (meeting game) 和模态互模拟之间有一个有趣的类比。如果两个模型M, N上的点s, t 之间满足如下条件，则它们之间具有互模拟关系：从s到M中s的某个后继点s’ 的每一步，都存在t到N中t的某个后继点t’ 的某一步与之相匹配（即 s’Zt’ 成立）。博弈的互模拟很像相遇/回避博弈。众所周知，互模拟是不能用只包含三个变号的一阶公式来刻画，因此它的元理论比较复杂。

[10] Declan Thompson, A Modal Logic of Local Graph Change, Department ofPhilosophy, Stanford University, 2018.

[11]Pierre Duchet and Henri Meyniel, Kernels in Directed Graphs: APoison Game,Discrete Mathematics, 115:273-276, 1993.

[12] Chris Mierzewski and Francesca Zaffora Blando, The Modal Logic(s)of Poison Games, Department of Philosophy, Stanford University, 2016.

[13] Fenrong Liu, Reasoning about PreferenceDynamics, Dordrecht: Springer Science Publishers, 2011, pp.87-122.

[14] Johan van Benthem, Logic inGames, Cambridge MA: The MIT Press, 2014, pp.85-102.

[15] Fenrong Liu, Choice Points for Graph Games, Seminar Note,  Department of Philosophy, Tsinghua University,2017.

[16] Dazhu Li, Losing Connections: Modal Logics of Definable LinkDeletion, Department of Philosophy, Tsinghua University, accepted and presentedat LOFT 13, Milano, 2018.

[17] Carlos Areces, Raul Fervari and Guillaume Hoffmann,Relation-Changing Modal Operators, LogicJournal of the IGPL, 23(4):601-627, 2015.

[18]Johan  van Benthem and DominikKlein, Interfaces of Logic and Games,StanfordOn-Line Encyclopedia of Philosophy, 2018.

[19] Yuri Gurevich and Saharon Shelah, Fixed-Point Extensions ofFirst-Order Logic,Annals of Pure andApplied Logic, 32: 265-280, 1986.

[20] Johan van Benthem,  Logical Dynamics of Information andInteraction, Cambridge UK: Cambridge University Press, 2011, pp.250-252

[21] Erich Grädel,  WolfgangThomas and Thomas Wilke, eds, Automata,Logics, and Infinite Games: A Guide to Current Research, Lecture Notes inComputer Science 2500, Berlin: Springer Science Publishers,  2002.

[22] Johan van Benthem,  Logic in Games, Cambridge MA: The MITPress, 2014, pp.495-506.

[23] Chanjuan Liu, Fenrong Liu and Kaile Su,  A Dynamic-Logical Characterization ofSolutions in Sight-Limited Extensive Games, Proceedingsof PRIMA 2015, pp.467–480.