💻 computer science

Two Remarks about Game Semantics of Classical Logic

この論文は、ゲーム意味論に関連するステファノ・ベラルディの未発表の2つの考察を紹介・解説するものである。

原著者： Thierry Coquand

公開日 2026-03-05

📖 1 分で読めます☕ さくっと読める

原著者： Thierry Coquand

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

🎮 全体像：論理は「対話のゲーム」だ

まず、この論文の前提となる世界観を理解しましょう。
通常、数学の証明は「正解か不正解か」を静かに判断するものですが、ここでは**「証明」を「2 人のプレイヤーが繰り広げる対話ゲーム」**として捉えます。

プレイヤー A（∃ロイーズ）： 「何か存在する！」と主張する側（攻撃者）。
プレイヤー B（∀ベルアルド）： 「本当にそうなのか？」と疑う側（防御者）。

このゲームでは、プレイヤー A は**「後戻り（バックトラック）」**ができるのが最大の特徴です。
「あ、間違えた！こっちの選択肢にしよう！」と、過去の選択を取り消してやり直すことができます。この「後戻り」ができる能力こそが、古典論理（排中律などを含む）の強さを表しています。

💡 第 1 の洞察：無限の議論と「誰のせい？」

【シチュエーション】
2 人のプレイヤーが、永遠に終わらない議論（無限のゲーム）を始めたとします。

【ベラルディの発見】
「もし議論が永遠に続くなら、どちらか一方のプレイヤーだけが『無限の責任』を負っていることがわかる」ということです。

🌊 アナロジー：川の流れ
議論の流れを川の流れに例えてみましょう。
川には「支流（過去の選択）」と「本流（現在の選択）」があります。

もし川が無限に流れ続けるなら、それは「ある特定の支流」から流れ出しているはずです。
ベラルディは、「無限に続く議論の正体は、どちらのプレイヤーがその『無限の支流』を作り出したかを特定できる」と指摘しました。

🎯 意味：
ゲームが永遠に終わらない場合、それは単なる偶然ではなく、**「どちらかがルールを破って（あるいは戦略的に）無限ループを作った」**と特定できます。これにより、無限の議論を「超有限（トランスフィニート）」な視点から分析できるようになります。

🎭 第 2 の洞察：「嘘」が勝つ不思議なゲーム

【シチュエーション】
次に、「明らかに嘘（偽）」である命題をゲームにしてみましょう。
通常、嘘は負けるはずですが、このゲームでは**「嘘」を主張するプレイヤー A が、相手の「連続的な」反応に対して勝つ戦略を持っている**ことがありました。

🍳 アナロジー：嘘をついて料理を作る

嘘の命題（★）： 「どんなレシピ（関数）でも、ある材料（x）を選べば、味が 0 になる（f(x)=0）し、別の材料（y）を選べば味が 0 にならない（f(y)≠0）ような料理がある！」
- これは明らかに嘘です。なぜなら、すべての材料が味が 0 になる料理も、すべてが 0 にならない料理も存在するからです。
プレイヤー A の戦略（嘘つき）：
1. 最初は「全部 1 になる料理（f=1）」と主張する。
2. 相手が「じゃあ、x=0 はどう？」と聞いてくる。
3. A は「あ、間違えた！0 は 0 にしよう」と後戻りして料理を変更する。
4. 相手が「じゃあ、x=1 は？」と聞いてくる。
5. A は「あ、1 も 0 にしよう」とまた後戻りして変更する。
- ポイント： 相手が「有限の情報しか持っていない（連続的な反応）」場合、A は相手が「すでに答えたことのある x」を聞いてくる瞬間を狙って、「あ、その答えは 0 だったよ！」と勝つことができます。

🤔 驚きの結末：

嘘（★）には、A が勝つ戦略がある。
しかし、**「嘘の否定（本当のこと）」**を主張するプレイヤー B も、A に対して勝つ戦略を持っている。
結果：A と B が戦うと、永遠に終わらない無限の議論（無限ループ）が生まれる。

🚨 重要な教訓：
「相手が連続的に反応する（有限の情報しか持たない）」という条件だけでは、「何が真実で、何が嘘か」を区別できないことがわかりました。
嘘であっても、相手の反応次第で「勝てるゲーム」になってしまうのです。これは、従来の「計算可能性」や「連続性」だけでは、論理の真偽を完全に説明できないことを示しています。

🌟 まとめ：この論文が伝えたいこと

無限の議論の正体：
議論が永遠に続く場合、それは「誰のせいか」を特定できる（第 1 の洞察）。これは、無限のループを数学的に整理する新しい視点を与えます。
嘘の勝利と限界：
「嘘」であっても、相手の反応が「連続的（有限の情報）」であれば、嘘つきが勝つゲームを作れてしまう（第 2 の洞察）。
これは、「計算の強さ（リソース）」に差がある場合、強い側は弱い側に「嘘」を信じ込ませる可能性があるという哲学的な示唆を含んでいます。

🎓 ステファノ・ベラルディへのオマージュ
著者のティエリー・クコントは、ベラルディ氏との 30 年前の議論を振り返り、これらの「直感的だが深遠な洞察」が、現代の計算機科学や論理学においていまだに重要な意味を持っていることを伝えています。

要するに、「論理のゲーム」において、後戻り（バックトラック）というルールが、真実と嘘の境界をどう揺さぶるのかを、ベラルディのアイデアを通じて再発見した論文なのです。

論文「Two Remarks about Game Semantics of Classical Logic」の技術的サマリー

著者: Thierry Coquand
対象: ステファノ・ベラルディ（Stefano Berardi）への献呈論文
概要: この論文は、古典論理のゲーム意味論に関するステファノ・ベラルディの未発表の 2 つの重要な洞察（所見）を報告・解説するものである。具体的には、無限相互作用シーケンスへの「視点（view）」概念の自然な拡張と、実在性意味論（realizability semantics）における「連続性」に基づく正当化の限界を示す反例について論じている。

1. 問題設定と背景

古典論理の計算的意味論として、ゲーム意味論（Game Semantics）が提案されている。特に、ベラルディとコカンによる先行研究 [2] では、古典論理の証明を「完全情報ゲーム」として解釈し、証明の「カット除去（cut-elimination）」プロセスを、プレイヤー間の相互作用（議論）としてモデル化している。

プレイヤー: 存在量化者（ $\exists$ loise）と全称量化者（ $\forall$ belard）。
特徴: $\exists$ loise は、環境（ $\forall$ belard）からの応答に基づいて、自分の選択を後戻り（backtrack）できる。この後戻り能力が、古典論理の排中律や二重否定除去などの非構成的原理に対応する。
既存の成果: 有限な相互作用シーケンスにおける終止性（カット除去の終了）は、幾何学的な相互作用解析によって示されている。

しかし、無限の相互作用や、関数型を含むより複雑な論理体系（HA $^\omega$ に可算選択公理などを加えた系）において、ゲーム意味論がどのように振る舞うか、また「実在性（realizability）」の条件として何が適切かが完全には解明されていない。ベラルディの 2 つの所見は、これらの境界領域における重要な洞察を提供する。

2. 方法論

論文は、以下の 2 つの主要な所見を、ゲーム意味論の枠組み（特に相互作用シーケンスと視点の概念）を用いて分析・定式化している。

相互作用シーケンスの超有限拡張:
- 有限な相互作用シーケンスの定義を、無限（ $\omega$ ）および超有限（transfinite）な段階に拡張する。
- 「視点（view）」の概念を無限の議論まで適用し、無限の議論がどちらのプレイヤーの責任であるかを特定する数学的構造を構築する。
連続性に基づく戦略の分析:
- 関数型を含む論理式（可算選択公理など）における $\exists$ loise の戦略を分析する。
- 「連続性（continuity）」の仮定（ $\forall$ belard が関数の有限部分情報しか使わない）の下で、 $\exists$ loise が勝利する戦略が存在するかどうかを検討する。
- 偽の論理式であっても、連続な相手に対しては $\exists$ loise が勝利する戦略が存在しうるという反例を構成する。

3. 主要な貢献と結果

所見 1: 無限相互作用シーケンスへの視点の自然な拡張

従来のゲーム意味論では、相互作用シーケンスは有限長であったが、ベラルディはこれを無限の議論に拡張するアイデアを示した。

定理 1（古典論理）: 無限の相互作用シーケンス $V, \phi$ $V, ϕ$ において、一意な数列 $n_k < n_{k+1}$ $n_{k} < n_{k + 1}$ が存在し、 $n_k + 1 = \phi(n_{k+1})$ $n_{k} + 1 = ϕ (n_{k + 1})$ かつ $S(n_k)$ $S (n_{k})$ が $[0, \omega[$ $[0, ω [$ の分割をなす。
- ここで $S(k)$ はセグメント（区間）を表す。
意味: この一意性は、無限の議論が続く場合、その責任をどちらのプレイヤーが負うかを明確に特定できることを示している。
- 無限の議論がある場合、その「視点（view）」は $V(\omega) = \{n_k\}$ として定義され、 $\exists$ loise と $\forall$ belard のどちらかが無限に後戻りを繰り返しているか、あるいは議論が特定のプレイヤーの視点で固定されているかを判定できる。
- これにより、相互作用シーケンスを $\omega$ を超えて（超有限に）拡張することが可能となり、無限の議論の構造を厳密に記述できる。

所見 2: 連続性に基づく正当化の限界と偽の論理式

ベラルディのもう一つの重要な洞察は、「連続な相手に対する勝利戦略」だけでは、実在性意味論（realizability semantics）を特徴づけるには不十分であるという点である。

背景: 先行研究 [2] や Hida [7] では、 $\forall$ belard が「連続的」（関数の有限部分のみを参照する）に振る舞う限り、 $\exists$ loise が勝利する戦略が存在すれば、その論理式は実在可能（realizable）であるとみなされていた（例：可算選択公理）。
反例の構成:
- 論理式 $(*)$ $(*)$ : $\bigvee_f \bigwedge_x \bigvee_y (f(x) = 0 \land f(y) \neq 0)$ $⋁_{f} ⋀_{x} ⋁_{y} (f (x) = 0 \land f (y) \neq = 0)$
  - この式は明らかに偽である（すべての $x$ に対して $f(x)=0$ かつある $y$ で $f(y) \neq 0$ となる関数 $f$ は存在しない）。
- しかし、 $\exists$ $\exists$ loise は以下の戦略で、任意の連続な $\forall$ belard に対して勝利することができる。
  1. 初期関数 $f_0 = \lambda n. 1$ を選ぶ。
  2. $\forall$ belard が $x_0$ を選ぶと、 $\exists$ loise は $f_1$ を $f_0$ を修正し $f_1(0)=0$ となるように更新して後戻りする。
  3. $\forall$ belard が $x_1$ を選ぶと、もし $x_1 < 1$ なら勝利。そうでなければ $f_2$ を更新し、 $f_2(1)=0$ として後戻りする。
  4. このプロセスを続け、 $\forall$ belard が連続的であれば、必ずある時点で $x_n < n$ となるため、 $\exists$ loise は $y=n$ を選んで勝利する。
対立戦略:
- 一方、この論理式の否定に対する戦略 $B_1$ も存在する。
- $A_1$ （上記の戦略）と $B_1$ が対戦すると、無限の議論（無限の後戻り）が発生し、カット除去が終了しない。
結論:
- 偽の論理式であっても、 $\exists$ loise が「連続な相手」に対して勝利する戦略を持つ場合がある。
- したがって、「連続性に基づく議論」だけでは、古典論理の実在性意味論を完全に特徴づけることはできない。計算リソースの非対称性（一方が他方を欺くことができる）が、誤った命題の「勝利」を生み出す可能性がある。

4. 意義と結論

この論文は、ステファノ・ベラルディの洞察を通じて、古典論理のゲーム意味論における以下の点を明確にしている。

無限議論の定式化: 無限の相互作用を「視点」の概念を用いて厳密に扱えることを示し、カット除去の終止性に関する分析を超有限な領域へ拡張する道を開いた。
実在性意味論の限界: 「連続性」は実在性を保証する十分条件ではないことを示した。特に、関数型を含む論理系において、偽の命題であっても特定の計算リソース制約（連続性）の下では「勝てる」戦略が存在しうる。これは、ソロビエフ（Soloviev）のアーベルマン関数に関する例とも哲学的に共通しており、プレイヤー間の非対称性が論理的真理の認識に与える影響を浮き彫りにしている。

これらの結果は、古典論理の計算的内容（computational content）をより深く理解し、修正実在性（modified realizability）やゲーム意味論の理論的基盤を強化する上で重要な貢献である。