广义博弈中的认知逻辑框架及其应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记278（2011）245-260www.elsevier.com/locate/entcs广义博弈埃米利亚诺·洛里尼和弗雷德里克·莫伊桑Universit'edeToulouse，CNRS，图卢兹信息研究所摘要这项工作的目的是提出一个逻辑框架，表示在上下文中的交互代理广泛的游戏形式。 由于这种游戏提供的时间维度的重要性，我们创建了一个模态认知逻辑，它允许对博弈树中的策略和顶点进行量化。文章的第一部分致力于逻辑本身及其语言和语义的定义。为了说明这一逻辑的使用，我们在下面的部分中定义了扩展形式博弈中的理性概念和逆向归纳概念，正如罗伯特·奥曼所定义的那样。基于这些定义，我们然后提供了奥曼定理的句法证明，该定理陈述如下：“对于任何非退化的完美信息博弈，理性的常识意味着逆向归纳解”。最后，我们提出了一个深入的正式分析的假设，需要证明这样一个定理。关键词：认知逻辑，广泛形式博弈，理性，逆向归纳，奥曼1介绍这篇文章的目的是提出一个模态逻辑框架，允许理性的认知游戏在广泛的形式。在这类博弈中，参与者根据理性的一般原则决定做什么，而不确定交互的几个方面，如其他代理人虽然认知博弈在经济学中得到了广泛的研究（在所谓的互动认识论领域，参见例如，[3，2，8，5，9，11]），而很少有模态逻辑分析的认知游戏都在战略形式和广泛的形式（见，例如，[22，10，8，18，26，14，23，24，4]），不存在逻辑与相应的形式语义的广泛形式的游戏已被证明是sufficiently一般：• 为了用对象语言来表达像逆向归纳这样的解决方案概念，• 从句法上推导出这些解的概念所依据的认识和合理性条件。1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.10.019246E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245虽然[23]和[24]中表明，仅对行为进行推理是足够的， 为了计算像逆向归纳法这样的解概念，这种博弈逻辑不能像奥曼的定义那样表达实质合理性的概念，奥曼的定义充分考虑了策略概念的时间方面。事实上，与策略游戏不同，策略可以简单地简化为一组动作（参见[14]），扩展形式游戏中的策略不仅表达了接下来将发生的动作序列，而且还表达了将在游戏的每个顶点发生的动作。[10] 提出了一种逻辑，它能够推理广泛的游戏的认识方面这种逻辑处理几个博弈论的概念，如知识，理性和逆向归纳的概念然而，所有这些概念都是由一个特别的公理化管理的逻辑的原子命题。此外，[10]中提出的扩展形式博弈的逻辑方法是纯粹的语法：没有提出扩展形式博弈的模型理论分析在这篇文章中，我们试图填补这一空白，提出了语义和语法分析广泛的形式游戏在模态逻辑。特别是，我们介绍了一个多模态逻辑解释的Kripke风格的语义集成的概念，行动，战略，知识和偏好，并允许广泛的形式游戏的属性的原因。为了说明逻辑的表达能力，我们在其对象语言中定义了理性和逆向归纳的众所周知的概念，因为它们是根据经济理论定义的。基于这些定义，我们然后提供了奥曼定理的句法证明 虽然存在其他形式化类似定理的逻辑，但这些逻辑都没有足够的表达力来提供语法证明，强调定理的各种要求。例如，虽然[4]提出了一种逻辑，可以正确地定义奥曼定理的陈述，但没有提供它的句法证明，并且它的语言不允许验证当认识条件被削弱时该定理是否成立。事实上，如果一个人实际上只考虑常识被限制在某个有限的水平上，那么游戏的最大深度就代表了定理证明的一个重要变量。 通过考虑这种广泛的游戏的时间维度，我们证明了它的相关性，一些较弱版本的定理的证明我们的意图，在整个本文中，是不是要表明，奥曼定理的句法推导本身是有趣的。相反，我们希望证明，这种分析对于确定关于参与者知识和博弈结构之间关系的特定假设是有用的，这些假设是证明定理所必需的本文的其余部分组织如下。第二节致力于展示我们的行动、策略、知识和偏好逻辑，并对其语言和语义进行定义。然后，在第3节中，我们定义了扩展形式博弈中的理性概念和逆向归纳概念，正如罗伯特·奥曼所定义的那样。第4节提供了奥曼的著名定理的句法证明，E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245247最后，在第5节中，我们对我们的逻辑提出了一些可能的修改，从而导致对奥曼定理的更现实的解释。有关广泛博弈的逻辑的工作将在第6节中讨论。奥曼定理的句法证明的草图2行动、策略、知识和偏好的模态逻辑在这一节中，我们提出了模态逻辑ELEG（广泛博弈的认知逻辑），它整合了行动、策略、知识和偏好的概念。这种逻辑支持对广泛形式的游戏进行推理，其中代理可能不确定其他代理的当前选择2.1语法逻辑ELEG的句法原语是代理的有限集合Agt，原子命题的集合Atm，原子动作名称的非空有限集合Act={α1，α2，...，α|法|}，n个整数的非空有限集合I ={0，.，n}。逻辑ELEG的语言L由以下BNF给出χ：：= p|α|反过来我|端|Ki：：=χ|¬ϕ|ϕ∨ϕ|Q|AX系列|[Ki]|X轴其中，p的范围超过Atm，i的范围超过Agt，α的范围超过Act，并且k的范围超过I.公式χ称为原子公式。经典的布尔连接词T，T，、→和Participare以通常的方式从公式α必须读作分别读作最后，end意味着算子Q用于量化当前博弈的策略。Q必须被读为运算符AX用于量化当前扩展博弈的下一个顶点。 AX必须读作“在当前策略中的每个可能的下一个顶点处都这个公式通常被读作“agen t i kno wsthatkindis true”。 X是next的标准时态运算符。公式X必须读作“将是真的下一个此外，还提供了以下缩写：Q=efEXd=ef¬Q¬ϕ<$AX<$AX0d=efAXn+1d=efϕAX（AXn）248E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245defndefC∈CCCCCCCCKi<$[Ki]<$AX≤nd=ef0≤m≤n AXmαid=efX0d=efXn+1d=efα-β-turniϕXXnEXnd=efEX≤nd=ef<$AX<$<$AX≤n<$Q必须读作“对当前扩展博弈的至少一个策略成立”，而EX必须读作“在当前策略中的至少一个可能的下一个顶点中成立”。 KiXn必须被读为运算符AXn和AX≤n分别表示“在从现在开始，沿着当前策略，在正好n步（s）内可以到达的每个顶点中，为真”和“在从现在开始，沿着当前策略，在n步（s）内可以到达的每个顶点中，为真”。最后，对应的对偶算子EXn和EX≤n可以被解释为“在至少一个顶点中，沿着当前策略，从现在起正好在n步内可以到达”和“在至少一个顶点中，沿着当前策略，从现在起在在命题动态逻辑（PDL）中，我们引入了一个连续复合算子我们将动作序列的集合Seq定义为最小集合，使得：对于任何α∈Act，α∈Seq，并且如果α1，α2∈Seq，则α1;α2∈Seq。此外，我们认为Seq n<$Seq是长度为n的动作序列的集合。一个给定的动作序列将会发生，并且在此之后将为真，这一事实可以在对象语言中通过以下定义来定义：0;. ;αn=0≤l≤nXlαlXn我们使用[EKC]作为iC[Ki]的缩写，即每一个年龄段的人都知道，（如果C=，则[E KC]等于T）。然后，我们通过归纳法[EKk]定义，每个自然数k∈N：并且对于所有k≥1，[EK0]d=ef[EKk]d=ef[EK]（[EKk−1]）同样，我们对所有自然数n∈N定义：[CK0]d=ef并且对于所有n≥1，[CKn]d=ef1≤k≤n[EKk][CKn]k表示CC中的每个人都知道，C中的每个人都知道，C中的每个人都知道，依此类推，直到第n层。E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245249Q2.2语义一个策略结构包括一组顶点、一组策略、一个将顶点和策略关联到顶点的后继函数、一个将代理分配到顶点的话轮转换函数。该组顶点包括端顶点。定义2.1[战略结构]战略结构是一个元组T=其中：• V是顶点的非空集合;• Q是全函数Q：V−→Agt，将顶点映射到智能体;• S是V上的一个非空策略集，且每个策略s∈S都是一个全函数s：V−→Act将顶点映射到动作;• next是一个部分函数next：V×S−→V将顶点和策略映射到顶点，使得：C1如果s（w）=sJ（w）则next（w，s）=next（w，sJ）;• EndV是一组端点，使得：C2w∈EndV当且仅当，next（w，s）对每个s都是未定义的。（w）=i意味着在顶点w处轮到代理i玩，并且next（w，s）= w j意味着w j是关于策略s的w的下一个我们称指数为一对（w，s），其中w∈V，s∈S.我们定义H = V ×S为所有指标的集合。请注意，定义2.1中的策略的特定概念考虑了博弈的每个顶点，而不是像博弈论中通常所做的那样仅限于单个参与者的移动。然而，对于每一个s∈S，单个参与人i根据约束C1，在给定顶点选择相同动作的两个策略导致相同的下一个顶点。根据约束C2，结束顶点是不具有下一顶点的顶点定义2.2[后继者]R是顶点上的关系，使得：对任意w，v∈V，wRv当且仅当存在s∈S使得next（w，s）=v.wRv表示顶点v是顶点w的后继。一个广泛的博弈模型只不过是一个战略结构，补充了代理人对战略的知识，代理人的偏好和原子命题的估值的可及性关系定义2.3[扩展博弈模型]扩展博弈模型是一个元组M = T，{Ei|i∈Agt}，{Pi|i∈Agt}，π其中：• T是一种战略结构;• 每个Ei是S上的等价关系，使得：C3如果SEISJ且Q（w）=i，则s（w）=SJ（w）;• 每个Pi是一个全函数Pi：H−→I，它将每个索引映射到一个整数，使得：C4如果next（w，s）=wJ，则Pi（w，s）=k当且仅当Pi（wJ，s）=k;250E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245C5若w∈EndV且s（w）=SJ（w）则Pi（w，s）=Pi（w，SJ）.• π：Atm−→2H是指数上的赋值函数sEisJ意味着智能体i无法区分策略s和策略sJ。Pi（w，s）=k意味着在顶点w处采取的策略s将确保代理i的支付k。约束C3是假设每个代理人都知道他的选择，当轮到他玩[1，5]。约束C4正确地表达了这样一个事实，即在一个广泛形式的博弈中，偏好是建立在历史之上的，其中历史只不过是一个索引序列（w0，s），.，（wn，s），. 使得next（wi，s）=wi+1，对于每 0≤i。根据约束条件C5，两个策略在一个端点上选择相同的动作会导致一个代理的相同的支付。换句话说，在一个端点，一个动作的支付是唯一确定的。定义2.4[真值条件]在给定指数（w，s）下，模型M中公式的真值定义如下：• M，W，S| = pi<$（w，s）∈π（p）;• M，W，S|=<$ iM，w，s| = 0;• M，W，S| =iM，w，s |= m或M，w，s |= 0;• M，W，S|= αis（w）= α;• M，W，S |= turnii <$Q（w）= i;• M，W，S| = endiw ∈ EndV;• M，W，S |= kii <$Pi（w，s）= k;• M，W，S|如果next（w，s）被定义，则M，next（w，s），s |= 0;• M，W，S| = Q iM，w，sJ|对于所有的sJ∈ S，• M，W，S| = AXiM，wJ，s|对于所有的wJ∈V，使得wRwJ;• M，W，S|=[Ki]iM，w，sJ|对于所有sJsuc h，在广义博弈模型M i <$M，w，s中，公式ψ成立|对于V中的每个顶点w和S中的每个策略s， 是ELEG-有效（注明|=）i在所有扩展博弈模型中均为真。如果不符合ELEG-valid标准，则表示ELEG-合格。2.3一些有效性表1提供了ELEG有效性的详尽列表，这些有效性足以在第4节中提供奥曼定理的句法证明让我们提供价值P erm[Ki]，AX作为示例。 假设M，w，s|=[Ki]AX，对于任意ELEG模型M。这相当于说M，w，sJ|= AX对所有sJ，使得sEisJ，这反过来等价于说M，wJ，sJ|对于所有的（wJ，sJ），使得sEisJ和wRwJ。后者相当于说M，wJ，s|=[Ki]n，对于所有wJ，使得wRwJ，反过来，等于s，并且M，w，s|=AX[Ki]在续集中，我们将写ELEG，意思是可以通过以下方式导出：E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245251（CPL）（S5Q）（S5[Ki]）（KX）（KAX）（DetX）（EndVert）（PerfectInfo）（PermQ，AX）（NxtVert）（Perm[Ki]，AX）（TurnStr）（TimeVert）（Aware）（CompletePref）（SinglePref）经典命题逻辑的所有原理Q的所有S5原则[Ki]X的所有K原则AX的所有K原则X的endParticipQ XQ→[Ki]QAXParticipAXQQXQParticipAXQ[Ki]AXParticipAX[Ki]turni→QturniAX→ X转角i→（α→[Ki]α）Kik∈Iki→<$hi，如果ki=h（OneAct）αα∈Act（单幕）如果α β则α→ <$β（TurnTaking）i∈Agt反过来我（单圈）（TimePref）turni→<$turnj，如果i=/J<$end→（kiParticipateXki）（EndAct）（StrAct）（end<$α<$ki）→Q（α→ki）（α<$XQ<$）→Q（α→X<$）表1ELEG的一些有效性表1中给出的原则列表。一个完整的公理化逻辑ELEG的研究被推迟到未来的工作。3逆向归纳与理性我们在这里定义了奥曼对外延形式博弈的认识论分析中的两个基本概念为了便于以后证明奥曼然而，我们应该注意到，逆向归纳和理性的更一般的定义可以很容易地在ELEG中表达。252E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）2453.1逆向归纳逆向归纳的概念代表了从游戏的每个端点开始，以确定最佳行动序列的时间向后推理的过程这种方法通常用于计算序贯博弈中的子博弈完美纳什均衡逆向归纳（BI）解决方案在一个E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245253我我我深度为n的游戏（即，到达游戏的结束顶点需要最多n步）可以通过迭代过程n次来计算，因为一个状态下的BI解依赖于每个可能的连续状态下的BI解。因此，第一步BI解决方案（n= 0）对应于最后一个玩家在游戏的每个可能的结束顶点处进行游戏的偏好最大化在n（n >0）步之后的BI解对应于当前参与者偏好的最大化在ELEG中，n步后BI解的递归形式定义如下。对于n= 0的情况，我们定义：BI0d=EF结束时间i∈Agt，k∈I（turnikiQ（h∈I：h≤kh（i））对于每个n >0，我们定义：BInd=有效期i∈Agt，k∈I（turnikiAX（BIn−1h∈I：h≤kh（i））因此：M，w，s| = BIn当且仅当当前策略s，当从顶点w开始时，对应于可以在n步中计算的逆向归纳解。3.2认识理性下面的ELEG定义描述了奥曼对广泛形式博弈的认知分析中假设的理性概念1、A=B= A=h（i））k∈Ih∈I：h≤kRatend意味着一个代理i在一个结束顶点（即在博弈的某个结束顶点）是理性的，当且仅当我选择一个使他的个人收益最大化的行动。请注意，在这种情况下，理性并不依赖于任何认知成分。（1）A=（Kik∈Ih∈I：h≤kRat<$iend意味着年龄nti在nyi中间顶点（不是博弈结束顶点的nynde）处是理性的，当且仅当我选择了一个行动，使得他认为可能发生的事情不会严格地被他会考虑的其他未来所支配，如果他选择了任何其他行动。换句话说，由于每个可能的下一个顶点对应于i的一个254E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245M我我我选的）。Ratid=efRatendRat<$end注意，关于合理性的内省由ELEG的以下有效公式表示：Rati参与[Ki]Rati4Aumann定理的一个句法证明如前一节所述，奥曼定理的一个基本假设是博弈处于“一般位置”，即博弈的每一个历史都与每个代理的唯一偏好值相关联。这个重要的概念可以在逻辑ELEG中以如下方式定义GenPosnd=efAX≤nQ（（kiend）→Q（endParticiki））0≤h≤nk∈I，i∈Agt，n∈Seqh在奥曼定理的句法证明中下面的结构Depthn意味着换句话说，无论将来选择什么动作，都将在n步内到达终点。因此，这一概念可通过以下ELEG公式得到深度nd=ef（QX）nend这个假设在奥曼的原始定理中没有说明，这里只用来简化形式证明。然而，应该注意的是，任何广泛的游戏都可以用具有统一深度的广泛游戏来表示（即通过添加额外的非信息性动作和偏好）。根据奥曼• 游戏结束了，• 博弈具有从当前顶点开始的均匀的n度深度• 博弈处于一般位置;• 存在直到至少n层的常识，即在每个未来顶点（直到深度n），所有代理都是理性的。定理4.1对于每个n，m∈N，使得n≤m，我们有：►ELEG（[CKAgt]n≤n（i∈Agt大鼠i）DopplerDepthnDopplerGenPosn）→BInE. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245255我注意，定理4.1的证明仅需要证明m=n的情况因为公理T适用于每一个[Ki]modal操作者。附录中定理4.1的证明指出了需要讨论的几点。定理中的一个强有力的假设是关于所使用的比率的类型。事实上，奥曼定理在假设中考虑了实质合理性，这意味着在博弈的每个顶点，参与者都是理性的。这样的定义是值得批评的，因为它要求参与者在给定某种预期策略下永远无法到达的顶点上保持均匀的比例根据Stalnaker[19]1，一个更现实的理性概念应该只考虑实际到达的顶点。然而，后一种定义并不能保证逆向归纳法的解。我们对该定理的证明表明，实质合理性的这一定义对于均衡解的推导确实很重要。更确切地说，在定理4.1的证明中使用公理Perm[Ki]，AX表明，关于实质合理性的常识不仅现在必须为真，而且在未来的每个顶点上都必须为真。显然，公理Perm[Ki]，AX是非常强大的，因为它假设玩家在游戏开始时就知道这仅仅意味着玩家不能通过游戏学习任何东西5更方便的知识根据前面对奥曼定理的句法证明的分析首先，我们可以从附录中的句法证明中注意到，奥曼定理可以通过对认知算子的重新解释而被削弱。事实上，定理4.1中使用公理T的每个证明步骤对于S5知识操作器[Ki]仍然可以使用KD45原理来提供。这样的观察意味着一个简单的信念概念（不一定是真实的）足以证明奥曼定理的详细证明附录中的4.1表明，这种认知算子的弱化主要是通过公理意识（AxiomAware）实现的，公理意识要求代理人对自己的行为进行自省。换句话说，代理人总是毫无疑问地相信他们实际上会执行什么此外，认知算子仍然是不切实际的，因为它限制代理只考虑静态的不确定性的战略（即代理有相同的不确定性，无论他们在哪个顶点的战略），因此防止他们通过游戏学习为了更加现实，我们本文通过对每个主体i∈Agt和顶点w∈W的策略的等价认知关系Ew来解释认知模态算子。在这种情况下，代理人鉴于认识关系的这种变化，知识的真值条件[12]参见[13]。256E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245我我我我我我我我我我运算符变为：• M，W，S|=[Ki]iM，w，sJ|对于所有sJsuc h，考虑到这个新的认识关系Ew，先前的约束C3必须：重新拟订如下：C3如果sEwsJ且Q（w）=i，则s（w）=s（w）J此外，需要引入以下约束以保持公理Perm[Ki]，AX如表1所示：C6如果sEvsJ和wRv，则sEwsJC7如果sEwsJ和wRv，则sEvsJ根据约束C6，代理将永远不会忘记他们当前的不确定性在每个可达顶点的策略。换句话说，C6仅仅意味着在整个博弈过程中，智能体总是能够完美地回忆起他们过去的不确定性。根据约束C7，智能体总是知道他们未来的不确定性在每个可达顶点的策略。换句话说，C7意味着智能体将永远无法丢弃策略，因此随着时间的推移而学习。让我们提供对应于约束C6的公理：（Perm[K]，AX）[Ki]AX→AX[Ki]AX请注意，公理P erm[K]，AX只是表1中初始公理P erm[Ki]，AX的一个周版本。在约束C6的A条件中清楚地示出了连同其相应的公理Permn[K]，AX都服从定理4.1的结构定理。这样的观察简单地意味着奥曼然而，这一分析也表明，奥曼定理要求代理人通过游戏有完美的回忆。换句话说，要使定理正确，玩家在时间推进的过程中不应该忘记任何事情。6相关作品我们并不是第一个对广泛的游戏进行逻辑分析的人。已经提出了几个逻辑系统，支持这类游戏的推理我们在这里讨论其中的一些系统，并将它们与我们的逻辑ELEG进行比较。在[21]中，van Bentham使用不同的模态语言分析了扩展游戏，例如命题动态逻辑（PDL），具有逆的PDL和模态强制语言，该语言允许表达玩家在给定的扩展游戏中可以带来什么 此外，他还研究了各种基于互模拟的博弈等价概念。虽然vanBentham展示了如何用认知算子扩展PDL，E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245257游戏与不完美的信息，他不考虑理性的概念，这是一个基本要素，奥曼值得注意的是，与我们的逻辑ELEG不同，标准PDL将无法定义这样的概念，因为它既不能识别将要使用的当前策略，也不能表达在当前策略的每个可能的下一个顶点上什么是真的（这是通过ELEG中的运算符AX完成的）。此外，我们的逻辑ELEG表明，在对象语言中明确定义策略-如PDL中所做的那样-对于表达有趣的博弈论概念（如合理性和逆向归纳）是不必要的。与van Benthem的工作相关的然而，Ramanujan Simon没有处理广泛游戏的认知方面，因为他们的逻辑没有代表玩家认知状态的算子。在[15]中提出的博弈逻辑也缺乏认知算子，因此阻碍了认知理性概念的形式化和奥曼定理的逻辑分析。Bonanno他提出了一种动态逻辑的变体，扩展了（分支）未来和（线性）过去的时间运算符，并展示了他的逻辑如何[2]但是，像Ramanujan Simon同样的评论也适用于最近的一些工作[20]，它提出了一个类似的逻辑方法，广泛的游戏，而不考虑认知方面。[28]和[25]中提出的基于ATL的广泛游戏方法更接近我们当前的方法。例如，在[28]中，提出了一种具有显式策略的ATL（交替时间时序逻辑）变体，称为ATEL（具有显式策略的交替时间逻辑），它允许定义诸如逆向归纳的解概念。 与ATL相比，ATEL的有趣之处在于，人们可以显式地推理对象语言中的策略。然而，像Ramanujan Simon和Bonanno一样，ATEL错过了定义奥曼合理性概念所必需的认识算子。ATEL和我们的逻辑ELEG之间的另一个重要区别是，在ATEL中，公式是关于状态来解释的，而在ELEG中，它们是关于状态/策略对来解释的（在这个意义上，ELEG语义是二维的）。后者是一个优势，因为不同于ATEL，在ELEG中可以推理在当前策略的每个可能的下一个顶点处什么是真的。我们已经表明，这是基本的表达对象语言奥曼的在[27]中，作者提出了一种通过使用基于类型论的纯证明理论方法来证明Aumann定理的替代方法区别于2.Bonanno博弈树的每个未来顶点的情况，（2）过去每个顶点的情况，（3）在博弈树的每个预测的未来顶点处将是什么情况，以及（4）在预测今天的每个过去顶点处一直是什么情况。258E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245Vestergaard等人的方法，我们的方法基于模态逻辑的优势相结合的证明理论分析广泛的游戏-这是我们在第4节所做的-与模型理论语义。7结论在本文中，我们引入了一个逻辑框架，它提供了一种替代的方式来表示广泛形式的游戏，而不是它们在经济学中的通常规范。我们证明了我们的逻辑对于我们推理动态认知博弈的目的来说是非常普遍的，正如众所周知的理性和逆向归纳概念所说明的那样。虽然这些概念在经济学中得到了广泛的研究，但迄今为止很少有人提出逻辑分析。虽然一些相关的作品讨论并提出了一些逻辑方法，以认识推理在这种广泛的游戏，没有这些定义的逻辑表达足以表示语法的认识概念和均衡解决方案。通过奥曼定理的形式化句法证明除了提供一个完整的公理化我们的逻辑，我们打算在未来的工作中，调查一些扩展的逻辑ELEG。虽然这里提出的逻辑语言仅限于对未来的推理，但当前语义学也可以扩展到对过去和每一种可能的反事实情况的推理这是我们也考虑进一步研究的另一个研究方向。引用[1] R. J·奥曼逆向归纳法与合理性常识。博弈与经济行为，8：6[2] R. J. 奥曼互动认识论I：知识。International Journal of Game Theory，28（3）：263[3] R. J. Aumann和A.布兰登伯格纳什均衡的认知条件。Econometrica，63：1161[4] A. Baltag，S. Smets和J.A.兹维斯帕保持Synthese，169（2）：705-737，2009.[5] P. Battigalli和G.博南诺 关于信仰、知识和认知基础的最新结果 博弈论经济学研究，53：149[6] G. 博南诺分支时间、完全信息博弈和逆向归纳法。博弈与经济行为，36（1）：57[7] G.博南诺模态逻辑与博弈论：两种可供选择的方法。Risk Decision and Policy，7（3）：309[8] G.博南诺有序支付博弈中理性的句法分析。在L0 FT 2008的Proc.，第59北京：北京大学出版社.[9] A.布兰登伯格博弈中的知识与均衡。Journal of Economic Perspectives，6：83-101，1992.[10] B.德布鲁因解释博弈：论博弈论解释的逻辑。荷兰阿姆斯特丹大学博士论文，2004年。E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245259Agt=Agt[11] H.金提斯理性的界限：博弈论与行为科学的统一。普林斯顿大学出版社，2009年。[12] J.Y. 哈尔彭实质性 合理性 和 落后诱导博弈与经济行为，37（2）：425[13] E. Lorini和F.莫伊桑广泛博弈的认知逻辑 Rapport de recherche IRIT/RT-2011-4-FR，IRIT，Uni versit'ePaulSabatier，图卢兹，2011年。可在ftp://ftp.irit.fr/IRIT/LILAC/Reports/epistemic_logic_extensive_games.pdf上找到。[14] E. Lorini和F.施瓦岑特鲁伯认知游戏的模态逻辑Games，4（1）：478[15] R. 帕里克游戏的逻辑及其应用。Annals of Discrete Mathematics，24：111[16] R. Ramanujam和S.西蒙战略的逻辑结构。在LOFT 7的Proc.中，第151-176页。北京：北京大学出版社.[17] R. Ramanujam和S. E.西蒙结构化策略博弈的动态逻辑。 在KR 2008的Proc.，49-58页中AAAI Press，2008.[18] O. 罗伊行动之前的思考：意图，逻辑，理性选择。荷兰阿姆斯特丹大学博士论文，2008年。[19] R.潜行者博弈中的信念修正：正向和反向归纳。Mathematical Social Sciences，36（1）：31[20] D.苏罗维克扩展博弈的时间逻辑方法。Studies in Logic，Grammar and Rhetoric，7（20）：69[21] J·范·本瑟姆广泛的游戏作为过程模型。Journal of Logic，Language and Information，11（3）：289[22] J·范·本瑟姆博弈中的理性动态与认知逻辑。International Game Theory Review，9（1）：13[23] J. van Benthem，E. Pacuit和O.罗伊走向游戏理论：游戏和互动的逻辑视角Games，2（1）：52[24] J. van Bentham，S. van Otterloo和O.罗伊游戏中的偏好逻辑、条件和解决方案概念。 InH. Lagerlund，S.Lindstréom和R. Sliwinski，editors，M odalityMatters，pages61-76. 乌普萨拉大学，2006年。[25] W. van Der Hoek，W. Jamroga和M.伍尔德里奇战略推理的逻辑。在AAMAS'05的Proc.ACM，2005年。[26] W. van der Hoek和M. Pauly.游戏和信息的模态逻辑。在P. Blackburn，J. van Benthem和F.Wolter，editors，Handbook of Modal Logic（3）.爱思唯尔，阿姆斯特丹，2006年。[27] R. Vestergaard，P. Lescanne，and H.小野 Aumann定理的归纳和模态证明理论关于理性技术报告IS-RR-2006-009，日本科学技术高等研究所，2006年。[28] D. Walther ， W. van der Hoek 和 M. 伍 尔 德 里 奇 具 有 显 式 策 略 的 交 替 时 序 逻 辑 。 在 TARK'07的Proc.ACM，2007年。A附录由于篇幅的限制，我们只给出了奥曼定理的一个简单证明下面是证明定理4.1所需的引理：(i)ELEG[CKn+1]AXnAllRat →[CKn[AXnAllRat(ii)ELEG（Depthn此外，为了使定理4.1的证明更容易理解，我们使用以下缩写：AllRatdefi∈Agt 大鼠i260E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245Agt0AgtAgtAgtAgt我我AgtAgt∈∈01 - 02- 03-02A.1定理4.1的句法证明这是直截了当地表明，奥曼►李晓（0≤m ≤n[CKm]AXmAllRat（所有Rat）深度n（所有GenPosn）→BIn因此，我们归纳地证明了这个定理基本病例n=0：在这里，我们证明了ELEGAllRat的最后一步是ELEGGenPos0→BI0。(i)ELEG（AllRat→i∈Agt（endnturninh∈I：k≥hhi）我根据Rati和Ratend的定义，以及AxiomTurnTaking;(ii)BELELEG（AllRat和BELGenPos0）→BI0i和BI的定义;归纳案例：设n∈N，我们证明如果定理对所有k≤n成立，则对n+1成立(i) 李晓波（0≤m ≤n+1[CKm]AXmAllRat深度n+1（GenPosn+1）Agt→AX（0≤m≤n [CKm]AXmAllRat（所有Rat）（所有Rat深度n）（所有GenPosn）通过深度n+1和GenPosn+1的定义，引理i和公理Perm[K]，AX（或Perm）;(ii) 李晓波（Agt0≤m ≤n+1我[CKm]AXmAllRat深度n+1（GenPosn+1）Agt[Ki]，AX→[EK1]]AX（ 0≤m≤n [CKm]AXmAllRat（所有Rat）（所有Rat深度n）（所有GenPosn）通过深度n+1和GenPosn+1的定义，以及公理Perm[K]，AX（或Perm）;(iii) 李晓波（0≤m≤n我[CKm]AXmAllRat（所有Rat）深度n（所有GenPosn）→BIn[Ki]，AX通过归纳;(iv)ELEG（0≤m≤n+1Agt[CKm]AXmAllRat深度n+1（GenPosn+1）→AXBIn[EK1]AXBIn第一，第二，第三，(v)ELEG（0≤m≤n+1[CKm]AXmAllRat深度n+1（GenPosn+1）→AX（[001 pdf 1st-31files][001 pdf 1st-31files][001 pdf1st-31files][001 pdf 1st-31files]（k∈Iki<$BIn<$[Kj]BIn<$Depthn<$GenPosn）通过iv，Depthn+1和GenPosn+1的定义，公理CompletePref和Perm[K]，AX（或Perm[K]，AX）和[Ki]的公理4(vi) 李晓波（0≤m ≤n+1[CKm]AXmAllRat深度n+1（GenPosn+1）→i∈Agt，α∈Act转i<$αi<$$>[Ki]αi<$Xk∈IQ（BIn→ki）由v，引理ii，和公理TurnTaking，TimeVert，OneAct，和Aware;(vii) 李晓波（0≤m ≤n+1[CKm]AXmAllRat深度n+1（GenPosn+1）→i∈Agt，α∈Act转i<$αi<$$>[Ki]αi<$k∈IQ（αi→X（BIn→ki））由vi和公理StrAct;(viii) 李晓波（0≤m ≤n+1[CKm]AXmAllRat深度n+1（GenPosn+1）AgtE. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245261Agt→iAgtturniXBIn[Ki]XBInkIX（BIn→ki）<$[Ki]X（BIn→ki）byvii和iv，公理PerfectInfo和时间Vert，公理TforQ，公理Kfor[Ki]，和bof原理;262E. Lorini，F.Moisan/Electronic Notes in Theoretical Computer Science 278（2011）245AgtAgtAgt→∧ ∧→∈AgtAgtAgtAgtAgt∈∈∈≤AgtAgtAgt(ix) 李晓波（0≤m ≤n+1[CKm]AXmAllRat深度n+1（GenPosn+1）→i∈Agt ，k∈I转i<$Xki<$[Ki]Xkibyv