具有显式策略的LP博弈论语义与Nim博弈的嵌入

理论计算机科学电子笔记165（2006）133-144www.elsevier.com/locate/entcs具有显式策略的Bryan Renne布莱恩·雷恩1，2纽约市立大学研究生中心纽约州纽约市第五大道365号4319室，邮编10016摘要本文介绍了LP的一种博弈论语义--Artemov为了证明这个观点的效用，我们定义了一个著名的Nim博弈嵌入到命题验证博弈中，它允许我们通过将该实例的形式化版本的证明内在化到LP中，来提取一个可获胜的Nim实例上的获胜策略保留字：证明逻辑，博弈论语义学，GTS1引言让我们来看看两个游戏，Nim和验证。尼姆很有趣，但什么事都不告诉我们。验证是无聊的，但告诉我们很多关于命题的可证明性。我们将看到，可以赢的Nim游戏可以嵌入到验证中，所以也许在命题的可证明性中会发现一些乐趣。但是，尽管我们成功地把无聊变成了乐趣，我们还是遇到了一些关于策略和策略操作的有趣想法特别地，我们将看到，一个关于策略的自然运算类与LP中的某些运算密切相关，LP是Artemov这个逻辑将公式标记项t引入到命题逻辑的语言中，允许我们取一个公式F并构造新的公式t：F，其预期的阅读是这种解读来自于理论的构建：期限结构模仿了系统中的演绎，使得每个定理F都可以构造一个项t，使得t：F也是一个定理。[1]作者得到了纽约市立大学CCCI研究基金#91639-0001“知识表示的数学基础”的部分支持2电子邮件：bryan@renne.org1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.042134B. Renne/Electronic Notes in Theoretical Computer Science 165（2006）133在本文中，我们的任务是通过作为验证的扩展而获得的形式博弈来提供对LP在这个形式博弈中，项t将被指定为策略，因此公式t：F可以读作，这种解释自然产生于我们在《尼姆》和《验证》中所做的直观的战略观察。特别地，通过将可获胜的Nim实例嵌入到Verification中，我们获得了一个命题定理F，其证明可以在LP中内部化。这就产生了一个项t，使得t：F是一个LP定理，所以t是F上的一个策略，我们可以从中提取出特定Nim实例的获胜策略。2阿尔捷莫夫LP语言通过引入变量x1，x2，x3，..的可数集合来扩展命题逻辑的语言。. ，常数c1，c2，c3，.. . 在此基础上，提出了一种新的函数符号：F，一元函数符号。术语是由使用函数符号的变量和常量组成的。公式形成的规则是那些命题逻辑除了以下：如果t是一个项，F是一个LP公式，那么t：F也是一个LP公式。LP理论由以下公理和规则模式组成• 命题逻辑C. 命题逻辑RC. 肯定前件：从A推断B，B和A• 证据管理LP 1. u：（A <$B）（v：A <$（u·v）：B）LP 2.u：A！u：（u：A）LP 3.u：A v：A（u + v）：ALP 4。 u：A ARLP。 常数必然性：从常数c和公理A推断c：A通过推导长度的归纳，可以证明LP满足以下内在化性质：如果A是LP的一个定理，则存在不包含变量的项t使得t：A也是LP定理。因此，LP内化了它自己的证明。我们将在后面利用这一点来看看LP如何用于描述验证（以及尼姆）中的获胜策略。让我们先来介绍一下尼姆和验证。3两个游戏：Nim和验证著名的尼姆博弈[2]是一个两人零和有限博弈。尼姆游戏的初始设置包括三个独立的棍子堆，每堆都是有限大小的。一个回合包括选择一堆，然后从那堆中删除任何非零数量的棍子，留下其他两堆。被移除的棍子将被丢弃，因为它们不再是游戏的一部分。两名球员轮流，直到所有的棍子被删除。拿起最后一根棍子的玩家B. Renne/Electronic Notes in Theoretical Computer Science 165（2006）133135就是赢家尼姆是一个分支深度有限的零和博弈，因此由策梅罗定理决定。也就是说，对于尼姆的每一个例子，其中一个参与者总是有一个获胜的策略-一种选择他的行动的方式，以确保自己获胜，而不管其他参与者的行动我们的目标是Ehrenfeucht-Frase-Hintikkaubformula-choosingver ii-i fication game，我们称之为验证[3，4]。这个游戏也是两个玩家，零和，有限的。验证游戏的初始设置包括一个使用否定和析取写成的命题公式F，以及一个解释原子公式的模型M为了方便起见，我们将第一个玩家称为True，第二个玩家称为False。游戏开始于公式F，使用True进行游戏。在一个玩家的回合中• 如果公式是析取A→B，则当前玩家选择A或B，然后游戏继续与同一玩家进行该子公式。• 如果公式是否定的<$A，那么回合改变，另一个玩家继续A上的游戏。• 如果公式是原子p，那么游戏结束。获胜者通过测试M中p的真值并将其与要移动的玩家的名字进行比较来确定。如果它们匹配，True获胜。否则，假赢。验证也是零和的，并且具有有限的分支深度，所以它也是确定的。然而，验证是一个正式的游戏。这不仅意味着这个游戏对小学生来说是无聊的，而且还意味着它被操纵了，以便说出关于命题公式F的一些有用的东西。特别是，如果我们在M中称F为真，只要真在F与模型M的博弈中有获胜策略，那么我们最终会像通常的塔斯基语义那样在M这也可以扩展到有效性水平：无论模型M如何，只要True在F上的博弈中有获胜策略，就称F有效，并且我们得到了塔斯基有效公式类（即命题定理）。正如我们现在所展示的，尼姆可以嵌入到验证中。Nim实例的初始配置可以用一个非负整数的三元组（a，b，c）来描述在这样的三元组上定义一个排序如下：（aJ，bJ，cJ）（a，b，c）当且仅当对于恰好一个坐标，素数严格小于非素数，并且其他两个坐标相等。<<我们现在将分配公式（a，b，c）T和（a，b，c）F到每个Nim实例（a，b，c）。首先，设（0，0，0）T：=T和（0，0，0）F：=T（分别为真命题常数和假命题常数）。 那么对于a，b，c不全为零，设（a，b，c）T：=JJJF（a，b，c）（aJ，bJ，cJ）（a，b，c）（a，b，c）F的定义也是如此，尽管T上标在右边。可以证明，True在验证博弈（a，b，c）T中有一个获胜策略，而第一个参与者在Nim博弈（a，b，c）中有一个获胜策略。原因是这些游戏的游戏树具有相同的结构，136B. Renne/Electronic Notes in Theoretical Computer Science 165（2006）133在一个游戏中的一个动作与另一个游戏中的一个动作以这样一种方式双射地对应，即一个游戏的一个动作与另一个游戏中的对应动作具有相同的获胜者。例如 ， 考虑 Nim 博弈 （1， 1， 1） 。我 们有 （ 1， 1， 1）T=<$（0，1，1）F<$（1，0，1）F<$（1，1，0）F。如果真的选择了<$（0， 1， 1）F（所以他从第一堆中取出棍子），那么假的必须在公式（0，1，1）F上移动，其中（0，1，1）F=<$（0，0，1）T<$（0，1，0）T.但无论子公式False然后选择，他输了。因为如果False选择<$（0， 0， 1）T（所以他从第二堆中取出棍子），那么True在（0， 0， 1）T上移动。现在，（0， 0，1）T=<$（0， 0， 0）F，所以True只有一次移动（他拿起最后一根棍子）。然后轮到False在所有的模型中，都是假的。类似地，如果False选择<$（0， 1， 0）T，那么True在（0， 1， 0）T=<$（0， 0， 0）F=<$上移动（并再次拿起最后一根棍子）并获胜。因此，我们看到True在验证博弈（1，1，1）T这个策略与他在尼姆博弈（1，1，1）中的获胜策略直接对应。似乎这种嵌入验证游戏的方法应该适用于任何两人零和有限游戏的实例。虽然这本身很有趣，但我们将在本文中花时间更仔细地研究验证游戏中的策略，并将嵌入式Nim游戏作为特例的验证。特别是，我们对特定的获胜策略如何结合和相互作用感兴趣，Nim将是收集我们的直觉和理解所涉及问题的自然场所。特别是，我们将描述LP如何提供一种自然的方法，将获胜策略以一种与我们在尼姆博弈背景下对获胜策略的直观讨论有意义的方式纳入验证博弈。我们最终得到了LP的语义，它是验证游戏沿着我们考虑的路线4关于战略首先，验证游戏中的策略是什么？由于策略应该描述选择哪个子公式，我们说验证游戏中关于公式F的策略是定义在F的解析树上的函数，它将每个非叶子带到它的一个孩子。F上的获胜策略是这样一种策略，它保证了根据这个策略选择行动的参与者获胜，而不管其他参与者的行动。现在让我们对验证博弈中的获胜策略进行一些观察。因为尼姆可以被看作是验证的一个特例，所以我们自由地使用尼姆的例子来支持直觉。• 避开对手的胜局。在Nim博弈（3，2，0）中，如果第一个玩家B. Renne/Electronic Notes in Theoretical Computer Science 165（2006）133137把剩下的一堆都倒空现在， 因此，策略s不能包括从一堆中取出所有的棍子，因为（0， 2， 0）和（3， 0， 0）对于任何落在它们上面的人来说都是获胜的位置，因此关于（3，2， 0）的获胜策略必须避免给其他玩家首先移动这些位置的机会。所以我们看到，一个成功的策略必须避免那些对对手有利的位置。• 如果失去一切就投降，否则就战斗。如果一个球员的每一否则，他应该继续下去。例如，在尼姆博弈（0， 1， 1）中，要移动的玩家可能希望简单地投降，因为他肯定会输。因此，让玩家在移动时选择投降是很方便的。 策略的定义可以改变以适应这一点：策略是解析树上的一个函数，它将每个非叶节点带到它的一个子节点，或者带到一个被理解为投降的特殊值请注意，特别是当一个参与者遇到否定<$A时，他可以选择投降或继续参与。如果他投降，游戏就结束了，他输了。如果他继续，那么游戏就像以前一样传递给子公式A上的另一个玩家。• 选择最好的计划。如果在同一个公式F上有两个不同的策略，那么参与人应该选择对他最有利的策略。有时这不过，有时候这确实很重要：尼姆博弈中第一个参与者的获胜策略（3， 2， 0）需要第一个参与者做出明智的选择。现在让我们尝试用LP的语言对这些直观的观察进行半形式化的解释。如果s是一个策略，其定义域包含F，那么我们写s：F.所以我们还是像以前一样读s：F然后，我们可以将我们的意见重申如下。• 避开对手的胜局。假设s是关于<$A<$B的策略，t是关于A的策略;也就是说，s：（<$A<$B）和t：A都是。如果s和t在各自的公式上都是获胜策略，那么s的第一步肯定不可能是选择-A，因为对手可以先在A上移动，然后他可以在A上使用获胜策略t。因此，获胜策略选择B作为第一步。 因为博弈在B上继续，换了一个回合，那么B上就有一个获胜的策略：在B上跟随S。 另一方面，如果s或t之一不是获胜策略，那么参与人必须采取其他策略。所以考虑以下关于B的策略：此策略仅在s和t是正确的类型，否则做其他事情。让我们用s·t来表示这个策略。然后我们看到，如果s在<$A赢B，t在A赢，那么s·t在B赢。• 如果失去一切就投降，否则就战斗。 如果s：A和s在A上获胜，那么参与人138B. Renne/Electronic Notes in Theoretical Computer Science 165（2006）133应该战斗：在A上应用S，然后获胜。否则，如果s在A上没有获胜，玩家必须做别的事情。这个S.• 选择最好的计划。假设s和t都是A上的策略，参与人要决定是选s还是选t.当然，他应该选择两者中更好的一个。这个虽然我们的考虑已经引导我们构建了战略s·t，！s和s+t给定策略s和t，我们希望反过来。因此，让我们定义二元运算·和+以及一元运算！根据我们上面的描述。这些是在我们的游戏中具有明确意义的策略上的操作。事实上，这些操作允许我们将逻辑LP解释为显式策略的逻辑。5显式策略假设AB是<$AB的缩写，因此在AB中选择A（然后同意继续玩游戏，而不是投降）使另一个玩家轮到A，而选择B则允许当前玩家保留他在B的然后，我们可以通过验证游戏的扩展来解释LP。特别地，让我们假设术语被分配了它们所标记的公式上的策略。然后让函数符号被解释为我们在前一节中定义的策略上的操作。 LP的验证博弈是从命题逻辑的验证博弈中通过添加以下规则得到的：如果一个参与者在他的回合中达到s：A，他同意此后根据策略s进行游戏。这为LP公式提供了一种解释，因此我们可能会问这种解释是否合理。让我们依次考虑每个LP公理。LP 1. u：（A <$B）（v：A <$（u·v）：B）如果u不是A<$B上的获胜策略，那么有一些策略s击败了它。因此，True选择左子公式u：（A<$B），这迫使在游戏的剩余时间里，根据u来玩。真则赢，因为他可以玩s和击败u。如果v在A上不是获胜策略，也会发生类似的情况：True选择右子公式v：A（u·v）：B（保留他的回合），然后选择左子公式v：A，所以False在A上选择v，True可以击败v，因为v在A上没有获胜。在u和v都是获胜策略的情况我们已经看到，u·v是B上的获胜策略，所以True向右移动两次到（u·v）：B，然后获胜，因为他在B上使用获胜策略u·v。LP 2.u：A！u：（u：A）u在A上不是获胜策略的情况与LP 1相同，因此假设u在A上是获胜策略。True然后向右移动并保留他在公式上的回合！u：（u：A），因此必须按策略玩！联合 现在，！u是策略B. Renne/Electronic Notes in Theoretical Computer Science 165（2006）133139如果u既然你赢了A，那么策略！u让True继续玩，所以True移动到u：A，然后让他的下一个移动应用策略u（根据策略的指示！u）。 在公式u：A上，True应该将u应用于A，与指示一致！u，所以True同意采取的策略是一致的。真的，真的。LP 3.u：A v：A（u + v）：A如果u和v都不是A上的获胜策略，那么True向左移动，并在u：A上击败False，无论False选择哪个子博弈。假设u或v是A上的获胜策略那么u+v是选择u和v中较好的策略，所以如果True在LP 3上向右移动，达到公式（u+v）：A，他赢了，因为u+v让他采取在A上获胜的策略。LP 4。 u：A A如果u不是A上的获胜策略，则True向左移动到u：A，并像以前一样获胜。假设u是ATrue然后向右移动到A，保留他的回合，然后在A上遵循获胜策略u。真的赢了。因此，我们已经看到True在LP 1到LP 4上有一个获胜策略。我们之前提到过，True在命题定理上有一个获胜策略，因此，特别地，True在LP的公理C上有一个获胜策略。True的获胜策略在肯定前件下是封闭的，这是根据LP 1中的考虑得出的（这是有道理的，因为LP 1是一个内化的肯定前件）。最后，由于我们已经证明了公理LP 1到LP 4和C都有获胜策略，只要LP常数被分配给公理的获胜策略，获胜策略在常数必然性下是封闭的。 总之，我们显示了以下情况。定理5.1（合理性）LP对于验证博弈是合理的;也就是说，True在验证博弈中的每个LP定理上都有一个获胜策略。这一切都是相当非正式的，目的是侧重于想法，而不是技术形式。感兴趣的读者可以在附录中找到技术细节。特别地，通过对一些细节的处理，我们还可以得到下面的完备性结果，其证明也在附录中给出定理5.2（完备性）LP对于验证博弈是完备的;也就是说，True在验证博弈中只有那些作为定理的LP公式才有获胜策略。现在让我们看看如何使用LP内在化属性来描述嵌入验证的博弈中的获胜策略。6Nim的LP考虑尼姆博弈（1， 2， 0），由于第三个坐标总是零，我们将其写为（1，2）。第一个参与者在这个博弈中有一个获胜策略，因此True在验证博弈（1，2）T中也有一个获胜策略。（1， 2）T140B. Renne/Electronic Notes in Theoretical Computer Science 165（2006）133JFFJFF1 .一、¬¬⊥ ⊃ ⊥A1二、 （）（（）（））A23 .第三章。RC的1，2四、 （））A3五、 ）RC 3，4六、 ）（（））A47 .第一次会议。（）“我的天，（1， 1）FRC5，6图1.一、命题逻辑中的（1，2）T的证明RC是肯定前件。1 J. c1：（）2 J。 c2：{（）（（）（））}3 J。（（c2·c1）·c1）：{}4 J。 c3：{（）（）}5 J。 （c3·（（c2·c1）·c1））：）.Σ六、 c4：）（1，0））（））.Σ7 .第一次会议。 （c4·（c3·（（c2·c1）·c1）：（（1，0））（）图二.（1，2）T.在命题逻辑中是可证明的。我们将展示如何将这个证明内在化到LP中，从而给我们一个描述验证博弈（1， 2）T以及尼姆博弈（1， 2）中获胜策略的术语。我们首先计算几个关键公式，如下所示。（0， 1）T=（1，0）T=（1， 1）F=<$（0， 1）T<$$>（1，0）T=<$$><$$><$（1，2）T=（1，0）F（1，1）F我们现在证明命题逻辑中的（1，2）T，使用以下命题公理的实例：A1. ¬¬A⊃AA2. （A C）（（B C）（A B C））A3. （A）A4. AB A证据如图1所示。 然后，我们在图2中的LP中内化这个证明。B. Renne/Electronic Notes in Theoretical Computer Science 165（2006）133141现在，一旦我们描述了公理A1到A4上的真的获胜策略，我们就可以对由LPtermc4·（c3·（（c2·c1） ·c1））定义的序列进行分类。为了简化描述，我们将公式A写成“第一个玩家（真）在A上有一个获胜策略s1（A）。类似地，由常数c1到c4描述的获胜策略如下。A1. c1：如果A为真，则选择A并应用s1（A）;否则，选择A，继续通过否定，然后应用s2（A）。A2. c2：(i) 如果C为真，选择正确的子公式三次，到达C，然后播放s1（C）。(ii) 如果C为假而A为真，则选择左边的子公式A→C，继续过去否定，然后应用s1（A）或s2（C）来响应另一个参与者(iii) 如果C为假而B为真，则选择右边的子公式，然后选择左边的子公式，到达BC，并继续通过否定。然后应用s1（B）或s2（C）来响应另一个玩家(iv) 如果A、B和C都为假，则选择右边的子公式两次，然后选择左边的子公式，到达A→B，并继续通过否定。然后应用s2（A）或s2（B）来响应另一个玩家A3. c3：如果A为假，则选择<$A，继续经过否定，然后应用s2（A）;否则，选择A，继续经过否定，如果另一个参与者选择A，则应用s1（A）。A4. c4：如果A为假，则选择A，继续通过否定，然后应用s2（A）;否则，选择B→A，然后选择A并应用s1（A）。因此，我们可以计算以下乘积的意义：•c2·c1排除了c2策略中的第ii项，其他情况保持不变。• （c2·c1）·c1进一步排除了c2·c1策略中的第iii•c3·（（c2·c1）·c1）排除了c3策略的A类这个乘积就是）上的策略。根据c3，这个策略如下：继续通过<$（1，1）F中的否定，然后在（1，1）F上使用第二个参与者让我们计算第二个参与人在（1，1）F.继续经过<$（1， 1）F中的否定，在（1， 1）F上使用假=我知道了因此，False选择左析取或右析取。“假”是“真”，“假”是“真”，“假”是“真”。真对假的获胜策略是简单地继续，在假对假的情况下将游戏传递给假（所以真赢）。所以，总的来说，策略c3·（（c2·c1）·c1）是这样的：让False在（1，1）F上移动，不管他的移动如何，都继续通过下一个否定。• c4·（c3·（（c2·c1）·c1））排除了c4策略的A情况，只剩下选择右析取式A，然后应用策略s1（A）。那么，142B. Renne/Electronic Notes in Theoretical Computer Science 165（2006）133在我们的A4的特定例子中，这个乘积是在（1， 2）T上的以下获胜策略：选择<$（1， 1）F，然后应用策略c3·（（c2·c1）·c1）;也就是说，选择<$（1， 1）F，让False在（1， 1）F上移动，并且，不管他的移动，继续通过下一个否定。因此，我们看到，内在化的证明给出了验证博弈（1， 2）T中的获胜策略。这个策略对应于尼姆博弈中第一个玩家的获胜策略（1， 2）：从第二堆中取出一根棍子，让对手取出他想要的任何一根棍子作为回应，然后通过进行唯一剩下的移动（即拿起最后一根棍子）继续7致谢作者感谢Evan Goris，Roman Kuznets，Sergei Artemov，Melvin Fitting，RohitParikh，Eric Pacuit，两位匿名裁判，以及纽约市立大学计算逻辑研讨会的参与者提供了有用的反馈。提交人感谢Sergei Artemov和Elena Nogina提供的资金支持。引用[1] 阿尔捷莫夫，S.N.，显式可证明性和构造性语义，符号逻辑通报7（2001），pp。1-36号。[2] 布顿角L.，Nim，a game with a complete mathematical theory，The Annals of Mathematics3（2ndSeries）（1901-1902），pp. 35比39[3] Escherichfeucht，A.，博弈在形式化理论完备性问题中的应用，Fundamenta Mathematicae49（1960），pp. 第129-141页。[4] Hintikka，J.和G. Sandu，博弈论语义学，J. van Bentham和A. ter Meulen，编辑，《逻辑与语言手册》，Elsevier，1997年。361-410B. Renne/Electronic Notes in Theoretical Computer Science 165（2006）133143一附件：技术证明设A是一个LP公式。 T（A）表示A的解析树。 关于A的策略是T（A）上的一个函数，它将每个非叶节点带到它的一个子节点或一个唯一的投降值。 如果A上的一个策略的第一步（即T（A）的根A上的值）是投降，则称该策略是平凡的。一个策略如果不是微不足道的，就不是微不足道的一个可能的策略映射是一个函数S，它为每个项t和每个LP公式A分配A上的策略S（t，A）。一个可能的策略映射S是一个策略映射，如果它还满足以下每个属性：• 产品 如果S（u，A<$B）和S（v，A）都是非平凡的，则S（u·v，B）=S（u，A<$B）。• 砰如果S（u，A）是非平凡的，则S（！u，u：A）是T（u：A）上的函数，它将根u：A映射到它唯一的子节点A，并根据S（u，A）映射T（u• 总计。 如果S（u，A）是非平凡的，则S（u+v，A）=S（u，A）。 如果S（u，A）是平凡的，S（v，A）是非平凡的，则S（u+v，A）=S（v，A）.如果SJ是一个可能的策略图，则SJ的闭包是通过修改SJ（u·v，A），SJ（！u，A）和SJ（u+v，A），以便满足乘积、Bang和中的每一个。 不很难证明每一个可能的策略图都有一个闭包（事实上，有很多闭包）。 我们假设我们有一个一劳永逸的方法来生产每个可能的策略图SJ的闭包S，所以我们可以说，一个模型是一个对M=（V，SJ），由命题字母的集合V和可能的策略图SJ组成。对于 一 个 模 型 M 和 一 个 命 题 字 母 q ， 我 们 记 为 M|=qtomeanq∈VandwwwriteM|=qtomeanq∈/V。我们所有人都在看M| = T和M|对于所有型号M，= 1/2。验证是一个两个玩家的零和有限游戏，由玩家True和False玩。这个游戏有一个LP公式F和一个模型M=（V，SJ）作为它的初始设置。True则允许修改有限个对（c，A）的值SJ（c，A），其中c是常数，A是LP公理。 这产生了可能的策略图SJJ。我们将True所做的修改称为常量指定。如果True选择不做任何修改，那么我们称这个常量指定为空。设S是SJJ的闭包。游戏开始。从T（F）的根F上的True开始，如果当前节点不是叶子，要移动的玩家选择当前节点的直接子节点，否则选择投降。如果他投降，游戏就结束了，他输了。• 如果当前节点标记为<$A，他选择子节点A，则轮到另一个参与者• 如果当前节点被标记为A→B，并且他选择了a子节点，那么当前玩家保留他选择的任何子节点的回合144B. Renne/Electronic Notes in Theoretical Computer Science 165（2006）133• 如果当前节点被标记为u：A，并且他选择了标记为A的子节点，那么他保留他的回合，但此后同意根据S（u，A）选择他的移动。注意，如果他先前同意根据S（u，A）移动，则他后来遇到一个公式v：B，和S（v，B）S（u，B），那么我们要求他如果他投降，他可能不会履行他的承诺。一旦到达一片叶子，游戏结束。真赢得了一场已经到达叶子p的验证游戏，当且仅当我们有那个M| = p和True是移动或M| = p和False是移动。定理A.1（合理性）LP对于验证博弈是合理的;也就是说，True在每个LP定理的验证中都有一个获胜策略。证据推导长度的归纳法。众所周知，命题逻辑对于验证是合理的[4]。本文给出了LP公理的可靠性论证。可靠性在常数必然性下是封闭的，这一点很清楚：True简单地选择一个常数指定，将公理A（我们刚刚断言其存在性）上的获胜策略分配给（c，A）。这种可靠性在肯定前件下是封闭的，这是因为True可以将他对A B的常数指定与A的常数指定结合起来，然后在子公式B上使用他对AB的获胜策略，正如本文所讨论的那样。Q定理A.2（完备性）LP对于验证博弈是完备的;也就是说，True在验证博弈中只有那些作为定理的LP公式才有获胜策略。证据 我们使用最大一致性论证。现在，所谓集合，我们指的是LP公式的集合如果LP不从任何有限子集的合取中导出合取，则称一个集合是相容的称一个集合为极大相容的，如果它是相容的，并且加法不存在的任何公式使集合不一致。相容集通常可以推广到极大相容集。如果F不是LP定理，则{<$F}是相容的，因此可以推广到极大相容集S。对每个A∈S，设W（A）是A上的策略，满足以下性质：没有节点要求投降，对T（A）的每个节点B∈C，如果B∈S，则选择子节点B，如果B∈S，则选择子节点C.然后通过设置V = { q}来定义模型M =（V，SJ）|q∈S}，设SJ（t，A）= W（A），若t：A∈S，设SJ（t，A）为T（A）上的处处投降函数，若t：A∈/S. 如果True只接受空常数指定，则通过在W（A）处对A∈ S进行iiinth表示的n是A上具有模型M的由于<$F∈S，True在<$F上有获胜策略W（<$F），因此True在F上不可能有获胜策略。Q