A New Ehrenfeucht-Fraïssé Game for Dependence Logic

技術要約：依存論理のための新しいエレンフェシュト・フライス・ゲーム

問題提起
依存論理（$D$）は、$\vec{x}$ の値によって $y$ の値が機能的に決定されることを主張する依存アトム $=(\vec{x}, y)$ を追加することで、一階述語論理を拡張したものである。$D$ の意味論は通常、単一の割り当てではなく、割り当ての集合（チーム）上で公式を評価するチーム意味論を通じて定義される。したがって、[15] における依存論理のためのエレンフェシュト・フライス（EF）ゲームの試みは、プレイヤーがチーム全体や割り当ての集合を選択するという「二階」的な動きに依存していた。著者らは、チームは膨大になり得るため、これらの動きは計算量および概念の両面で複雑であると主張している。本論文は、依存論理の表現力を維持しつつ、古典的な一階述語論理の EF ゲームと同様に、動きが単一の要素で構成される、依存論理のための「一階的」な EF ゲームを定義することを目的としている。

手法
著者らは、2 つの構造 $A$ と $B$ の間でプレイされる新しいゲーム $EF^{dep}_n(A, B)$ を導入する。その手法は、主に以下の 3 つの構成要素からなる。

1. ゲームのメカニクス:
   ゲームは $n$ ラウンド進行する。各ラウンド $k$ において、プレイヤー I（スプイラー）は $A$ または $B$ から要素 $x_k$ を選択する。極めて重要な点は、プレイヤー I が「依存コミットメント」の集合 $W_k \subseteq \mathcal{P}(n)$ および原子公式の集合 $U^+_k, U^-_k$ も宣言しなければならないことである。

• もしインデックスの集合 $\{i_0, \dots, i_{k-1}\} \in W_k$ である場合、プレイヤー I は、現在の動き $x_k$ が、同一モデル内の以前の動きのみによって決定される（すなわち、$x_k \in A$ であれば $\{x_{i_0}, \dots, x_{i_{k-1}}\}$ に、$x_k \in B$ であれば対応する要素にのみ依存する）と宣言する。
• プレイヤー II（デュプリケーター）は、反対側の構造から要素 $y_k$ を応答として選択する。
• 単一のプレイにおけるプレイヤー II の勝利条件は、これらのコミットメントに基づいたものではない。むしろ、コミットメントは複数のプレイを同時に考慮する際にのみ評価される。

2. 一様勝利戦略:
   核心となる革新は、プレイヤー II の**一様勝利戦略（uniform winning strategy）**の定義である。戦略が一様で勝利的であるとは、プレイヤー I が一貫してプレイする場合（すなわち、複数のプレイにおいて同じコミットメントを行い、同じ原子公式を満たす場合）、プレイヤー II の応答が宣言された依存関係を尊重する場合を指す。具体的には、もし 2 つの異なるプレイにおいて、プレイヤー I の動きが $W_k$ で宣言されたインデックス上で同一であれば、プレイヤー II の応答もまた同一でなければならない。このメカニズムにより、チーム全体を選択することなく、依存アトムの機能的な性質を捉えることが可能となる。

3. 補助ゲームと等価性:
   特徴付けの結果を証明するために、著者らはインデックス付きチームに基づく補助ゲーム $EFD_n((A, X), (B, Y))$ を導入する。このゲームは [15] のゲームの修正版であるが、補完関数（チームがどのように拡張されるかを定義するもの）をチームそのものではなく、動きとして使用する。著者らは、これら 2 つのゲームの間に架け橋を築く：

• プレイヤー II が補助ゲーム $EFD_n$ において勝利戦略を持つならば、新しいゲーム $EF^{dep}_n$ において一様勝利戦略を持つことを示す。
• プレイヤー II が $EF^{dep}_n(A, B)$ において一様勝利戦略を持つことの存在は、量子ランク $\le n$ のすべての依存論理の文について、$A$ から $B$ への真理の保存と同値であることを証明する。

主な貢献と結果

• $EF^{dep}_n(A, B)$ の定義: 本論文は、チームではなく単一の要素を動きとする新しい EF ゲームを定義する。これにより、従来の定式化に見られた「二階」的な動きの複雑さが解消される。
• 一様性条件: 「一様勝利戦略」の概念を導入し、プレイヤー II の応答が、プレイヤー I によって宣言された機能的依存関係を遵守することを強制する。
• 特徴付け定理: 主要な結果（定理 6.1）は、任意の 2 つの構造 $A$ と $B$ について、プレイヤー II がすべての $n$ に対して $EF^{dep}_n(A, B)$ において一様勝利戦略を持つことは、$A \equiv_D B$（$A$ と $B$ が依存論理において初等的に等価であること）と同値であることを確立する。
• 一階的動きへの還元: 著者らは、依存論理の意味論が「二階」的な性質を持っているにもかかわらず、戦略が一様性条件を満たす限り、ゲームは一階的な動きでプレイできることを示している。

意義と主張
本論文は、一階述語論理における古典的な結果を模倣した、依存論理における初等的な等価性の「一階的」な特徴付けを提供すると主張している。その意義は、ゲームプレイ中に巨大なチームを操作することを避けることで、依存論理のゲーム理論的な分析を簡略化した点にある。

著者らは、結果の範囲について控えめな姿勢をとっている。彼らは以下の点に留意している：

• 主要な結果の証明は、依存論理の特定の標準形（定理 2.5）に依存しており、これはゲームの長さと任意の公式の量子ランクを直接結びつけることを困難にするため、やや不十分であると認めている。
• 結果は、依存論理の下方閉鎖性（downward closedness）（事実 2.3）に強く依存している。したがって、著者らは、これらの結果を包含論理や独立論理のような、この性質を持たない他のチーム論理に直ちに適用することはできないと述べている。
• 今後の課題として、包含論理や独立論理のために同様のゲームを構築できるかどうかの探求、および標準形に頼ることなくゲームの長さを量子ランクにより密接に結びつける方法の調査が示唆されている。

本論文は、新しい応用や実験的な提案を行うものではなく、ゲーム意味論を通じた依存論理の理論的な特徴付けに厳密に焦点を当てている。