博弈语义
| 语义学 | ||||||||
|---|---|---|---|---|---|---|---|---|
| 形式语义学 | ||||||||
|
||||||||
博弈语义是一种基于博弈论定义真或有效性等逻辑概念的形式语义，比如游戏者的赢策略。保尔·洛伦茨首先在1950年代晚期为逻辑引入了博弈语义。此后在逻辑中已经研究了很多不同的博弈语义。博弈语义也已经应用于编程语言的形式语义。
直觉主义逻辑，指称语义，线性逻辑
保罗·洛伦岑和Kuno Lorenz的主要动机是为直觉主义逻辑找到一种博弈论（他们的术语是"对话式" Dialogische Logik）语义。Blass （页面存档备份，存于互联网档案馆）首先指出在博弈语义和线性逻辑之间的联系。这个路线进一步由Samson Abramsky、Radhakrishnan Jagadeesan、Pasquale Malacaria和独立的由Martin Hyland和Luke Ong发展，对组合性加以特别强调，就是递归的在语法上定义策略。使用博弈语义，上面提及的作者们解决了长期存在的为可计算函数的编程语言定义完全抽象模型的问题。于是，在博弈语义的基础上，产生了为各种编程语言提供了完全抽象的语义模型，以及由此产生了用软件模型检测进行软件验证的新的语义导向的方法。
量词
博弈语义的基础性考虑被Jaakko Hintikka和Gabriel Sandu更加强调，特别是为Independence Friendly逻辑（IF逻辑，更加新近地Information-friendly逻辑）提供语义。IF逻辑是带有分枝量词的逻辑，一度，组合原则被认为对IF逻辑不成立，所以无法利用Tarski的真理定义为此逻辑定义合适的语义。为解决这个问题，量词被赋予博弈论的意义，特别的，这种方法和经典命题逻辑的博弈论语义类似，区别仅在于博弈者并非总是掌握对弈者前面的行动的完全信息。Wilfrid Hodges给出了组合语义，并证明了它和IF-逻辑的博弈语义等价。基础性考虑已经推动了其他的工作，比如Japaridze的可计算性逻辑。
参见
- Independence Friendly逻辑
- 直觉主义逻辑
- 线性逻辑
- 可计算性逻辑
- 交互式计算
- 直觉主义
- BHK释义
- 直觉类型论
- 经典逻辑
- 中间逻辑
- 构造性证明
- Curry-Howard对应
- 可计算性逻辑
引用
- Krabbe, E. C. W., 2001. "Dialogue Foundations: Dialogue Logic Revisited," Supplement to the Proceedings of The Aristotelian Society 75: 33-49.
- K. Lorenz, P. Lorenzen: Dialogische Logik, Darmstadt 1978
- P. Lorenzen: Lehrbuch der konstruktiven Wissenschaftstheorie, Stuttgart 2000 ISBN 3-476-01784-2
- R. Inhetveen: Logik. Eine dialog-orientierte Einführung., Leipzig 2003 ISBN 3-937219-02-1