博弈语义

博弈语义

什么是博弈语义

博弈语义是一种逻辑的语义，基于在博弈论概念上的真理或有效性的概念，比如对一个游戏者存在一种获胜策略。保尔·洛伦茨首先在1950年代晚期为逻辑介入了博弈语义。此后在逻辑中已经研究了很多不同的博弈语义。博弈语义也已经应用于编程语言的形式语义。

Lorenzen和KunoLorenz的主要动机是为直觉逻辑找到一种博弈论(他们的术语是“对话式”DialogischeLogik)语义。Blass首先指出在博弈语义和线性逻辑之间的联系。这个路线进一步由Samson Abramsky、Radhakrishnan Jagadeesan、Pasquale Malacaria和独立的由Martin Hyland和LukeOng发展，对合成性加以特别强调，就是递归的在语法上定义策略。使用博弈语义，上面提及的作者们解决了长期存在的为可计算函数的编程语言定义完全抽象模型的问题。从此，博弈语义成为各种编程语言的完全抽象的语义模型，导致了软件模型检查的软件验证的新的语义制导的方法。

博弈语义下的量词

博弈语义的基础性考虑已经被Jaakko Hintikka和Gabriel Sandu更加强调，特别是为了友好独立逻辑(IF逻辑，更加新近的友好信息逻辑)，它是带有分支量词的逻辑。复合性原理被认为对这些逻辑失败，所以Tarski主义的真理定义不能提供合适的语义。

要解决这个问题，量词被给予博弈论意义，全称量词和存在量词表示一个游戏者从这个域做的一个选择。在全称情况下，给游戏者的自然名字是“证伪者”；在存在情况下，是“证实者”。注意一个单一的反例证伪一个全称量化陈述，而一个单一的例子足够证实一个存在量化陈述。Wilfrid Hodges提议了复合语义并证明了它等价于给IF-逻辑的博弈语义。基础性考虑已经推动了其他人的工作，比如Japaridze的可计算性逻辑。