エーレンフォイヒト対フレッセ戦

モデル理論という数学分野において、エーレンフォイヒト・フレッセゲーム（往復ゲームとも呼ばれる）は、2つの構造 が基本的に等価であるかどうかを判定するためのゲーム意味論に基づく手法である。エーレンフォイヒト・フレッセゲームの主な応用は、一階述語論理における特定の性質の表現不可能性を証明することである。実際、エーレンフォイヒト・フレッセゲームは、一階述語論理における表現不可能性結果を証明するための完全な方法論を提供する。この役割において、これらのゲームは有限モデル理論とそのコンピュータ科学における応用（特にコンピュータ支援検証とデータベース理論）において特に重要である。なぜなら、エーレンフォイヒト・フレッセゲームは、有限モデルの文脈で有効なモデル理論の数少ない手法の1つだからである。コンパクト性定理など、表現不可能性結果を証明するために広く用いられている他の手法は、有限モデルでは機能しない。

エーレンフォイヒト・フレッセのようなゲームは、不動点論理^{[ 1 ]}や有限変数論理のペブルゲーム^{[ 2 ]}など、他の論理に対しても定義できます。拡張は、単項二階論理における定義可能性を特徴付けるのに十分強力です。^{[ 3 ]}様相論理の類似のゲームは双模倣ゲームです。

このゲームの基本となる考え方は、2つの構造と2人のプレイヤー（スポイラーとデュプリケーター）が存在するというものです。デュプリケーターは、2つの構造が本質的に同等であること（同じ一階述語論理を満たすこと）を示したいのに対し、スポイラーは、2つの構造が異なることを示したいのです。ゲームはラウンド制で行われます。1ラウンドは次のように進行します。スポイラーは一方の構造から任意の要素を選択し、デュプリケーターはもう一方の構造から要素を選択します。簡単に言うと、デュプリケーターのタスクは、スポイラーが選択した要素と「類似」する要素を常に選択することであり、スポイラーのタスクは、もう一方の構造に「類似」する要素が存在しない要素を選択することです。2つの異なる構造から最終的に選択された部分構造の間に同型性が存在する場合、デュプリケーターの勝ちとなります。そうでない場合は、スポイラーの勝ちとなります。

ゲームは決められたステップ数で終了します${\displaystyle \gamma }$（これは序数です。通常は有限の数または${\displaystyle \omega }$)

2つの構造が与えられていると仮定します${\displaystyle {\mathfrak {A}}}$ そして${\displaystyle {\mathfrak {B}}}$それぞれ関数記号がなく、同じ関係記号のセットを持ち、固定された自然数nを持つ。こうして、エーレンフォイヒト・フレッセゲームを定義できる。${\displaystyle G_{n}({\mathfrak {A}},{\mathfrak {B}})}$これは、スポイラーとデュプリケーターという2人のプレイヤー間で行われるゲームで、以下のようにプレイされます。

1. 最初のプレイヤーであるスポイラーは、メンバーのいずれかを選択します。${\displaystyle a_{1}}$の${\displaystyle {\mathfrak {A}}}$またはメンバー${\displaystyle b_{1}}$の${\displaystyle {\mathfrak {B}}}$。
2. スポイラーがメンバーを選んだ場合${\displaystyle {\mathfrak {A}}}$デュプリケーターがメンバーを選択します${\displaystyle b_{1}}$の${\displaystyle {\mathfrak {B}}}$それ以外の場合は、Duplicatorがメンバーを選択します。${\displaystyle a_{1}}$の${\displaystyle {\mathfrak {A}}}$。
3. ネタバレはメンバーのいずれかを選ぶ${\displaystyle a_{2}}$の${\displaystyle {\mathfrak {A}}}$またはメンバー${\displaystyle b_{2}}$の${\displaystyle {\mathfrak {B}}}$。
4. 複製装置が要素を選択する${\displaystyle a_{2}}$または${\displaystyle b_{2}}$スポイラーが選ばなかったモデルにおいて。
5. スポイラーとデュプリケーターは引き続きメンバーを選びます${\displaystyle {\mathfrak {A}}}$そして${\displaystyle {\mathfrak {B}}}$のために${\displaystyle n-2}$さらに手順があります。
6. ゲームの終了時に、私たちは明確な要素を選択しました${\displaystyle a_{1},\dots ,a_{n}}$の${\displaystyle {\mathfrak {A}}}$そして${\displaystyle b_{1},\dots ,b_{n}}$の${\displaystyle {\mathfrak {B}}}$したがって、この集合には2つの構造が存在する。${\displaystyle \{1,\dots ,n\}}$、1つは${\displaystyle {\mathfrak {A}}}$地図送信を介して${\displaystyle i}$に${\displaystyle a_{i}}$、そして他のものは ${\displaystyle {\mathfrak {B}}}$地図送信を介して${\displaystyle i}$に${\displaystyle b_{i}}$これらの構造が同じであれば複製者が勝ち、そうでなければスポイラーが勝ちます。

各nに対して、関係を定義する${\displaystyle {\mathfrak {A}}\ {\overset {n}{\sim }}\ {\mathfrak {B}}}$デュプリケーターがn手ゲームに勝利した場合${\displaystyle G_{n}({\mathfrak {A}},{\mathfrak {B}})}$これらはすべて、与えられた関係記号を持つ構造のクラス上の同値関係です。これらの関係の共通部分もまた同値関係です。${\displaystyle {\mathfrak {A}}\sim {\mathfrak {B}}}$。

Duplicator がすべての有限nに対してこのゲームに勝つ場合、つまり、${\displaystyle {\mathfrak {A}}\sim {\mathfrak {B}}}$、 それから${\displaystyle {\mathfrak {A}}}$そして${\displaystyle {\mathfrak {B}}}$これらは基本的に同等である。考慮される関係記号の集合が有限である場合、その逆もまた真である。

不動産${\displaystyle Q}$が真実である${\displaystyle {\mathfrak {A}}}$しかし、${\displaystyle {\mathfrak {B}}}$、 しかし${\displaystyle {\mathfrak {A}}}$そして${\displaystyle {\mathfrak {B}}}$Duplicator の勝利戦略を提供することで同等であることが示されれば、これは次のことを示している。${\displaystyle Q}$与えられた関係記号を持つ構造の一次論理では表現できない。

エーレンフォイヒト-フレッセゲームで基本等価性を検証するために用いられる往復法は、ローランド・フレッセが論文で提示したもので、[ 4 ] ^{[ 5 ]アンジェイ・エーレン}フォイヒト がゲームとして定式化した。^{[ 6 ]}スポイラーとデュプリケーターという名前はジョエル・スペンサーによるものである。^{[ 7 ]}その他一般的な名前としてはエロイーズ[sic]とアベラール（しばしば、${\displaystyle \exists }$そして${\displaystyle \forall }$）エロイーズとアベラールにちなんで、ウィルフリッド・ホッジスが著書『モデル理論』^{[ 8 ]}で導入した命名法、あるいはイブとアダムにちなんで。

ポワザのモデル理論のテキスト^{[ 9 ]}の第1章にはエーレンフォイヒト・フレッセゲームの入門が含まれており、ローゼンシュタインの線形順序に関する本の第6章、第7章、第13章にも同様に紹介されている^{[ 10 ]}。 エーレンフォイヒト・フレッセゲームの簡単な例は、イヴァルス・ピーターソンのMathTrekコラムの1つで紹介されている^{[ 11 ] 。}

フォキオン・コライティスのスライド^{[ 12 ]}とニール・イマーマンの著書の章^{[ 13 ]}では、エーレンフォイヒト・フレッセゲームについて、コンピュータサイエンスにおける応用、表現不可能性の証明方法、およびこの方法を用いたいくつかの単純な表現不可能性の証明について論じている。

エーレンフォイヒト＝フレッセゲームは、モデルロイドに対する微分演算の基礎となる。モデルロイドは特定の同値関係であり、微分は標準的なモデル理論の一般化を提供する。

• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel ; Vardi, Moshe Y .; Venema, Yde; Weinstein, Scott (2007).有限モデル理論とその応用. 理論計算機科学テキストシリーズ. EATCSシリーズ. ベルリン: Springer-Verlag . ISBN 978-3-540-00428-8. Zbl 1133.03001 . 

• コーネル大学数学科のMATH EXPLORERS' CLUBにおける、エーレンフォイヒト＝フレッセゲームに関する6回の講義。
• モデルロイドI、ミロスラフ・ベンダ、アメリカ数学会紀要、第 250 巻 (1979 年 6 月)、 47 ～ 90 ページ (44 ページ)