Loading article…
ゲーム意味論は、形式意味論へのアプローチの一つであり、真理や妥当性の概念を、プレイヤーにとっての必勝戦略の存在といったゲーム理論的概念に基づいて構築する。この枠組みでは、論理式は2人のプレイヤー間のゲームを定義するものとして解釈される。この用語は、対話論理（1950年代からドイツのポール・ローレンツェンとクノ・ローレンツによって開発された）やゲーム理論的意味論（フィンランドのヤッコ・ヒンティッカによって開発された）など、関連性はあるものの異なる複数の伝統を包含する。
ゲーム意味論は、静的な真理値割り当てではなく、論理的推論の動的で相互作用的な性質を強調することで、従来のモデル理論的アプローチから大きく逸脱しています。古典論理、直観主義論理、線形論理、様相論理など、さまざまな論理体系に対して直感的な解釈を提供します。このアプローチは、古代のソクラテス対話、中世の義務論、構成的数学と概念的に類似しています。1990年代以降、ゲーム意味論は理論計算機科学、特にプログラミング言語の意味論、並行性理論、計算複雑性の研究において重要な応用を見出しています。
1950年代後半、ポール・ローレンツェンは論理学におけるゲーム意味論を初めて提唱し、その後クノ・ローレンツによってさらに発展させられた。ローレンツェンとほぼ同時期に、ヤーッコ・ヒンティッカは、文献ではGTS （ゲーム理論的意味論）として知られるモデル理論的アプローチを開発した。それ以来、論理学において様々なゲーム意味論が研究されてきた。
シャヒド・ラフマン（リール第3大学）とその共同研究者たちは、対話論理を論理的多元主義に関連する論理的および哲学的問題を研究するための一般的な枠組みへと発展させた。1994年以降、これは永続的な影響を及ぼす一種のルネサンスを引き起こした。この新たな哲学的衝動は、理論計算機科学、計算言語学、人工知能、プログラミング言語の形式意味論の分野でも並行して刷新された。例えば、アムステルダムのヨハン・ファン・ベンテムとその共同研究者たちは論理とゲームの接点を徹底的に研究し、ハノ・ニッカウはゲームを用いてプログラミング言語における完全抽象化の問題に取り組んだ。ジャン＝イヴ・ジラールによる、一方では数学的ゲーム理論と論理、他方では議論理論と論理の接点における線形論理の新たな成果は、 S. アブラムスキー、J. ファン・ベンテム、A . ブラス、 D. ギャベイ、M. ハイランド、W. ホッジス、R. ジャガディーサン、G. ジャパリゼ、E. クラッベ、L. オング、H. プラッケン、G. サンドゥ、D. ウォルトン、J. ウッズなど、多くの研究者の研究につながり、彼らは論理を動的な推論の道具として理解する論理の新しい概念の中心にゲーム意味論を据えた。証明論と意味論に関する別の視点もあり、証明論の文脈で理解されるウィトゲンシュタインの「使用としての意味」パラダイムでは、いわゆる還元規則（導入規則の結果に対する除去規則の効果を示す）が、命題から引き出すことができる（直接的な）帰結の説明を形式化するのに適切であると見なされるべきであり、それによって言語計算におけるその主要な結合子の機能/目的/有用性を示すべきであると主張している（de Queiroz (1988)、de Queiroz (1991)、de Queiroz (1994)、de Queiroz (2001)、de Queiroz (2008)、de Queiroz (2023)、de Queiroz (2025a)、de Queiroz (2025b)）。
ゲーム意味論の最も単純な応用例は命題論理である。この言語の各論理式は、「検証者」と「反証者」と呼ばれる2人のプレイヤー間のゲームとして解釈される。検証者は論理式内のすべての選言を「所有」し、反証者は同様にすべての論理積を所有する。ゲームの各ターンは、主結合子の所有者がその分岐の1つを選択することで構成される。その後、その部分論理式でプレイが続き、主結合子をコントロールしているプレイヤーが次のターンを行う。2人のプレイヤーが原始命題を選択した時点でプレイは終了する。この時点で、結果として得られた命題が真であれば検証者が勝者とみなされ、偽であれば反証者が勝者とみなされる。元の論理式は、検証者が勝利戦略を持っている場合にのみ真とみなされ、反証者が勝利戦略を持っている場合は常に偽とみなされる。
式に否定や含意が含まれる場合は、より複雑な手法を用いる必要がある。例えば、否定は否定されるものが偽である場合に真となるべきであり、したがって、2人のプレイヤーの役割を入れ替える効果を持たなければならない。
より一般的には、ゲーム意味論は述語論理に適用できます。新しい規則では、主量化子をその「所有者」（存在量化子の場合は検証者、全称量化子の場合は反証者）が削除し、その束縛変数を、所有者が量化領域から選択したオブジェクトで全ての出現箇所で置き換えることができます。全称量化された命題は単一の反例で反証され、存在量化された命題は単一の例で検証されることに注意してください。選択公理を仮定すると、古典的一階述語論理のゲーム理論的意味論は、通常のモデルベース（タルスキアン）意味論と一致します。古典的一階述語論理の場合、検証者の勝利戦略は、基本的に適切なスコレム関数と証拠を見つけることにあります。たとえば、SがSの等充足可能な文は次のようになります。スコレム関数f (存在する場合) は、偽造者が行う可能性のあるxの選択ごとに存在部分式の証拠を返すことにより、Sの検証者にとっての勝利戦略を実際にコード化します。 [ 1 ]
上記の定義は、Jaakko Hintikka が GTS 解釈の一部として最初に定式化したものです。Paul Lorenzen と Kuno Lorenz による古典論理 (および直観主義論理) のゲーム意味論のオリジナル版は、モデルではなく形式対話における勝利戦略の観点から定義されていました(P. Lorenzen、K. Lorenz 1978、S. Rahman および L. Keiff 2005)。Shahid Rahman と Tero Tulenheimo は、古典論理の GTS 勝利戦略を対話の勝利戦略に変換し、またその逆も行うアルゴリズムを開発しました。
形式対話と GTS ゲームは無限であり、プレイヤーがいつプレイを終了するかを決定するのではなく、プレイ終了ルールを使用する。 戦略的推論の標準的な手段 (支配戦略の反復的排除または IEDS) でこの決定に到達することは、GTS および形式対話では停止問題の解決と同等であり、人間のエージェントの推論能力を超える。 GTS は、基礎モデルに対して数式をテストするルールでこれを回避し、論理対話は、非反復ルール (チェスの3 回繰り返しに類似) でこれを回避している。 Genot と Jacot (2017) [ 2 ]は、厳しく限定合理性を持つプレイヤーは、IEDS なしでプレイを終了するように推論できることを証明した。
上記を含むほとんどの一般的な論理体系では、そこから生じるゲームは完全情報ゲームである。つまり、2人のプレイヤーは常に各プリミティブの真偽値を知っており、ゲームにおける先行するすべての動きを認識している。しかし、ゲーム意味論の登場により、ヒンティッカとサンドゥの独立性重視の論理体系のように、不完全情報ゲームの観点から自然な意味論を持つ論理体系が提案されている。
ローレンツェンとクノ・ローレンツの主な動機は、直観主義論理のためのゲーム理論的（彼らの用語では対話的、ドイツ語ではDialogische Logik）意味論を見つけることでした。アンドレアス・ブラス[ 3 ]は、ゲーム意味論と線形論理の関連性を最初に指摘しました。この流れは、サムソン・アブラムスキー、ラダクリシュナン・ジャガディーサン、パスクアーレ・マラカリア、そして独立してマーティン・ハイランドとルーク・オンによってさらに発展し、彼らは構成性、つまり構文に基づいて戦略を帰納的に定義することに特に重点を置きました。上記の著者は、ゲーム意味論を用いて、プログラミング言語PCFの完全抽象モデルを定義するという長年の問題を解決しました。その結果、ゲーム意味論は、さまざまなプログラミング言語の完全抽象意味モデルと、ソフトウェアモデル検査によるソフトウェア検証の新しい意味論指向手法につながりました。
シャヒド・ラーマンとヘルゲ・リュッケルトは、対話的アプローチを拡張し、様相論理、関連性論理、自由論理、連結論理といった非古典論理の研究に応用した。最近では、ラーマンとその共同研究者らは、論理的多元主義の議論を目的とした一般的な枠組みへと対話的アプローチを発展させた。
ゲーム意味論の基礎的な考察は、Jaakko HintikkaとGabriel Sanduによってより強調されてきた。特に、分岐量化子を持つ独立性優先論理（IF論理、より最近では情報優先論理）においてである。これらの論理では構成性の原理が成り立たないと考えられていたため、タルスキアン真理定義では適切な意味論を提供できないと考えられていた。この問題を回避するために、量化子にゲーム理論的な意味が与えられた。具体的には、アプローチは古典的な命題論理と同じであるが、プレイヤーは他のプレイヤーの以前の動きについて常に完全な情報を持っているわけではない。Wilfrid Hodgesは構成意味論を提案し、IF論理のゲーム意味論と同等であることを証明した。
さらに最近では、シャヒド・ラフマンとリールの対話論理チームは、内在的推論と呼ばれる直観主義型理論への対話的アプローチによって、対話的枠組み内で依存関係と独立性を実装した。[ 4 ]
ジャパリゼの計算可能性論理は、ゲームを論理の研究や正当化のための技術的あるいは基礎的な手段としてではなく、論理によって奉仕されるべき対象として扱う、極端な意味でのゲーム意味論的論理アプローチである。その出発点となる哲学的立場は、論理は「現実世界をナビゲートする」ための普遍的で汎用的な知的ツールであるべきであり、したがって、現実世界と、そうでなければ意味のない形式体系（構文）との間の橋渡しとなるのは意味論であるため、構文は構文論よりも意味論的に解釈されるべきであるというものである。したがって、構文は二次的なものであり、根底にある意味論に奉仕する限りにおいてのみ興味深い。この観点から、ジャパリゼは、ローレンツェンの直観主義論理へのアプローチを例に挙げながら、既存の対象構文構造に意味論を調整するという、しばしば行われる慣習を繰り返し批判してきた。この考え方は、ゲームは「エージェントのすべての『ナビゲーション』活動の本質、つまり周囲の世界との相互作用に対して、最も包括的で、首尾一貫していて、自然で、適切で、便利な数学的モデルを提供する」ため、意味論はゲーム意味論であるべきだと主張する。[ 5 ]したがって、計算可能性論理が採用する論理構築パラダイムは、ゲームに対する最も自然で基本的な操作を特定し、それらの演算子を論理演算として扱い、次にゲーム意味論的に有効な式の集合の健全で完全な公理化を探すことである。この道筋で、さまざまな種類の否定、連言、選言、含意、量化子、様相を備えた、おなじみまたはなじみのない多数の論理演算子が、計算可能性論理のオープンエンド言語に出現した。
ゲームは、機械とその環境という2つのエージェント間で行われ、機械は計算可能な戦略のみに従うことが求められます。このように、ゲームは対話型の計算問題とみなされ、機械の勝利戦略はそれらの問題の解決策とみなされます。計算可能性論理は、許容される戦略の複雑さの妥当な変動に対して堅牢であることが確立されており、論理に影響を与えることなく、対数空間と多項式時間（対話型計算では一方が他方を意味するわけではありません）まで低くすることができます。これらすべてが「計算可能性論理」という名称を説明し、コンピュータ科学のさまざまな分野における適用可能性を決定します。古典論理、独立性に配慮した論理、および線形論理と直観主義論理の特定の拡張は、特定の演算子または原子のグループを禁止するだけで得られる、計算可能性論理の特別な断片であることがわかります。
