逻辑与游戏 and games (Wilfrid Hodges and Jouko Väänänen)

首次发表于 2001 年 7 月 27 日，实质修订于 2019 年 8 月 16 日。

二名玩家之间的游戏，其中一名玩家获胜而另一名玩家失败，成为二十世纪下半叶逻辑学许多分支中常见的工具。重要的例子包括用于定义真理的语义游戏，用于比较结构的来回游戏，以及用于表达（或许解释）形式证明的对话游戏。

1. 逻辑学史上的游戏

逻辑学与游戏之间的联系可以追溯到很久以前。如果将辩论看作一种游戏，那么亚里士多德早已建立了这种联系；他关于三段论的著作与他对辩论目标和规则的研究密切相关。亚里士多德的观点一直延续到中世纪对逻辑的普遍称呼：辩证法。二十世纪中叶，查尔斯·汉布林重新唤起了对话与合理推理规则之间的联系，不久之后，保罗·洛伦岑将对话与逻辑的建设性基础联系在一起。

游戏和教学之间存在着密切的联系。整个中世纪的作家都谈到对话作为一种“教学”或“测试”合理推理的方式。我们至少有两本 16 世纪早期的逻辑教科书，将其呈现为个体学生的游戏，刘易斯·卡罗尔的《逻辑游戏》（1887 年）是同一类型的另一个例子。现代也有很多例子，尽管可能没有足够的连续性来证明通过游戏教授逻辑的传统。

数学博弈论始于 20 世纪初。虽然直到 1950 年代才出现与逻辑的数学联系，但令人惊讶的是，早期博弈论的先驱者中有很多人也以他们对逻辑的贡献而闻名：约翰·凯门尼，J. C. C. 麦金西，约翰·冯·诺伊曼，威拉德·奎因，朱莉娅·罗宾逊，恩斯特·策梅洛等等。1953 年，大卫·盖尔和弗兰克·斯图尔特在集合论和博弈论之间建立了有益的联系。不久之后，利昂·亨金提出了一种使用博弈论为无穷语言提供语义的方法。

二十世纪上半叶是逻辑学严谨性和专业性不断增强的时代，对于那个时期的大多数逻辑学家来说，在逻辑学中使用游戏可能会被认为是轻浮的。直觉主义者勒·E·J·布劳尔在指责对手将数学“堕落为一种游戏”时表达了这种态度（正如大卫·希尔伯特在 1927 年引用他所说的，引自范·海耶诺特 1967 年）。赫尔曼·韦尔（引自曼科苏 1998 年）使用游戏的概念来解释希尔伯特的元数学：数学证明就像毫无意义的游戏的进行，但我们可以站在游戏之外并对其提出有意义的问题。维特根斯坦的语言游戏对逻辑学家几乎没有引起什么反响。但是在二十世纪下半叶，逻辑研究的重心从基础转向技术，从大约 1960 年开始，游戏在逻辑论文中越来越常见。

到了二十一世纪初，人们普遍认可游戏和逻辑是相辅相成的。结果是逻辑和游戏的新组合大量涌现，尤其是在逻辑应用领域。其中许多新发展最初源于纯粹逻辑的研究，尽管如今它们有着自己的议程。一个这样的领域是论证理论，其中游戏成为分析辩论结构的工具。

下面我们将集中讨论与纯粹逻辑最密切相关的那些游戏。

2. 逻辑游戏

从博弈论的角度来看，逻辑学家研究的主要游戏并不典型。它们通常只涉及两个玩家，长度通常是无限的，唯一的结果是胜利和失败，并且行动或结果没有附加的概率。逻辑游戏的最基本要素如下。

有两个玩家。一般来说，我们可以称他们为 ∀ 和 ∃。发音“Abelard”和“Eloise”可以追溯到 20 世纪 80 年代中期，并且有助于将玩家定为男性和女性，使得引用更容易：她的回合，他的回合。在特定类型的逻辑游戏中，还有其他常用的玩家名称。

玩家通过选择一个称为游戏域 Ω 的集合的元素来进行游戏。当他们进行选择时，他们逐步构建起一个序列

a0,a1,a2,…

Ω 的元素。Ω 的元素的无限序列称为游戏。Ω 的元素的有限序列称为位置；它们记录了游戏在某个时间点可能达到的位置。一个函数 τ（回合函数或玩家函数）将每个位置 a 映射到 ∃ 或 ∀；如果 τ（a）=∃，这意味着当游戏达到位置 a 时，玩家 ∃ 会做出下一个选择（∀ 同理）。游戏规则定义了两个集合 W∀ 和 W∃，它们由位置和游戏组成，并具有以下特性：如果位置 a 在 W∀ 中，则以 a 开头的任何游戏或更长的位置也在其中（W∃ 同理）；并且没有游戏既在 W∀ 中又在 W∃ 中。我们说玩家 ∀ 赢得了游戏 b，并且 b 是 ∀ 的胜利，如果 b 在 W∀ 中；如果某个作为 b 的初始片段的位置 a 在 W∀ 中，则我们说玩家 ∀ 已经在 a 处获胜（∃ 和 W∃ 同理）。因此，总结起来，逻辑游戏是一个具有刚才描述的特性的四元组（Ω，τ，W∀，W∃）。

我们说一个逻辑游戏是完全的，如果每一次游戏都在 W∀ 或 W∃ 中，所以没有平局。除非有明确的例外，逻辑游戏总是被假定为完全的。（不要将完全与更强的决定性属性混淆-见下文。）

之所以在上述定义中期望游戏在某个有限位置上某个玩家获胜时继续无限进行，仅仅是为了数学上的方便；在玩家获胜后发生的任何事情都没有兴趣。许多逻辑游戏具有这样的特性，即在每一次游戏中，其中一个玩家已经在某个有限位置上获胜；这种游戏被称为良基的。更强的条件是存在某个有限数 n，使得在每一次游戏中，其中一个玩家已经在第 n 个位置上获胜；在这种情况下，我们说游戏具有有限长度。

对于一个玩家来说，策略是一组规则，准确描述了该玩家应该如何选择，这取决于两个玩家在之前的移动中的选择。在数学上，对于 ∀ 来说，策略由一个函数组成，该函数将每个位置 a（其中 τ(a)=∀）映射到 Ω 中的一个元素 b；我们认为这是对 ∀ 的一种指示，即当游戏达到位置 a 时，选择 b。（对于 ∃ 的策略也是如此。）如果一个玩家的策略在使用该策略的每一次游戏中都能获胜，无论对手做什么，那么该策略被称为获胜策略。最多只有一个玩家有获胜策略（否则玩家可以使用他们的获胜策略相互对抗，两者都会获胜，与 W∀ 和 W∃ 没有共同的游戏相矛盾）。偶尔会遇到一些情况，似乎两个玩家都有获胜策略（例如在下面的强制游戏中），但仔细检查后发现两个玩家实际上在玩不同的游戏。

一个游戏被称为是确定的，如果其中一方玩家有一个获胜策略。有许多游戏的例子是不确定的，正如盖尔和斯图尔特在 1953 年使用选择公理所证明的。这一发现导致了确定性概念在集合论基础中的重要应用（参见关于大基数和确定性的条目）。盖尔和斯图尔特还证明了一个以他们名字命名的重要定理：每个良基游戏都是确定的。由此可知，每个有限长度的游戏都是确定的——这个事实在 1913 年已经被策梅洛所知。（盖尔-斯图尔特定理的一个更精确的陈述是这样的。如果 ∃ 在 G 的每一次游戏中都没有在任何有限位置上输过，那么 G 被称为是封闭的。该定理表明每个封闭游戏都是确定的。该定理的证明基本上很容易：让我们称一个位置对于 ∀ 来说是获胜的，如果他从这个位置开始有一个获胜策略。假设 ∀ 在游戏中没有获胜策略，也就是说，在开始时，这个位置对于 ∀ 来说不是获胜的。如果第一步是 ∀ 的一步，在他的行动之后，这个位置对于他来说仍然不是获胜的。如果第一步是 ∃ 的一步，她必须有一步之后，这个位置对于 ∀ 来说仍然不是获胜的，否则之前的位置对于 ∀ 来说就是获胜的。游戏以这种方式无限进行下去，通过对于 ∀ 来说不是获胜的位置进行无数次的行动。由于游戏是封闭的，∃ 获胜。）

正如在经典博弈论中一样，上述逻辑游戏的定义充当了一个衣架，我们可以将其他概念挂在上面。例如，通常会有一些法则描述 Ω 中的哪些元素可以供玩家在特定移动时选择。严格来说，这种细化是不必要的，因为如果我们命令违反法律的玩家立即失败，那么获胜策略不会受到影响；但对于许多游戏来说，这种观察方式似乎不自然。下面我们将看到一些其他可以添加到游戏中的额外特性。

上述游戏和策略的定义纯粹是数学的。因此，它们忽略了游戏可能是最重要的特征，即人们玩游戏（至少是比喻性地）。玩家的目标是赢得游戏，并通过研究他们可以选择的策略，我们研究了对于一个具有特定目标的人来说什么行为是理性的。在大多数游戏中，有几个玩家，因此我们可以研究对他人行为的理性回应。通过限制玩家的移动和可能的策略，我们可以研究有限理性，即在信息、记忆或时间有限的条件下做出理性决策的代理人。

简而言之，游戏被用于建模理性和有限理性。这与逻辑的任何联系都是独立的。但是，一些逻辑学是为了研究理性行为的方面而设计的，近年来，将这些逻辑与适当的游戏联系起来变得越来越常见。请参阅第 5 节（“其他逻辑的语义游戏”）及其参考文献。

但直到最近，逻辑游戏与理性行为的联系方式完全不同。表面上，所讨论的逻辑与行为没有直接的联系。但逻辑学家和数学家注意到，如果将一些思想与可能的目标联系起来，它们可能会更加直观。例如，在许多逻辑游戏的应用中，中心概念是对玩家 ∃ 的获胜策略。通常这些策略（或其存在）被证明与某些逻辑上重要的东西等价，而这些东西本可以在不使用游戏的情况下定义，例如一个证明。但是游戏被认为给出了更好的定义，因为它们确实提供了一些动机：∃ 试图获胜。

这引出了一个在数学上并不太有趣的问题，但它应该引起使用逻辑游戏的哲学家们的关注。如果我们希望 ∃ 在游戏 G 中的动机具有任何解释价值，那么我们需要理解如果 ∃ 获胜会实现什么。特别是，我们应该能够讲述一个现实的情境故事，其中一个名为 ∃ 的代理人试图做一些可理解的事情，而做这件事情就等同于在游戏中获胜。正如理查德·道金斯在讨论梅纳德·史密斯的进化游戏时所说，

我们搜索的整个目的是发现一个适合扮演我们目的隐喻中主角的合适演员。我们希望能够说，“这是为了…的好处。”本章中我们的探索是为了找到完成那个句子的正确方式。（《扩展表型》，牛津大学出版社，1982 年牛津，第 91 页。）

为了将来参考，让我们称之为道金斯问题。在许多种逻辑游戏中，回答这个问题比这些游戏的先驱们意识到的要困难得多。（马里昂 2009 进一步讨论了道金斯问题。）

3. 经典逻辑的语义游戏

在 20 世纪 30 年代初，阿尔弗雷德·塔斯基提出了一个真理的定义。他的定义包括了一个典型形式理论语言中的句子为真的必要和充分条件；他的必要和充分条件仅使用了语法和集合论的概念，以及所讨论的形式理论的原始概念。事实上，塔斯基定义了更一般的关系“公式 ϕ(x1,...,xn) 对元素 a1,...,an 为真”；句子的真是 n=0 的特殊情况。例如，问题是是否

"对于所有的 x，存在 y 使得 R(x,y)成立" 是真的

归结为以下问题是否成立：

对于每个对象 a，句子 "存在 y 使得 R(a,y)成立" 是真的。

这反过来又减少到：

对于每个对象 a，都存在一个对象 b，使得句子“R(a,b)”为真。

在这个例子中，这就是塔斯基的真理定义所能带给我们的。

在 1950 年代末，利昂·亨金（Leon Henkin）注意到我们可以直观地理解一些无法通过塔斯基的定义处理的句子。例如，考虑无限长的句子

对于所有的 x0，存在一个 y0，使得对于所有的 x1，存在一个 y1，使得... R(x0,y0,x1,y1,...)。

塔斯基的方法失败是因为开头的量词串是无限的，我们永远无法去掉它们。相反，亨金建议我们应该考虑一个游戏，其中一个人 ∀ 选择一个对象 a0 作为 x0，然后第二个人 ∃ 选择一个对象 b0 作为 y0，然后 ∀ 选择 a1 作为 x1，∃ 选择 b1 作为 y1，依此类推。如果无限原子句是 ∃ 的胜利，则这个游戏的进行是 ∃ 的胜利。

R(a0,b0,a1,b1,…)

是真的。原始句子只有当玩家 ∃ 对这个游戏有一个获胜策略时才为真。严格来说，亨金只是将游戏作为一个隐喻，并且他提出的真实条件是该句子的斯科莱姆化版本为真，即存在函数 f0,f1,…使得对于每个选择的 a0,a1,a2 等，我们有

R(a0,f0(a0),a1,f1(a0,a1),a2,f2(a0,a1,a2),…)。

但是这个条件立即转化为游戏的语言；Skolem 函数 f0 等定义了 ∃ 的获胜策略，告诉她如何根据 ∀ 之前的选择来进行选择。（后来有人发现，C.S.皮尔斯已经建议用选择对象的方式来解释“每个”和“一些”之间的区别；例如，在他 1898 年的第二次剑桥会议演讲中。）

亨金的工作不久之后，雅科·欣蒂卡（Jaakko Hintikka）补充说，相同的思想也适用于合取和析取。我们可以将合取“ϕ∧ψ”视为一个普遍量化的陈述，表示“每个句子 ϕ，ψ 都成立”，因此对于 ∀ 来说，应该选择其中一个句子。正如欣蒂卡所说，要玩游戏 G(ϕ∧ψ)，∀ 选择游戏应该继续进行为 G(ϕ)还是 G(ψ)。同样，析取变成了关于句子集合的存在量化的陈述，并且它们标记了玩家 ∃ 选择游戏应该如何进行的移动。为了将量词引入相同的风格，他提出游戏 G(∀xϕ(x))的进行方式如下：玩家 ∀ 选择一个对象并为其提供一个名称 a，游戏继续进行为 G(ϕ(a))。（存在量词也是如此，只是 ∃ 进行选择。）欣蒂卡还对引入否定提出了一个巧妙的建议。每个游戏 G 都有一个对偶游戏，除了在玩游戏和获胜规则中，∀ 和 ∃ 的角色互换。游戏 G(¬ϕ)是 G(ϕ)的对偶。

人们可以证明，对于任何在固定结构 A 中解释的一阶句子 ϕ，玩家 ∃ 在 Hintikka 的游戏 G(ϕ)中有一个获胜策略，当且仅当 ϕ 在 Tarski 的意义下在 A 中为真。这个证明有两个有趣的特点。首先，如果 ϕ 是任意的一阶句子，那么游戏 G(ϕ)的长度是有限的，因此 Gale-Stewart 定理告诉我们它是确定的。我们推断出 ∃ 在 G(ϕ)和它的对偶中恰好有一个获胜策略；所以她在 G(¬ϕ)中有一个获胜策略当且仅当她在 G(ϕ)中没有一个。这解决了否定的问题。其次，如果 ∃ 对于每个游戏 G(ϕ(a))都有一个获胜策略，那么在选择每个 a 时，她可以将它们串联成一个对于 G(∀xϕ(x))的单一获胜策略（即，“等待并观察元素 a∀ 选择了什么，然后玩 fa”）。这解决了全称量词的问题；但这个论证使用了选择公理，事实上很容易看出 Hintikka 和 Tarski 关于真理定义的等价性本身等价于选择公理（在 Zermelo-Fraenkel 集合论的其他公理给定的情况下）。

令人困惑的是，我们在这里有两个关于句子何时为真的理论，而且如果选择公理失败，这些理论并不等价。实际上，原因并不是很深奥。选择公理之所以需要，并不是因为 Hintikka 的定义使用了游戏，而是因为它假设策略是确定性的，即它们是给用户没有选择选项的单值函数。将 Tarski 的定义更自然地转化为游戏术语的方法是使用非确定性策略，有时称为准策略（详见 Kolaitis 1985）。（然而，Hintikka 1996 坚持认为“真”的正确阐释是使用确定性策略的阐释，并且这个事实证明了选择公理的正确性。）

Hintikka 的计算机实现游戏证明是教授一阶句子意义的非常有效的方式。斯坦福大学的 Jon Barwise 和 John Etchemendy 设计了一个名为“Tarski's World”的软件包。独立地，Omsk 大学的另一个团队构建了一个俄语版本，供天才儿童学校使用。

在 Hintikka 于 1973 年在牛津大学发表的约翰·洛克讲座的版本中，他提出了 Dawkins 问题（见上文）关于这些游戏。他的答案是应该参考维特根斯坦的语言游戏，而理解量词的语言游戏是围绕寻找和发现展开的。在相应的逻辑游戏中，应该将 ∃ 视为自己，将 ∀ 视为一个不可靠的自然界，永远不能依赖它来呈现我想要的对象；所以为了确保找到它，我需要一个获胜的策略。这个故事从来没有令人信服过；自然界的动机是无关紧要的，逻辑游戏中没有任何与寻找相对应的内容。回顾起来，没有人费心去寻找一个更好的故事，有点令人失望。更有帮助的是将在 G(ϕ)中 ∃ 的获胜策略视为一种证明（在适当的无穷系统中），证明 ϕ 是真的。

后来，Jaakko Hintikka 在两个方向上扩展了本节的思想，即自然语言语义和不完全信息游戏（见下一节）。Game-Theoretic Semantics（简称 GTS）这个名字已经被用来涵盖这两个扩展。

本节中描述的游戏几乎可以轻松地适应多分类逻辑：例如，量词 ∀xσ，其中 xσ 是一个属于 σ 类别的变量，是给玩家 ∀ 选择一个属于 σ 类别的元素的指令。这立即给我们提供了相应的二阶逻辑游戏，如果我们将结构的元素视为一种类别，元素集合视为第二种类别，二元关系视为第三种类别，依此类推。由此可见，我们也可以很常规地为大多数广义量词制定游戏规则；我们可以通过首先将广义量词翻译成二阶逻辑来找到它们。

4. 带有不完全信息的语义游戏

在本节和下一节中，我们将研究将前一节的语义游戏适应到其他逻辑的一些改编。在我们的第一个例子中，逻辑（Hintikka 和 Sandu 1997 年的独立友好逻辑，或简称为 IF 逻辑）是为了适应游戏而创建的。请参阅关于独立友好逻辑和 Mann，Sandu 和 Sevenster 2011 年的更详细介绍。

这里的游戏与前一节中的游戏相同，只是我们放弃了每个玩家都知道先前游戏历史的假设。例如，我们可以要求玩家在某些早期移动时做出选择，而不知道其他玩家在这些移动中做出了什么选择。在博弈论中处理这种情况的经典方法是对玩家的策略进行限制。例如，我们可以要求策略函数告诉 ∃ 在特定步骤上该做什么，这个函数的定义域是 ∀ 在他的第一和第二步可能选择的家族；这是一种表达 ∃ 不知道 ∀ 在他的第三步和以后的移动中选择了什么的方式。对策略函数施加这种限制的游戏被称为不完全信息的游戏，与前一节中的完全信息游戏相对。

为了构建适应这些游戏的逻辑，我们使用与前一节相同的一阶语言，只是在某些量词（可能还有一些联结词）上添加了一种符号，以显示这些量词（或联结词）的斯科莱姆函数与某些变量无关。例如，句子

(∀x)(∃y/∀x)R(x,y)

被读作：“对于每个 x，存在一个 y，不依赖于 x，使得 R(x,y)成立”。

关于完全信息和不完全信息之间的区别，有三个重要的评论要提出。首先，Gale-Stewart 定理仅适用于完全信息的游戏。例如，假设 ∀ 和 ∃ 玩以下游戏。首先，∀ 选择 0 和 1 中的一个数字。然后，∃ 选择这两个数字中的一个。如果所选数字相同，则玩家 ∃ 获胜，否则玩家 ∀ 获胜。我们要求 ∃ 在做出选择时不知道 ∀ 选择了什么；因此，对于她来说，一个 Skolem 函数将是一个常数。（这个游戏对应于上面的 IF 句子，其中 R 被解释为相等，在一个由 0 和 1 组成的结构中。）很明显，玩家 ∃ 没有一个恒定的获胜策略，而且玩家 ∀ 根本没有获胜策略。因此，这个游戏是不确定的，尽管它的长度只有 2。

一个推论是 Hintikka 将否定解释为对偶（‘玩家交换位置’）的理由，在他的一阶逻辑游戏中，并不适用于 IF 逻辑。Hintikka 的回应是，对偶在一阶情况下是否定的正确直观含义，因此不需要理由。

第二个评论是，即使在完全信息的游戏中，获胜策略也可能不使用所有可用的信息。例如，在完全信息的游戏中，如果 ∃ 玩家有一种获胜策略，那么她也有一种获胜策略，其中策略函数仅依赖于 ∀ 之前的选择。这是因为她可以使用先前的策略函数重构自己的先前移动。

当 Hintikka 在他的一阶逻辑游戏中使用 Skolem 函数作为策略时，他使一个玩家的策略仅依赖于另一个玩家的先前移动。（∃ 的 Skolem 函数仅依赖于全称量化的变量。）由于这些游戏是完全信息的游戏，因此根据上述第二个评论，这并没有损失。但是当他转向 IF 逻辑时，策略仅依赖于另一个玩家的移动的要求确实产生了影响。Hodges 1997 通过修订符号表示法来展示这一点，例如(∃y/x)的意思是：“存在 y 与 x 无关，无论哪个玩家选择了 x”。

现在考虑以下句子

(∀x)(∃z)(∃y/x)(x=y),

在一个由 0 和 1 两个元素构成的结构上再次进行游戏。玩家 ∃ 可以通过以下方式获胜。对于 z，她选择与玩家 ∀ 为 x 选择的相同；然后对于 y，她选择与她为 z 选择的相同。这种获胜策略之所以有效，仅仅是因为在这个游戏中，∃ 可以参照她自己之前的选择。如果第三个量词是(∃y/xz)，她将没有获胜策略，因为这个量词的任何 Skolem 函数都必须是常数。∃ 通过参照她之前的选择向自己传递信息的方式是信号传递现象的一个例子。约翰·冯·诺伊曼和奥斯卡·莫根斯特恩用桥牌的例子来说明这一点，其中一个单个玩家由两个合作伙伴组成，他们必须通过使用公开的动作向对方发送信号来共享信息。

第三个评论是，关于不完全信息的直观概念与博弈论中关于策略的定义之间存在错位。直观上，不完全信息是关于游戏进行的环境的事实，而不是关于策略的事实。这是一个非常棘手的问题，并且它继续导致对 IF 和类似逻辑的误解。例如，考虑以下句子。

(∃x)(∃y/x)(x=y),

再次在一个由元素 0 和 1 构成的结构上进行游戏。直观上，人们可能会认为如果 ∃ 在第二个量词中不允许记住她在第一个量词中选择的内容，那么她几乎不可能有一个获胜的策略。但实际上，她有一个非常简单的策略：“总是选择 0”！

与一阶逻辑相比，IF 逻辑缺少了游戏语义无法提供的一个组成部分。游戏语义告诉我们一个句子在一个结构中是真的时候。但是，如果我们拿一个带有 n 个自由变量的公式，这个公式对结构的有序 n 元素元组表示了什么？在一阶逻辑中，它将定义一个集合，即结构上的一个 n 元关系；Tarski 的真值定义解释了这一点。IF 逻辑的任意公式是否有类似的定义？事实证明，Hodges 1997 引入的略有不同的逻辑有一个这样的定义，并且它导致了该逻辑语言的类似 Tarski 的真值定义。稍加调整，这个真值定义也可以适用于 IF 逻辑。但是对于这两种新逻辑，有一个问题：我们不再说一个元素分配给自由变量时一个公式是真的，而是说一组元素分配给自由变量时一个公式是真的。Väänänen 2007 将这个想法作为研究依赖概念的一系列新逻辑的基础（参见关于依赖逻辑的条目）。在这些逻辑中，语义是在没有游戏的情况下定义的，尽管最初的灵感来自 Hintikka 和 Sandu 的工作。

在 Väänänen 的逻辑学中，很容易看出为什么需要一组赋值。他有一个原子公式表达“x 依赖于 y”。我们如何在一个结构中解释这个问题，例如自然数的结构？询问例如 8 是否依赖于 37 根本没有意义。但是，如果我们有一个自然数有序对的集合 X，询问在 X 中每对的第一个成员是否依赖于第二个成员是有意义的；回答是肯定的意味着存在一个函数 f，使得 X 中的每对(a,b)具有形式(f(b),b)。

5. 其他逻辑的语义游戏

下面这种结构引发了有趣的游戏。结构 A 由一组元素 S（我们称之为状态，补充说明它们通常被称为世界）、S 上的二元关系 R（我们将其读作箭头）和 S 的子集 P1，…，Pn 的家族组成。两个玩家 ∀ 和 ∃ 在 A 上进行游戏 G，从给定的状态 s 开始，通过阅读适当的逻辑公式 ϕ 作为一组游戏和获胜指令。

因此，如果 ϕ 是 Pi，那么如果 s 在 Pi 中，玩家 ∃ 立即获胜，否则玩家 ∀ 立即获胜。公式 ψ∧θ、ψ∨θ 和 ¬ψ 的行为与 Hintikka 的游戏中的行为相同；例如，ψ∧θ 指示玩家 ∀ 选择游戏是按照 ψ 还是按照 θ 继续。如果公式 ϕ 是 □ψ，那么玩家 ∀ 从 s 到状态 t 选择一个箭头（即一个使得对偶(s,t)在关系 R 中的状态 t），然后根据指示 ψ 从状态 t 继续进行游戏。◊ψ 的规则相同，只是玩家 ∃ 做出选择。最后，我们说公式 ϕ 在 A 中的 s 处为真，如果玩家 ∃ 在基于 ϕ 并从 s 开始的游戏中有一个获胜策略。

这些游戏与模态逻辑的关系与 Hintikka 的游戏与一阶逻辑的关系非常相似。特别是它们是给模态逻辑提供语义的一种方式，并且与通常的 Kripke 类型语义一致。当然，模态逻辑有许多类型和推广（包括与之密切相关的逻辑，如时间、认知和动态逻辑），因此相应的游戏有许多不同的形式。一个有趣的例子是 Matthew Hennessy 和 Robin Milner 的计算机理论逻辑，用于描述系统的行为；在这里，箭头有多种颜色，沿着特定颜色的箭头移动表示执行特定的“动作”以改变状态。另一个例子是 Dexter Kozen 的更强大的模态 μ-演算，它具有固定点运算符；参见 Stirling 2001 的第 5 章。

这些游戏的一个有趣特点是，如果某个玩家从某个位置开始具有获胜策略，那么该策略永远不需要参考先前发生的任何事情。先前做出的选择或者已经进行了多少步都是无关紧要的。因此，我们有时称之为“无记忆”获胜策略。

在 Rohit Parikh 提出的相关“游戏逻辑”中，将我们在状态之间移动的游戏作为主题，而不是给出真实定义的一种方式。这些游戏有许多有趣的方面。2003 年，《逻辑研究》杂志发表了一期专门讨论这些游戏的问题，由 Marc Pauly 和 Parikh 编辑。

经济学和计算机科学的影响导致许多逻辑学家使用逻辑来分析在部分无知条件下的决策制定。（例如，参见关于认识逻辑的文章。）有几种表示知识状态的方法。一种方法是将它们作为我们在本节开头提到的那种模态结构中的状态或世界。另一种方法是使用 IF 逻辑或其变体。这些方法之间有什么关系？Johan van Benthem 2006 年提出了一些关于这个非常自然的问题的思考和结果。还可以参考 Johan van Benthem、Krister Segerberg、Eric Pacuit 和 K. Venkatesh 的论文以及他们在 Van Benthem、Gupta 和 Parikh 2011 年的第四部分“逻辑、机构和游戏”中的参考文献，以及关于分析游戏逻辑的条目，了解这一领域最近的研究工作的样本。

6. 前后游戏

1930 年，阿尔弗雷德·塔斯基提出了两个结构 A 和 B 在元素上等价的概念，即在 A 中真实的一阶句子与在 B 中真实的一阶句子完全相同。在 1946 年普林斯顿的一次会议上，他描述了这个概念，并表达了希望能够发展一个与“同构等概念一样深入”的理论的希望（塔斯基 1946）。

这样一个理论的一个自然部分将是两个结构在元素上等价的纯粹结构上的必要和充分条件。法国-阿尔及利亚人罗兰·弗雷塞是第一个找到可用的必要和充分条件的人。几年后，哈萨克斯坦逻辑学家 A·D·泰曼诺夫重新发现了这个条件，并由波兰逻辑学家安德烈·埃伦福特以游戏的形式重新表述。这些游戏现在被称为埃伦福特-弗雷塞游戏，有时也被称为来回游戏。它们被证明是 20 世纪逻辑学中最多才多艺的思想之一。它们适应广泛的逻辑和结构。

在来回游戏中，有两个结构 A 和 B，以及两个常被称为 Spoiler 和 Duplicator 的玩家。（这些名称是由乔尔·斯宾塞在 1990 年代早期提出的。最近尼尔·伊默曼提出了使用相同首字母的 Samson 和 Delilah，将 Spoiler 定为男性玩家 ∀，Duplicator 定为女性玩家 ∃。）游戏中的每一步由 Spoiler 的一次移动，然后是 Duplicator 的一次移动组成。Spoiler 选择两个结构中的一个元素，然后 Duplicator 必须选择另一个结构中的一个元素。因此，在 n 步之后，从 A 中选择了一个序列，从 B 中选择了一个序列：

(a0,…,an−1; b0,…,bn−1).

如果且仅如果某个原子公式（形式为“R(v0,…,vk−1)”或“F(v0,…,vk−1)=vk”或“v0=v1”，或者这些公式中的一个，但变量不同）在 A 中由(a0,…,an−1)满足但在 B 中由(b0,…,bn−1)不满足，或者反之，则此位置对 Spoiler 来说是胜利的。Duplicator 获胜的条件在游戏的不同形式中是不同的。在最简单的形式 EF(A,B)中，如果游戏的任何初始部分都不是 Spoiler 的胜利（即如果她在任何有限阶段都没有输），则对 Duplicator 来说，一次游戏是胜利的。对于每个自然数 m，都存在一个游戏 EFm(A,B)；在这个游戏中，如果 Duplicator 在 m 步之后仍未输掉，她就获胜。根据 Gale-Stewart 定理，所有这些游戏都是确定的。如果 Duplicator 在 EF(A,B)上有一个获胜策略，则称结构 A 和 B 是来回等价的；如果她在 EFm(A,B)上有一个获胜策略，则称它们是 m-等价的。

可以证明，如果对于每个自然数 m，A 和 B 都是 m-等价的，则它们是元等价的。实际上，如果 Eloise 在 A 上的 Hintikka 游戏 G(ϕ)中的量词嵌套的层次最多为 m 级时有一个获胜策略 τ，而 Duplicator 在游戏 EFm(A,B)中有一个获胜策略 ϱ，则策略 τ 和 ϱ 可以组合成 Eloise 在 B 上的 G(ϕ)中的一个获胜策略。另一方面，EFm(A,B)中的 Spoiler 的获胜策略可以转化为一个一阶句子，该句子在 A 和 B 中恰好有一个为真，并且量词嵌套的层次最多为 m 级。因此，我们得到了元等价的必要和充分条件，以及更多的内容。

如果 A 和 B 是来回等价的，那么它们肯定是元等价的；但实际上，在比一阶逻辑更具表达力的无穷逻辑中，来回等价事实上等同于元等价。有许多游戏的调整可以得到其他类型的等价。例如，Barwise、Immerman 和 Bruno Poizat 独立地描述了一个游戏，在这个游戏中，两个玩家每个都有 p 个编号的小石子；每个玩家必须用一个小石子标记他或她的选择，并且在同一步中的两个选择必须用带有相同编号的小石子标记。随着游戏的进行，玩家们会用完小石子，因此他们将不得不重新使用已经使用过的小石子。在这个游戏中，Spoiler 在一个位置（以及所有后续位置）获胜的条件与之前相同，只是只计算该位置上带有标签的元素。在这个游戏中，Duplicator 存在一种获胜策略意味着这两个结构在使用最多 p 个变量的句子中达成一致（允许这些变量出现任意次数）。

背对背游戏背后的理论对所讨论的逻辑学做出了很少的假设。因此，这些游戏是少数既适用于有限结构又适用于无限结构的模型论技术之一，这使它们成为理论计算机科学的基石之一。人们可以使用它们来衡量形式语言的表达能力，例如数据库查询语言。一个典型的结果可能会说，某种语言无法区分“偶数”和“奇数”；我们可以通过找到对于该语言的复杂性公式的每个级别 n，Duplicator 在级别 n 的背对背游戏中都有一种获胜策略的一对有限结构来证明这一点，但其中一个结构具有偶数个元素，而另一个结构具有奇数个元素。自然语言的语义学家发现背对背游戏对比较广义量词的表达能力非常有用（例如参见 Peters 和 Westerståhl 2006 第 IV 节）。

在与我们上面的模态语义相对应的同时，还有一种来回游戏，就像 Ehrenfeucht-Fraïssé 游戏对应于 Hintikka 的一阶逻辑游戏语义一样。玩家从结构 A 中的状态 s 和结构 B 中的状态 t 开始。Spoiler 和 Duplicator 交替移动，就像以前一样。每次移动时，Spoiler 选择是在 A 中移动还是在 B 中移动，然后 Duplicator 必须在另一个结构中移动。移动总是通过沿着当前状态的箭头向前进行。如果两个玩家刚刚移动到 A 中的状态 s´ 和 B 中的状态 t´，并且某个谓词 Pi 仅在 s´ 和 t´ 中的一个状态上成立，则 Duplicator 立即失败。如果没有可用的箭头供 Duplicator 移动，她也会失败；但是如果 Spoiler 发现在任一结构中都没有可用的箭头供他移动，那么 Duplicator 获胜。如果两个玩家在给定的起始状态 s 在 A 中和 t 在 B 中玩这个游戏，并且两个结构只有有限多个状态，那么可以证明 Duplicator 只有在 A 中的 s 和 B 中的 t 上真的模态句子与真的模态句子相同的情况下才有获胜策略。

这个结果有许多推广，其中一些涉及以下概念。设 Z 是将 A 的状态与 B 的状态相关联的二元关系。如果 Duplicator 可以在 A 和 B 之间的来回游戏中使用 Z 作为非确定性的获胜策略，其中两个玩家的第一对移动是选择他们的起始状态，则我们称 Z 为 A 和 B 之间的双模拟关系。在计算机科学中，双模拟的概念对于理解 A 和 B 作为系统的方式至关重要；它表达了两个系统与其环境以相同的方式交互，一步一步。但是在计算机科学家引入这个概念之前，基本上相同的概念在 Johan van Benthem 的关于模态逻辑语义的博士论文（1976 年）中出现。

7. 其他模型论游戏

本节中的逻辑游戏是数学家的工具，但它们具有一些概念上有趣的特点。

7.1 强制游戏

强制游戏在描述集合论中也被称为 Banach-Mazur 游戏；有关数学背景的更多细节，请参阅 Kechris 或 Oxtoby 的参考文献。模型论者使用它们来构建具有受控属性的无限结构。在最简单的情况下，∀ 和 ∃ 进行所谓的模型存在游戏，其中 ∃ 声称一个固定的句子 ϕ 有一个模型，而 ∀ 声称他可以从 ϕ 中推导出一个矛盾。一开始，固定了一个可数无穷集 C 的新常量符号 a0，a1，a2 等。∃ 通过选择一个析取式的一个分支来捍卫一个析取式，并通过选择 C 中的一个常量作为证人来捍卫一个存在性陈述。∀ 可以通过选择任一合取式来挑战一个合取式，并通过选择 C 中的任意证人来挑战一个普遍陈述。如果没有出现矛盾的原子句，则 ∃ 获胜。∃ 有一个获胜策略（一致性属性是描述获胜策略的一种方式），当且仅当 ϕ 有一个模型。另一方面，如果 ∀ 有一个获胜策略，则针对他的获胜策略的所有对局（可以使其有限）与 ϕ 的否定的 Gentzen 风格证明相关。这种分析句子的方法与 Beth 的语义表和对话游戏（见第 8 节）密切相关。

为了勾勒出一般的游戏理论的思想，想象一下一个无限可数的建筑团队正在建造一个房子 A。每个建筑工人都有自己的任务要完成：例如安装浴缸或者给入口大厅贴壁纸。每个建筑工人都有无限次机会进入工地，并向房子添加一些有限的材料；这些建筑工人的时间安排是交错的，整个过程按照自然数计数的步骤进行。

为了证明房子可以按照要求建造，我们需要证明每个建筑工人都可以独立完成自己的指定任务，而不受其他建筑工人的影响。因此，我们将每个建筑工人想象成为 ∃ 在游戏中的玩家，而其他所有玩家则被归为 ∀，我们的目标是证明 ∃ 在这个游戏中有一个获胜策略。当我们分别为每个建筑工人证明了这一点之后，我们可以想象他们按照自己的获胜策略开始工作。他们都赢得了各自的游戏，结果就是一个漂亮的房子。

更具技术性地说，结构 A 的元素事先固定，比如说 a0、a1、a2 等等，但是这些元素的属性必须通过游戏来确定。每个玩家通过投入一组关于元素的原子或否定原子陈述来进行移动，只要这些投入的陈述集合与游戏之前写下的一组固定公理一致即可。（因此，投入一个否定原子句 ¬ϕ 的效果是阻止任何玩家在后期添加 ϕ。）在联合游戏结束时，投入的原子句集合具有一个规范模型，这就是结构 A；有办法确保它是一组固定公理的模型。如果给定一个使 P 在 A 中为真的任务，那么 P 是可强制执行的，如果一个建造者有一个获胜策略。一个中心观点（基本上是由 Ehrenfeucht 提出的）是，可强制执行的属性的可数无穷集合的合取仍然是可强制执行的。

模型论的各种 Löwenheim-Skolem 定理可以使用 Forcing Game 的变体来证明。在这些变体中，我们不是构造一个模型，而是给定模型的子模型。我们从一个句子（或一个可数的句子集）ϕ 的大模型 M 开始。然后我们列出 ϕ 的子公式，每个玩家都有一个带有自由变量的子公式要处理。玩家的任务是确保一旦子公式的参数在游戏中出现，并且在大模型中有一个公式的真实证明，就会播放一个这样的证明。当游戏结束时，一个可数的 M 的子模型已经被构建，以满足 ϕ。

“强制”这个名字来自于保罗·科恩在 20 世纪 60 年代初构建集合论模型时相关思想的应用。亚伯拉罕·罗宾逊将其改编为一种构建可数结构的通用方法，马丁·齐格勒引入了游戏设置。后来，罗宾·赫什和伊恩·霍金森使用相关游戏解决了一些关于关系代数的旧问题。

强制游戏是考虑道金斯问题时要牢记的一个良好例子。它们提醒我们，在逻辑游戏中，将玩家视为相互对立并不一定有助于解决问题。

7.2 切割和选择游戏

在传统的切割和选择游戏中，你拿一块蛋糕并将其切成两个较小的部分；然后我选择其中一块并吃掉它，留下另一块给你。这个过程被认为会对你施加公平切割蛋糕的压力。数学家们并不完全理解这个练习的目的，坚持要进行迭代。因此，我让你将我选择的那块切成两块，然后我再选择其中一块；然后你再次切割这块，如此无限循环。一些更加超凡脱俗的数学家甚至让你将蛋糕切成可数多块，而不是两块。

这些游戏在定义理论中非常重要。假设我们有一个对象集合 A 和一个属性家族 S；每个属性将 A 划分为具有该属性和不具有该属性的对象集合。让 ∃ 从整个集合 A 开始，使用 S 中的一个属性作为刀子进行切割；让 ∀ 选择其中一块（它们是 A 的子集）并将其交还给 ∃ 再次切割，再次使用 S 中的一个属性；如此循环。让 ∃ 在 ∀ 选择一个空的部分时输掉比赛。我们说，如果 ∀ 有一种策略可以确保 ∃ 在她的第 m 次行动之前输掉，那么（A，S）的等级至多为 m。（A，S）的等级提供了关于由 S 中的属性定义的 A 的子集家族的有价值的信息。

这个游戏的变体，允许将一个棋子切割成无限多个更小的棋子，是模型论中称为稳定性理论的一个基础。广义上说，一个理论在稳定性理论的意义上是“好的”，如果我们取一个理论的模型 A 和一阶公式集 S，其中的自由变量带有来自 A 的参数，那么结构(A,S)的“秩”是“小”的。另一种变体是要求在每一步中，∃ 将之前的每个存活的棋子切割成两个，而且只要有一个切割碎片为空，她就输了。（在这个版本中，∀ 是多余的。）在这种变体中，(A,S)的秩被称为它的 Vapnik-Chervonenkis 维度；这个概念在计算学习理论中被使用。

7.3 两个后继函数树上的游戏

想象一个树，它是逐层构建起来的。在底层有一个单独的根节点，但是从它分别出来一个左分支和一个右分支。在上一层有两个节点，每个分支上有一个节点，并且从每个节点分别生长出一个左分支和一个右分支。所以在上一层有四个节点，并且树在每个节点处再次分成左右两个分支。继续到无穷远，这个树被称为两个后继函数树（即左后继和右后继）。将节点作为元素，并引入左后继和右后继的两个函数符号，我们就有了一个结构。Michael Rabin 的一个强大定理表明，存在一个算法，对于这个结构适用的每个单调二阶句子 ϕ，它将告诉我们 ϕ 在结构中是否为真。（“单调二阶”意味着逻辑类似于一阶逻辑，除了我们还可以量化元素集合，但不能量化元素之间的二元关系，例如。）

Rabin 的定理有许多有用的结果。例如，Dov Gabbay 用它来证明了一些模态逻辑的可决定性。但是 Rabin 的证明，使用自动机，被公认为难以理解。Yuri Gurevich 和 Leo Harrington 以及独立的 Andrei Muchnik 在其中自动机是游戏中的一个玩家的证明中找到了简单得多的证明。

Rabin 的这个结果是将游戏与自动机联系起来的几个有影响力的结果之一。另一个例子是用于验证模态系统属性的奇偶游戏。例如，参见 Stirling（2001）第 6 章；Bradfield 和 Stirling（2006）讨论了模态 μ-演算的奇偶游戏。

8. 对话、交流和证明的游戏

几本中世纪的文本描述了一种被称为 obligationes 的辩论形式。有两个辩论者，Opponens 和 Respondens。在会议开始时，辩论者们会就一个“positum”达成一致，通常是一个错误的陈述。Respondens 的工作是根据 Opponens 的问题给出合理的答案，假设 positum 是真的；最重要的是，他必须避免不必要地自相矛盾。Opponens 的工作是试图迫使 Respondens 陷入矛盾。所以我们大致知道对于 Dawkins 的问题的答案，但我们不知道游戏规则！中世纪的教科书确实描述了辩论者应该遵循的几条规则。但这些规则不是游戏的规定规则；它们是教科书从合理推理原则和示例的帮助下推导出来的指导方针。（威尼斯的保罗通过“伟大的逻辑学家、哲学家、几何学家和神学家”的实践来证明一条规则。）特别是，obligationes 的教师有权发现新的规则。这种开放性意味着 obligationes 不是我们所理解的逻辑游戏。

并非每个人都同意前面的观点。例如，Catarina Dutilh Novaes（2007 年，6 页）详细阐述了 obligationes 呈现“中世纪和现代理论框架之间概念相似性的一个显著案例”的观点。但无论我们对这个问题持什么观点，这些辩论都激发了逻辑游戏领域的一条重要研究线索。

想象一下在证明论的口试中进行 ∃。考官给她一个句子，并邀请她开始证明。如果句子的形式为

ϕ∨ψ

那么她有权选择其中一句话并说：“好的，我将证明这个。”（实际上，如果考官是直觉主义者，他可能会坚持要求她选择其中一句话来证明。）另一方面，如果这句话是

ϕ∧ψ

那么，作为一个考官，作为一个考官，他可能会选择其中一个连词，并邀请她证明其中一个。如果她知道如何证明这个连词，那么她肯定知道如何证明这个连词。

ϕ→ψ 的情况有点微妙。她可能会想从假设 ϕ 开始，以推导出 ψ；但是有一些混淆的风险，因为到目前为止她写下的句子都是需要证明的事情，而 ϕ 不是需要证明的事情。考官可以通过说“我假设 ϕ，让我们看看你能否从那里得到 ψ”来帮助她。此时，她有可能通过从 ϕ 中推导出矛盾来找到得到 ψ 的方法；因此，她可能会反过来要求考官展示他的假设是一致的，以证明它不是一致的。对称性并不完美：他要求她展示一个句子在任何地方都是真实的，而她邀请他展示一个句子在某个地方是真实的。尽管如此，我们可以看到某种形式的对偶。

这种思想是保罗·洛伦岑辩证游戏的基础。他证明了通过一定程度的推动和推挤，可以为游戏编写规则，这些规则具有这样的特性：如果她在开始时被呈现的句子是直觉逻辑的定理，则 ∃ 具有获胜策略。向中世纪辩论致敬，他称 ∃ 为提出者，另一位玩家为反对者。几乎与中世纪的义务相同，反对者通过将提出者逼到只能进行明显的自相矛盾的地步来获胜。

Lorenzen 声称他的游戏为直觉主义和经典逻辑提供了理论依据（或者用他的话说，使它们“gerechtfertigt”，Lorenzen（1961,196））。不幸的是，任何“理论依据”都需要对 Dawkins 问题给出令人信服的答案，而 Lorenzen 从未提供过。例如，他将移动称为“攻击”，即使（就像上面的 ϕ∧ψ 的选择）它们看起来更像是帮助而不是敌意。

有关 Lorenzen 的游戏以及一些较新的变体的更详细解释，请参阅对话逻辑的条目。在其目前的形式（2013 年 1 月），它回避了 Lorenzen 关于证明逻辑的主张。相反，它将这些游戏描述为为逻辑提供语义（这一点 Lorenzen 肯定会同意的），并补充说，为了理解逻辑之间的差异，比较它们的语义可能会有所帮助。

从这个角度来看，洛伦岑的游戏是最近证明理论学家所称的证明语义的重要范例。证明语义不仅给出了“可证明”这个概念的“意义”，还给出了证明中每一步的“意义”。它回答了这样一个问题：“通过在证明中进行这一特定的步骤，我们实现了什么？”在 20 世纪 90 年代，一些计算机科学领域的研究人员寻找了一些与线性逻辑和其他一些证明系统类似的游戏，就像洛伦岑的游戏与直觉主义逻辑类似一样。安德烈亚斯·布拉斯，然后是萨姆森·阿布拉姆斯基和同事们，提出了与线性逻辑的部分对应的游戏，但在撰写本文时，我们还没有完美的游戏与逻辑之间的对应关系。这个例子特别有趣，因为对道金斯的问题的回答应该给出线性逻辑定律的直观解释，这是这种逻辑急需的。阿布拉姆斯基等人的游戏讲述了两个相互作用的系统的故事。但是，尽管他最初使用的是玩家有礼貌轮流行动的游戏，但后来阿布拉姆斯基允许玩家“以分布式、异步的方式”行动，只有在他们选择时才注意到对方。这些游戏不再符合逻辑游戏的正常格式，它们的现实生活解释引发了一系列新问题。

乔治·贾帕里泽提出了一种用于研究计算的“可计算逻辑”。它的语法是一阶逻辑，带有一些类似于线性逻辑的额外项目。它的语义是基于具有一些不寻常特征的语义游戏。例如，并不总是确定哪个玩家下一步行动。策略函数的概念已不再足以描述玩家；相反，贾帕里泽描述了将第二个玩家（在我们的符号中为 ∃）视为一种计算机的方式。更多信息请参见他的网站。

Lorenzen 的另一组与之相同的一般家族的游戏是 Pavel Pudlak 2000 的证明游戏。在这里，对手（称为证明人）扮演法庭上的律师的角色，他知道提出者（称为对手）犯了某种罪行。对手将坚持他是无辜的，并准备撒谎来为自己辩护。对手的目标是迫使提出者与提出者此前说过的某些话相矛盾；但对手保留记录（如上所述的鹅卵石游戏），有时由于空间或记忆不足，他必须从记录中删除项目。重要的问题不是对手是否有获胜策略（从一开始就假设他有一个），而是他需要多少内存来记录。这些游戏是用来显示各种证明系统中证明长度的上下界的有用工具。

允许撒谎的另一种逻辑游戏是 Ulam 的谎言游戏。在这里，一个玩家在给定范围内想一个数字。第二个玩家的目标是通过向第一个玩家提问是/否问题来找出那个数字；但第一个玩家被允许在回答中说一定数量的谎言。与 Pudlak 的游戏一样，第二个玩家肯定有一个获胜策略，但问题是他必须付出多大努力才能获胜。这次的衡量标准不是空间或记忆，而是时间：他需要问多少个问题？Cignoli 等人在 2000 年的第 5 章将这个游戏与多值逻辑联系起来。

暂时回到洛伦岑：他未能区分一个人在争论中可能采取的不同立场：陈述、假设、让步、质疑、攻击、承诺。是否真的可能在不预设某种逻辑的情况下定义所有这些概念，这是一个有争议的问题。但不要紧；在这些方面对洛伦岑游戏的改进可以作为对非正式逻辑的一种方法，特别是对旨在系统化合理非正式论证可能结构的研究。在这方面，请参阅沃尔顿和克拉贝（1995）的研究。Bench-Capon 和 Dunne（2007）的论文也是相关的。

Bibliography

Some of the seminal papers by Henkin and Lorenzen, and some of the papers cited below, appear in the collection Infinitistic Methods (Proceedings of the Symposium on Foundations of Mathematics, Warsaw, 2–9 September, 1959), Oxford: Pergamon Press, 1961. The editors are unnamed.

Games in the History of Logic

Dutilh Novaes, Catarina, 2007, Formalizing Medieval Logical Theories: Suppositio, Consequentiae and Obligationes, New York: Springer-Verlag.
Hamblin, Charles, 1970, Fallacies, London: Methuen.
Hilbert, David, 1967, “Die Grundlagen der Mathematik”, translated as “The foundations of mathematics,” in Jean van Heijenoort (ed.), From Frege to Gödel, Cambridge Mass.: Harvard University Press, pp. 464–479.
Paul of Venice, Logica Magna II (8), Tractatus de Obligationibus, E. Jennifer Ashworth (ed.), New York: British Academy and Oxford University Press, 1988.
Weyl, Hermann, 1925–7, “Die heutige Erkenntnislage in der Mathematik,”, translated as “The current epistemological situation in mathematics” in Paolo Mancosu, From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920s, New York: Oxford University Press, 1988, pp. 123–142.
Zermelo, Ernst, 1913, “Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels,” in E. W. Hobson and A. E. H. Love (eds.), Proceedings of the Fifth International Congress of Mathematicians, Volume II, Cambridge: Cambridge University Press.

Games for Teaching Logic

Barwise, Jon and John Etchemendy, 1995, The Language of First-Order Logic, including Tarski’s World 3.0, Cambridge: Cambridge University Press.
Carroll, Lewis, 1887, The Game of Logic, London: Macmillan.
Dienes, Zoltan P., and E. W. Golding, 1966, Learning Logic, Logical Games, Harlow: Educational Supply Association.
Havas, Katalin, 1999, “Learning to think: Logic for children,” in Proceedings of the Twentieth World Congress of Philosophy (Volume 3: Philosophy of Education), David M. Steiner (ed.), Bowling Green Ohio: Bowling Green State University Philosophy, pp. 11–19.
Nifo, Agostino, 1521, Dialectica Ludicra (Logic as a game), Florence: Bindonis.
Weng, Jui-Feng, with Shian-Shyong Tseng and Tsung-Ju Lee, 2010, “Teaching Boolean logic through game rule tuning,” IEEE Transactions, Learning Technologies, 3(4): 319–328. [Uses Pac-Man games to teach Boolean logic to junior high school students.]

Logical Games

Gale, David and F. M. Stewart, 1953, “Infinite games with perfect information,” in Contributions to the Theory of Games II (Annals of Mathematics Studies 28), H. W. Kuhn and A. W. Tucker (eds.), Princeton: Princeton University Press, pp. 245–266.
Kechris, Alexander S., 1995, Classical Descriptive Set Theory, New York: Springer-Verlag.
Marion, Mathieu, 2009, “Why play logical games?,” in Ondrej Majer, Ahti-Veikko Pietarinen, and Tero Tulenheimo eds., Games: Unifying Logic, Language and Philosophy, New York: Springer-Verlag, pp. 3-25.
Osbourne, Martin J. and Ariel Rubinstein, 1994, A Course in Game Theory, Cambridge: MIT Press.
Väänänen, Jouko, 2011, Models and Games, Cambridge: Cambridge University Press.
van Benthem, Johan, 2011, Logical dynamics of information and interaction, Cambridge: Cambridge University Press, 2011.
–––, 2014, Logic in games, Cambridge, MA: MIT Press.

Semantic Games for Classical Logic

Henkin, Leon, 1961, “Some remarks on infinitely long formulas,” in Infinitistic Methods, op. cit., pp. 167–183.
Hintikka, Jaakko, 1973, Logic, Language-Games and Information: Kantian Themes in the Philosophy of Logic, Oxford: Clarendon Press.
Hintikka, Jaakko, 1996, The Principles of Mathematics Revisited, New York: Cambridge University Press. [See for example pages 40, 82 on the axiom of choice.]
Hodges, Wilfrid, 2001, “Elementary Predicate Logic 25: Skolem Functions,” in Dov Gabbay, and Franz Guenthner (eds.), Handbook of Philosophical Logic I, 2nd edition, Dordrecht: Kluwer, pp. 86–91. [Proof of equivalence of game and Tarski semantics.]
Kolaitis, Ph. G., 1985, “Game quantification,” in J. Barwise and S. Feferman (eds.), Model-Theoretic Logics, New York: Springer-Verlag, pp. 365-421.
Peirce, Charles Sanders, 1898, Reasoning and the Logic of Things: The Cambridge Conferences Lectures of 1898, ed. Kenneth Laine Ketner, Cambridge Mass., Harvard University Press, 1992.

Semantic Games with Imperfect Information

Hintikka, Jaakko and Gabriel Sandu, 1997, “Game-theoretical semantics,” in Johan van Benthem and Alice ter Meulen (eds.), Handbook of Logic and Language, Amsterdam: Elsevier, pp. 361–410.
Hodges, Wilfrid, 1997, “Compositional semantics for a language of imperfect information,” Logic Journal of the IGPL, 5: 539–563.
Janssen, Theo M. V. and Francien Dechesne, 2006, “Signalling: a tricky business,” in J. van Benthem et al. (eds.), The Age of Alternative Logics: Assessing the Philosophy of Logic and Mathematics Today, Dordrecht: Kluwer, pp. 223–242.
Mann, Allen L., Gabriel Sandu, and Merlin Sevenster, 2011, Independence-Friendly Logic: A Game-Theoretic Approach (London Mathematical Society Lecture Note Series 386), Cambridge: Cambridge University Press.
von Neumann, John and Oskar Morgenstern, 1944, Theory of Games and Economic Behavior, Princeton: Princeton University Press.
Väänänen, Jouko, 2007, Dependence Logic: A New Approach to Independence Friendly Logic, Cambridge: Cambridge University Press.

Semantic Games for Other Logics

Bradfield, Julian and Colin Stirling, 2006, “Modal mu-calculi,” in P. Blackburn et al. (eds.), Handbook of Modal Logic, Amsterdam: Elsevier, pp. 721–756.
Dekker, Paul, and Marc Pauly (eds.), 2002, Journal of Logic, Language and Information, 11(3): 287–387. [Special issue on Logic and Games.]
Hennessy, Matthew, and Robin Milner, 1985, “Algebraic laws for indeterminism and concurrency,” Journal of the ACM, 32: 137–162.
Parikh, Rohit, 1985, “The logic of games and its applications,” in Marek Karpinski and Jan van Leeuwen (eds.), “Topics in the Theory of Computation,” Annals of Discrete Mathematics, 24: 111–140.
Pauly, Marc, and Rohit Parikh (eds.), 2003, Studia Logica, 72(2): 163–256 [Special issue on Game Logic.]
Stirling, Colin, 2001, Modal and Temporal Properties of Processes, New York: Springer-Verlag.
van Benthem, Johan, 2006, “The epistemic logic of IF games,” in Randall Auxier and Lewis Hahn (eds.), The Philosophy of Jaakko Hintikka, Chicago: Open Court pp. 481–513.
van Benthem, Johan with Amitabha Gupta and Rohit Parikh, 2011, Proof, Computation and Agency, Dordrecht: Springer-Verlag.

Back-and-Forth Games

Blackburn, Patrick with Maarten de Rijke and Yde Venema, 2001, Modal Logic, Cambridge: Cambridge University Press.
Doets, Kees, 1996, Basic Model Theory, Stanford: CSLI Publications and FoLLI.
Ebbinghaus, Heinz-Dieter and Jörg Flum, 1999, Finite Model Theory, 2nd edition, New York: Springer.
Ehrenfeucht, Andrzej, 1961, “An application of games to the completeness problem for formalized theories,” Fundamenta Mathematicae, 49: 129–141.
Grädel, Erich with Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, and Scott Weinstein, 2007, Finite Model Theory, Berlin: Springer-Verlag.
Libkin, Leonid, 2004, Elements of Finite Model Theory, Berlin, Springer-Verlag.
Otto, Martin, 1997, Bounded Variable Logics and Counting—A Study in Finite Models (Lecture Notes in Logic, 9), Berlin: Springer-Verlag.
Peters, Stanley and Dag Westerståhl, 2006, Quantifiers in Language and Logic, Oxford: Clarendon Press.
Tarski, Alfred, 1946, “Address at the Princeton University Bicentennial Conference on Problems of Mathematics (December 17–19, 1946),” Hourya Sinaceur (ed.), Bulletin of Symbolic Logic, 6 (2000): 1–44.
van Benthem, Johan, 2001, “Correspondence Theory,” in Dov Gabbay and Franz Guenthner (eds.), Handbook of Philosophical Logic III, 2nd edition, Dordrecht: Kluwer.

Other Model-Theoretic Games

Anthony, Martin, and Norman Biggs, 1992, Computational Learning Theory, Cambridge: Cambridge University Press. [For Vapnik-Chervonenkis dimension.]
Gurevich, Yuri and Leo Harrington, 1984,“Trees, automata, and games,” in H. R. Lewis (ed.), Proceedings of the ACM Symposium on the Theory of Computing, San Francisco: ACM, pp. 171–182.
Hirsch, Robin and Ian Hodkinson, 2002, Relation Algebras by Games, New York: North-Holland.
Hodges, Wilfrid, 1985, Building Models by Games, Cambridge: Cambridge University Press.
Hodges, Wilfrid, 1993, Model Theory, Cambridge: Cambridge University Press.
Oxtoby, J. C., 1971, Measure and Category, New York: Springer-Verlag.
Ziegler, Martin, 1980, “Algebraisch abgeschlossene Gruppen,” in S. I. Adian et al. (eds.), Word Problems II: The Oxford Book, Amsterdam: North-Holland, pp. 449–576.

Games of Dialogue, Communication and Proof

Abramsky, Samson and Radha Jagadeesan, 1994, “Games and full completeness for multiplicative linear logic,” Journal of Symbolic Logic, 59: 543–574.
Abramsky, Samson and Paul-André Melliès, 1999, “Concurrent games and full completeness,” in Proceedings of the Fourteenth International Symposium on Logic in Computer Science, Computer Science Press of the IEEE, pp. 431–442.
Bench-Capon, T. J. M. and Paul E. Dunne, 2007, “Argumentation in artificial intelligence,” Artificial Intelligence, 171: 619–641. [The introduction to a rich collection of papers on the same theme on pages 642–937.]
Blass, Andreas, 1992, “A game semantics for linear logic,” Annals of Pure and Applied Logic, 56: 183–220.
Cignoli, Roberto L. O., Itala M. L. D’Ottaviano, and Daniele Mundici, 2000, Algebraic Foundations of Many-Valued Reasoning, Dordrecht: Kluwer.
Felscher, Walter, 2001, “Dialogues as a foundation for intuitionistic logic,” in Dov Gabbay and Franz Guenthner (eds.), Handbook of Philosophical Logic V, 2nd edition, Dordrecht: Kluwer.
Hodges, Wilfrid and Erik C. W. Krabbe, 2001, “Dialogue foundations,” Proceedings of the Aristotelian Society (Supplementary Volume), 75: 17–49.
Japaridze, Giorgi, 2003, “Introduction to computability logic,” Annals of Pure and Applied Logic, 123: 1–99.
Lorenzen, Paul, 1961 “Ein dialogisches Konstruktivitätskriterium,” in Infinitistic Methods, op. cit., 1961, pp. 193–200.
Pudlak, Pavel, 2000, “Proofs as games,” American Mathematical Monthly, 107(6): 541–550.
Walton, Douglas N. and Erik C. W. Krabbe, 1995, Commitment in Dialogue: Basic Concepts of Interpersonal Reasoning, Albany: State University of New York Press.

Academic Tools

Other Internet Resources

Giorgi Japaridze’s Computability Logic page

上一页模糊逻辑 fuzzy (Petr Cintula, Christian G. Fermüller, and Carles Noguera)下一页混合逻辑 hybrid (Torben Braüner)

最后更新于8小时前