逻辑和游戏（五）
在技术上，结构A的元件预先固定，例如a0，a1，a2等，但是必须通过播放来沉降这些元件的性质。 每个玩家通过抛出关于元素的一组原子或否定的原子陈述，仅在到目前为止所抛出的所有陈述组成的条件中，必须与游戏前写下来的固定的一组公理组成。 （所以在否定的原子句子中投掷¬φ具有防止任何玩家在稍后阶段加入φ。）在联合游戏结束时，抛出的一组原子句具有规范模型，这是结构a; 有些方法可以确保它是固定的一组公理的模型。 如果给出了一个有胜利策略的建造商，据说A可能的属性p是可执行的。 中心点（基本上归因于EHENFEUCHT）是，可信地是无限的可执行性质的结合再次可强制执行。
可以使用强制游戏的变体证明模型理论的各种模型理论的定理。 在这些变体中，我们不会构建模型，而是一个给定模型的子模型。 我们以句子（或可数句子集）φ开头m型。 然后我们列出了φ的子表，每个播放器都有一个具有免费变量的子表单。 玩家的任务是尽快在游戏中发生的参数，并且有一个证人在大型模型中的公式的真相，一个这样的见证人。 当游戏结束时，已经建立了一个满足φ的方式建立了一个可数的M的亚模型。
“迫使”名称是Paul Cohen的应用程序，在20世纪60年代初构建了集合理论的模型。 亚伯拉罕罗宾逊调整了它制造了一种用于建立可数结构的一般方法，而马丁齐格勒介绍了游戏环境。 后来罗宾·赫希和伊恩霍斯斯顿使用过相关的游戏来解决一些关于关系代数的旧问题。
在考虑Dawkins问题时，迫使游戏是一个健康的例子。 他们提醒我们，在逻辑游戏中，不用有助于将球员视为彼此相对。
7.2切割和选择游戏
在传统的切割和选择游戏中，您拍了一块蛋糕并将其切成两个较小的碎片; 然后我选择其中一个碎片并吃它，让另一个留给你。 这个程序应该对你施加压力来削减蛋糕。 数学家，不太了解运动的目的，坚持迭代它。 因此，我让你切成了两个，然后我选择了这两个之一; 然后你再次削减了这件头，依此类推。 一些更具不爱心的数学家让你将蛋糕切成几件而不是两个。
这些游戏在定义理论中很重要。 假设我们有一个物体的集合和一个家庭的属性; 每个属性都将A剪切到具有属性的这些对象的集合和那些没有的集合中。 让∃切割，从整个集合A开始，并使用刀中的属性; 让∀选择其中一个部分（是a的子集），并将其恢复到∃再次切割，再次使用s中的属性; 等等。 一旦∀选择一个空作品，请让∃输掉。 我们说（A，S）如果∀有一个策略，那么∀∀有一个策略，这确保了在她第m的举动之前∃会丢失。 （a，s）的等级提供了关于S.中可定义的亚群系列的有价值的信息。
这场比赛的变化，允许一件件被切割成多重较小的碎片，是模型理论的分支的基础，称为稳定性理论。 广泛的说法，在稳定性理论的意义上，如果我们采取理论的模型和S在一个自由变量中的一组自由变量中的一个自由变量中，结构（a，s）具有“小”等级，理论是“良好”。 不同的变化是在每个步骤中要求，∃∃分成从早期步骤中幸存下来的两个部分，并且一旦其中一个切片是空的，她就会丢失。 （在这个版本中∀是冗余的。）通过这种变化，（a，s）的等级称为其VAPNIK-Chervonenkis维度; 这种概念用于计算学习理论。
7.3在两个后继函数树上的游戏
想象一下已经建立在级别的树。 在底部级别，有一个根节点，但左分支和右分支从中升起。 在下一个级别上，有两个节点，每个分支上一个，并且来自这些节点中的每一个左分支和右分支成长。 因此，在下一个级别上，有四个节点，并且树在每个节点中的每个节点处再次分支。 持续无限，这棵树被称为两个后续函数的树（即留下后继者和右后继者）。 将节点作为元素作为元素，并为左后和右继继承的两个功能符号，我们有一个结构。 Michael Rabin的强大定理指出，有一种算法将告诉我们，对于适合这种结构的语言中的每个Monadic二阶判断，是否在结构中是真的。 （'Monadic二阶'意味着逻辑就像一阶，除了我们还可以量化元素集 - 但不是对元素的二进制关系。）
拉比的定理有任何许多有益的后果。 例如，DOV Gabbay使用它来证明某些模态逻辑的可解锁性。 但是，利用自动机，rabin的证据令人惊奇地难以追随。 Yuri Gurevich和Leo Harrington，独立的Andrei Muchnik，发现了更简单的证据，其中自动机是游戏中的一名球员。
Rabin的这种结果是将与自动机构连接的游戏的几个有影响力的重建之一。 另一个例子是用于验证模态系统的属性的奇偶校验游戏。 查看斯特林（2001）第6章; Bradfield和Stirling（2006）讨论模态μ微积分的奇偶校验游戏。
8.对话，沟通和证明游戏
几个中世纪文本描述了一种辩称义务的形式。 有两种争议者，互联网和响应。 在会议开始时，争议者将同意“积极”，通常是虚假陈述。 响应者的工作是为了呈现彩色的真相，给予对手的有关问题的合理答案; 最重要的是，他不得不避免不必要地相矛盾。 opponens的工作是试图强迫响应矛盾。 所以我们广泛地了解Dawkins问题的答案，但我们不知道游戏规则！ 中世纪教科书确实描述了争议者应遵循的几条规则。 但这些规则不是游戏规则的规定; 他们是教科书借助于借助于示例来源于声音推理原则的指导方针。 （威尼斯的保罗通过“伟大的逻辑学家，哲学家，几何和神学家”的实践证明了一个规则。）特别是对义务教师开放，以发现新规则。 这种开放态度意味着我们在感觉中的义务不是逻辑游戏。
不是每个人都同意前一句话。 例如，Catarina Dutilh Novaes（2007,6）详细捍卫了义务在“中世纪和现代理论框架之间的概念相似之处的显着案例”。 但无论我们采取这个问题的观点，这些辩论都激发了逻辑游戏中现代研究的一个重要线路。
想象一下∃在证明理论中进行口头检查。 审查员给她一个句子，邀请她开始证明它。 如果句子有表单
φ∨ψ
然后她有权选择其中一个句子并说'OK，我会证明这一点'。 （实际上，如果审查员是一种直觉主义者，他可能坚持认为她选择了一个被证明的句子。）另一方面，如果句子是
φ∧ψ
然后是审查员，成为审查员，可能会选择自己的一个混合，并邀请她证明一个人。 如果她知道如何证明该联合，那么她肯定知道如何证明这一结词。
φ→ψ的情况是一个小的子集。 她可能想要首先假设φ才能推断出ψ; 但是有一些困惑的风险，因为她到目前为止写下的句子都是他们所证明的所有事情，而且φ并不是一件要证明的事情。 审查员可以通过说'我假设φ来帮助她，让我们看看你是否可以从那里得到♥。 在这一点上，她有可能看到了通过推导φ的矛盾来获得ψ的方法; 因此，她可以在审查员身上转动桌子，并邀请他表明他的假设是一致的，以便证明它不是。 对称性并不完美：他要求她表明一句话到处都是真的，而她邀请他展示一个句子在某个地方。 尽管如此，我们可以看到一种二元性。
这种想法躺在保罗洛伦登的辩证赛之后。 他表明，通过一定数量的推动和推动，人们可以编写游戏的规则，其中具有∃具有赢得策略的属性，如果句子，只有她在开始时呈现的句子是直观逻辑的定理。 在向中世纪辩论的姿态中，他称之为支持者和另一个球员对手。 几乎与中世纪的义务一样，对手赢得了推动者驾驶推荐人来到她的唯一动作是公然的自我矛盾。
Lorenzen声称他的游戏为直觉和古典逻辑（或用他的话来说提供了理由，使他们成为'Gerechtfertigt'，Lorenzen（1961,196））。 不幸的是，任何“辩解”涉及对Dawkins问题的令人信服的答案，而这一洛伦登从未提供过。 例如，他谈到了“攻击”的动作，即使（如审查员在上面的φ∧ψ的选择），它们看起来更像是敌意。
词条对话逻辑对 Lorenzen 的游戏和一些较新的变体进行了更全面的介绍。在其目前的形式（2013 年 1 月）中，它回避了 Lorenzen 关于证明逻辑的说法。相反，它将游戏描述为为逻辑提供语义（Lorenzen 肯定会同意这一点），并补充说，为了理解逻辑之间的差异，比较它们的语义会有所帮助。
从这个角度来看，Lorenzen 的游戏是最近证明理论家称之为证明语义的重要范例。证明语义不仅赋予可证明的概念“意义”，而且赋予证明中每个单独的步骤“意义”。它回答了“通过在证明中做出这一特定举动我们能得到什么？”的问题。 20 世纪 90 年代，许多从事计算机科学逻辑研究的人员寻找能够与线性逻辑和其他一些证明系统相符的游戏，就像 Lorenzen 的游戏与直觉逻辑相符一样。Andreas Blass 以及后来的 Samson Abramsky 和他的同事们都设计了与线性逻辑的部分内容相对应的游戏，但在撰写本文时，我们还没有在游戏和逻辑之间建立完美的对应关系。这个例子特别有趣，因为道金斯问题的答案应该对线性逻辑的定律给出直观的解释，而这正是这种逻辑所急需的。Abramsky 等人的游戏讲述了两个相互作用的系统的故事。但是，虽然他一开始的游戏是玩家礼貌地轮流进行，但 Abramsky 后来允许玩家“以分布式、异步的方式”行动，只有当他们选择时才会注意到对方。这些游戏不再是逻辑游戏的正常形式，它们在现实生活中的解释引发了许多新问题。
Giorgi Japaridze 提出了一种用于研究计算的“可计算性逻辑”。它的语法是一阶逻辑，带有一些让人联想到线性逻辑的额外项。它的语义是语义游戏，但有一些不寻常的特征。例如，并不总是确定哪个玩家进行下一步行动。策略函数的概念不再适合描述玩家；相反，Japaridze 描述了将第二个玩家（我们符号中的玩家 ∃）解读为一种计算机的方法。更多信息请访问他的网站。
另一组与 Lorenzen 的游戏属于同一家族的游戏是 Pavel Pudlak 2000 的证明游戏。在这里，对手（称为证明者）扮演法庭上的律师角色，他知道提议者（称为对手）犯了某些罪行。支持者会坚称自己是无辜的，并准备说谎来为自己辩护。对手的目的是迫使支持者反驳支持者之前说过的话；但对手会保留记录，并且（如上面的石子游戏一样）有时他不得不从记录中删除一些内容，因为空间或内存不足。重要的问题不是对手是否有获胜策略（从一开始就假设他有），而是他需要多少内存来记录。这些游戏是显示各种证明系统中证明长度的上限和下限的有用工具。
另一种允许说谎的逻辑游戏是乌拉姆的谎言游戏。在这里，一个玩家在某个给定的范围内想出一个数字。第二个玩家的目标是通过向第一个玩家问是/否问题来找出这个数字是多少；但第一个玩家可以在他的答案中说一些固定数量的谎言。就像在普德拉克的游戏中一样，第二个玩家肯定有获胜策略，但问题是这个玩家要付出多大的努力才能获胜。这次衡量标准不是空间或记忆，而是时间：他要问多少问题？Cignoli 等人 2000 年第 5 章将这个游戏与多值逻辑联系起来。
回到洛伦岑：他未能区分一个人在争论中可能采取的不同立场：陈述、假设、让步、质疑、攻击、承诺。是否真的有可能在不预设某种逻辑的情况下定义所有这些概念是一个有争议的问题。但不要介意；沿着这些思路对洛伦岑的游戏进行改进可以作为一种非正式逻辑的方法，尤其是旨在系统化合理非正式论证的可能结构的研究。关于这方面，请参阅 Walton 和 Krabbe 1995。Bench-Capon 和 Dunne 2007 中的论文也相关。
