博弈語義

什么是博弈語義

博弈語義是一種邏輯的語義，基于在博弈論概念上的真理或有效性的概念，比如對一個游戲者存在一種獲勝策略。保爾·洛倫茨首先在1950年代晚期為邏輯介入了博弈語義。此后在邏輯中已經研究了很多不同的博弈語義。博弈語義也已經應用于編程語言的形式語義。

Lorenzen和KunoLorenz的主要動機是為直覺邏輯找到一種博弈論(他們的術語是“對話式”DialogischeLogik)語義。Blass首先指出在博弈語義和線性邏輯之間的聯系。這個路線進一步由SamsonAbramsky、RadhakrishnanJagadeesan、PasqualeMalacaria和獨立的由MartinHyland和LukeOng發展，對合成性加以特別強調，就是遞歸的在語法上定義策略。使用博弈語義，上面提及的作者們解決了長期存在的為可計算函數的編程語言定義完全抽象模型的問題。從此，博弈語義成為各種編程語言的完全抽象的語義模型，導致了軟件模型檢查的軟件驗證的新的語義制導的方法。

博弈語義下的量詞

博弈語義的基礎性考慮已經被JaakkoHintikka和GabrielSandu更加強調，特別是為了友好獨立邏輯(IF邏輯，更加新近的友好信息邏輯)，它是帶有分支量詞的邏輯。復合性原理被認為對這些邏輯失敗，所以Tarski主義的真理定義不能提供合適的語義。

要解決這個問題，量詞被給予博弈論意義，全稱量詞和存在量詞表示一個游戲者從這個域做的一個選擇。在全稱情況下，給游戲者的自然名字是“證偽者”；在存在情況下，是“證實者”。注意一個單一的反例證偽一個全稱量化陳述，而一個單一的例子足夠證實一個存在量化陳述。WilfridHodges提議了復合語義并證明了它等價于給IF-邏輯的博弈語義。基礎性考慮已經推動了其他人的工作，比如Japaridze的可計算性邏輯。