博弈語義

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

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

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

Lorenzen和Kuno Lorenz的主要動機是為直覺主義邏輯找到一種博弈論（他們的術語是"對話式"Dialogische Logik）語義。Blass首先指出在博弈語義和線性邏輯之間的聯繫。這個路線進一步由Samson Abramsky、Radhakrishnan Jagadeesan、Pasquale Malacaria和獨立的由Martin Hyland和Luke Ong發展，對組合性加以特別強調，就是遞歸的在語法上定義策略。使用博弈語義，上面提及的作者們解決了長期存在的為可計算函數的編程語言定義完全抽象模型的問題。於是，在博弈語義的基礎上，產生了為各種編程語言提供了完全抽象的語義模型，以及由此產生了用軟件模型檢測進行軟件驗證的新的語義導向的方法。 ^[2]