ゲーム意味論（ゲームいみろん、Game Semantics）とは、ゲーム理論的概念（プレイヤーの勝利戦略の存在など）に基づいた論理の意味論の手法である。1950年代後半にパウル・ローレンツェンが提唱した。その後、様々なゲーム意味論が研究されてきた。ゲーム意味論はプログラミング言語の形式意味論にも適用されてきた。最も単純なゲーム意味論の応用として、命題論理への適用がある。各論理式を2人のプレイヤーの間で行われるゲームに見立てる。プレイヤーは「立証者; Verifier」と「偽証者; Falsifier」と呼ばれる。立証者はその論理式内の全ての論理和の「所有権」を有し、偽証者は同様に全ての論理積を所有する。このゲームの「手」で行うことは、論理演算子を所有するプレイヤーがその演算子の一方の枝を選ぶことである。ゲームはその選ばれた部分論理式について続行され、その論理式を制御している演算子を所有するプレイヤーが次の手を行うことができる（全体が論理和なら立証者が一方の枝を選ぶ）。こうして、論理和も論理積も含まれない単純な式となるまで続ける。ここで、その式が真であれば立証者の勝ちで、偽であれば偽証者の勝ちである。立証者が勝利戦略を持つ場合、元の論理式も真であると見なされ、逆に偽証者に勝利戦略があれば、偽と見なされる。論理式に否定や含意が含まれる場合、もっと複雑な技法が使われる。例えば、否定は否定する対象が偽であれば真となるので、2人のプレイヤーの役割を逆転させる効果がある。より一般化して、ゲーム意味論は述語論理にも適用される。新たなルールとして、支配的な量化子をその所有者（立証者は存在記号を所有し、偽証者は全称記号を所有する）が削除でき、その際に束縛変項の全ての出現をプレイヤーの選んだ任意の定項で置き換える。このとき、全称量化では1つの反例で偽となり、存在量化では1つの例で真となることに注意されたい。このようなゲームは全て完全情報ゲームである。2人のプレイヤーは論理式を構成する各項の真理値を知っており、常に先を読む。ローレンツェンと Kuno Lorenz の目的は、直観論理のためのゲーム理論的な意味論を見出すことであった。Blass で初めて線形論理とゲーム意味論の関連が指摘された。この方向で Samson Abramsky、 Radhakrishnan Jagadeesan、Rasquale Malacaria や、（それとは別に）Maritin Hyland と Luke Ong が研究を進め、合成性に重点を置いた（すなわち、文法から機能的に戦略を定義する）。ゲーム意味論を使って、これらの研究者は長年の課題であったプログラミング言語 PCF の完全抽象モデルの定義に成功した。その結果、ゲーム意味論によって各種プログラミング言語の完全抽象モデルが構築され、ソフトウェアのモデル検査の新たな形式的手法が導かれた。ゲーム意味論の基礎研究はヤーッコ・ヒンティッカと Gabriel Sandu によって進められ、特に分岐量化子を持つ（IF-Logic）が研究された。このような論理では合成性の原則が成り立たず、従ってタルスキ的真理意味論では意味論として不適であった。この問題を解決するため、量化子にゲーム意味論での意味を与えた。手法は命題論理と同様だが、プレイヤーはそれ以前の相手の「手」に関して必ずしも完全情報を持たない。Wilfrid Hodges は Compositional Semantics（合成的意味論）を提案し、それがIF-Logicのゲーム意味論と等価であることを証明した。基礎研究は他の研究を誘発し、Japaridze は Computability Logic（計算可能性論理）を生み出した。

出典:wikipedia