Ehrenfeucht–Fraïsséゲーム

同義語：Ehrenfeucht-FraïsséゲームEFゲームEhrenfeucht–Fraïssé gameEhrenfeucht game

概要

前提知識: 一階述語論理, 構造(モデル), 初等同値

2 つの構造が同じ文を満たすか（初等同値か）を確かめるには、本来は無限にある文を 1 つずつ調べなければならない。Ehrenfeucht–Fraïssé ゲーム（EF ゲーム）は、この問いを 2 人のプレイヤーの有限回のゲームに置き換える。妨害者（Spoiler）は 2 つの構造の違いを暴こうとして一方の構造から元を選び、模倣者（Duplicator）はもう一方の構造から対応する元を選んで違いを隠す。$n$ 回のやりとりの最後まで、選ばれた元どうしの対応が等号と関係記号を保っていれば模倣者の勝ちである。この記事では、模倣者が $n$ 回のゲームで必ず勝てることと、量化記号の入れ子が $n$ 以下の文をすべて同じように満たすことが同値であるという Ehrenfeucht–Fraïssé の定理 を証明する。応用として、要素が $2^k-1$ 個以上の有限な線形順序は量化記号の入れ子が $k$ 以下の文で区別できないことを示し、「要素の個数が偶数である」ことが順序の言語の一階の文で書けないことを導く。

定義

以下、言語 $L$ は 有限個の関係記号だけからなる（定数記号・関数記号をもたない）とする。構造は空でない台集合をもち、構造 $\mathcal M$ の台集合を $M$ と書く。構造・割り当て・充足関係 $\mathcal M\models\varphi[s]$ は一階述語論理の記事の定義「構造」「充足関係」の意味で用いる。変数を $v_1,v_2,\dots$ と並べておく。$\bar a=(a_1,\dots,a_k)\in M^k$ と相異なる変数 $u_1,\dots,u_k$ について、自由変数が $u_1,\dots,u_k$ の中にある論理式 $\varphi$ に対し、$s(u_i)=a_i$ となる割り当て $s$ で $\mathcal M\models\varphi[s]$ が成り立つことを $\mathcal M\models\varphi[\bar a/\bar u]$ と書く（$s$ の選び方によらないことは同記事の補題「一致補題」）。$\bar u=(v_1,\dots,v_k)$ のときは単に $\mathcal M\models\varphi[\bar a]$ と書く。

量化子階数と n-同値

論理式 $\varphi$ の 量化子階数（quantifier rank）$\operatorname{qr}(\varphi)$ を、次の再帰で定める。原子論理式では $0$、$\operatorname{qr}(\lnot\psi)=\operatorname{qr}(\psi)$、$\operatorname{qr}(\psi\ast\chi)=\max\{\operatorname{qr}(\psi),\operatorname{qr}(\chi)\}$（$\ast$ は $\land,\lor,\to$）、$\operatorname{qr}(\forall x\,\psi)=\operatorname{qr}(\exists x\,\psi)=\operatorname{qr}(\psi)+1$。
$L$ 構造 $\mathcal M,\mathcal N$ と $\bar a\in M^k$、$\bar b\in N^k$ について、自由変数が $v_1,\dots,v_k$ の中にあり量化子階数が $n$ 以下のすべての論理式 $\varphi$ で
$$ \mathcal M\models\varphi[\bar a]\iff\mathcal N\models\varphi[\bar b] $$
が成り立つことを $(\mathcal M,\bar a)\equiv_n(\mathcal N,\bar b)$ と書く。$k=0$ の場合、すなわち量化子階数 $n$ 以下の文をすべて同じように満たすことを $\mathcal M\equiv_n\mathcal N$ と書き、$\mathcal M$ と $\mathcal N$ は $n$-同値 であるという。

量化子階数は量化記号の入れ子の深さである。たとえば $\exists x\,\exists y\,(\lnot x=y)$ は $2$、$\exists x\,P(x)\land\exists y\,Q(y)$ は $1$ である。すべての $n$ で $\mathcal M\equiv_n\mathcal N$ であることは、どの文も有限の量化子階数をもつので、$\mathcal M$ と $\mathcal N$ が初等同値であること（$\mathcal M\equiv\mathcal N$）と同じである。

部分同型

$\bar a\in M^k$、$\bar b\in N^k$ とする。$L$ のすべての $r$ 項関係記号 $R$ と添字 $1\le i_1,\dots,i_r\le k$、$1\le i,j\le k$ について
$$ (a_{i_1},\dots,a_{i_r})\in R^{\mathcal M}\iff(b_{i_1},\dots,b_{i_r})\in R^{\mathcal N},\qquad a_i=a_j\iff b_i=b_j $$
が成り立つとき、対応 $a_i\mapsto b_i$ は 部分同型（partial isomorphism）であるという。

2 つ目の条件により、対応 $a_i\mapsto b_i$ は矛盾なく定まる単射である。言い換えると、$\bar a$ と $\bar b$ は、変数が $v_1,\dots,v_k$ の中にある原子論理式をすべて同じように満たす。

Ehrenfeucht–Fraïsséゲーム

$\mathcal M,\mathcal N$ を $L$ 構造、$\bar a\in M^k$、$\bar b\in N^k$、$n\ge0$ とする。局面 $(\bar a,\bar b)$ から始まる $n$ 手の Ehrenfeucht–Fraïssé ゲーム $G_n(\mathcal M,\bar a;\mathcal N,\bar b)$ は、妨害者と模倣者の 2 人が次のように行うゲームである。各手番 $t=1,\dots,n$ で、

妨害者が $\mathcal M,\mathcal N$ の一方を選び、その台集合から元を 1 つ選ぶ（前に選ばれた元を選んでもよい）。
模倣者が他方の台集合から元を 1 つ選ぶ。
第 $t$ 手で $M$ から選ばれた元を $a_{k+t}$、$N$ から選ばれた元を $b_{k+t}$ とする。$n$ 手の後、対応 $a_i\mapsto b_i$（$1\le i\le k+n$）が部分同型ならば模倣者の勝ち、そうでなければ妨害者の勝ちとする。
妨害者がどう選んでも模倣者が勝てる選び方（必勝戦略）を模倣者がもつとき、$\bar a\sim_n\bar b$ と書く。$k=0$ のときは $\mathcal M\sim_n\mathcal N$ と書き、これを $G_n(\mathcal M,\mathcal N)$ で模倣者が勝つという。

$\bar a\sim_0\bar b$ は、$a_i\mapsto b_i$ が部分同型であることにほかならない。$k=0$ では空の対応は部分同型なので、いつでも $\mathcal M\sim_0\mathcal N$ である。

直感

妨害者の 1 手は、量化記号 1 つに対応する。$\mathcal N$ にはないが $\mathcal M$ にはある性質「$\exists x\,\psi(x)$」があれば、妨害者は $\mathcal M$ から $\psi$ の証拠を選び、模倣者は $\mathcal N$ でそれに見合う元を見つけられない。$\exists x\,\exists y\,\psi(x,y)$ のように量化記号が 2 重なら、妨害者は 2 手かけて証拠を順に選ぶ。こうして、量化子階数 $n$ の文で 2 つの構造を区別できることと、妨害者が $n$ 手で勝てることが対応する。模倣者の側から見ると、必勝戦略は「$n$ 手先まで違いを見せない対応のつけ方」であり、これは無限にある文を調べる代わりに、有限の対象についての組合せ的な議論で $n$-同値を示す手段になる。

例

元を数える 2 手

1 項関係記号 $P$ だけの言語で、$M=\{a_1,a_2,a_3\}$、$P^{\mathcal M}=\{a_1\}$ とし、$N=\{b_1,b_2,b_3\}$、$P^{\mathcal N}=\{b_1,b_2\}$ とする。
$G_1(\mathcal M,\mathcal N)$ では模倣者が勝つ。妨害者が $P$ を満たす元を選べば、模倣者は他方から $P$ を満たす元を選び、満たさない元を選べば、他方から満たさない元を選べばよい。どちらの構造にも両方の種類の元があるので、いつでも応じられる。
$G_2(\mathcal M,\mathcal N)$ では妨害者が勝つ。妨害者は第 1 手で $b_1$、第 2 手で $b_2$ を選ぶ（どちらも $N$ から）。模倣者の応答はどちらも $P$ を満たさなければならないので、$M$ では 2 回とも $a_1$ になる。すると $b_1\ne b_2$ なのに $a_1=a_1$ となって、対応は部分同型でない。この違いは量化子階数 $2$ の文 $\exists x\,\exists y\,(\lnot x=y\land P(x)\land P(y))$ が $\mathcal N$ で真、$\mathcal M$ で偽であることに対応する。

稠密な線形順序

順序の言語 $\{<\}$ で、$\mathcal M,\mathcal N$ を端点のない稠密な線形順序とする。$\bar a\in M^k$、$\bar b\in N^k$ が部分同型（$a_i< a_j\iff b_i< b_j$、$a_i=a_j\iff b_i=b_j$）ならば、すべての $n$ で $\bar a\sim_n\bar b$ である。妨害者が $M$ から $a$ を選んだとき、$a$ と各 $a_i$ の大小の位置関係は「どの $a_i$ より小さい」「どの $a_i$ より大きい」「ある $a_i$ に等しい」「隣り合う 2 つの $a_i< a_j$ の間」のどれかであり、$N$ に端点がなく稠密であることから、$b_i$ たちに対して同じ位置にある $b$ を選べる。選んだ後の対応はまた部分同型なので、模倣者は毎手この選び方を続ければ勝つ（この拡張の一歩はカテゴリー性の記事の定理「Cantor の定理」の証明で使われるものと同じである）。特に $(\mathbb Q,<)\sim_n(\mathbb R,<)$ がすべての $n$ で成り立ち、後の cor-efg-elementary により $(\mathbb Q,<)$ と $(\mathbb R,<)$ は初等同値である。2 つは濃度が違うので同型ではない。

性質

1 手ずつの特徴づけ

往復条件による特徴づけ

$n\ge1$、$\bar a\in M^k$、$\bar b\in N^k$ とする。$\bar a\sim_n\bar b$ であるための必要十分条件は、次の 2 つがともに成り立つことである。

（行き）任意の $a\in M$ に対し、ある $b\in N$ があって $(\bar a,a)\sim_{n-1}(\bar b,b)$。
（帰り）任意の $b\in N$ に対し、ある $a\in M$ があって $(\bar a,a)\sim_{n-1}(\bar b,b)$。

第 1 手で場合を分ける

必要性：局面 $(\bar a,\bar b)$ からの $n$ 手のゲームでの模倣者の必勝戦略を 1 つ固定する。妨害者が第 1 手で $a\in M$ を選んだときのこの戦略の応答を $b$ とする。残りの $n-1$ 手は、局面 $((\bar a,a),(\bar b,b))$ から始まる $n-1$ 手のゲームそのものであり、固定した戦略の続きに従えば模倣者は勝つ。よって $(\bar a,a)\sim_{n-1}(\bar b,b)$ で、（行き）が成り立つ。妨害者が第 1 手で $N$ から選ぶ場合を考えれば（帰り）が成り立つ。
十分性：（行き）（帰り）を仮定する。模倣者は第 1 手で、妨害者が $a\in M$ を選べば（行き）の $b$ で、$b\in N$ を選べば（帰り）の $a$ で応じる。どちらの場合も、局面 $((\bar a,a),(\bar b,b))$ からの $n-1$ 手のゲームに模倣者の必勝戦略があるので、以後はそれに従う。こうして作った選び方は、妨害者のどの手にも応じて最後に部分同型を残すので、必勝戦略である。$\square$

この補題により、$\sim_n$ はゲームを持ち出さずに $n$ についての再帰で定められる。$\sim_0$ は部分同型であることで、$\sim_n$ は「行きと帰りで $\sim_{n-1}$ に延ばせる」ことである。OLT26 §25.6 は、この再帰の形（Definition 25.21 の関係 $I_n$）で議論している。

ゲームの勝ちは同じ文を満たすことを導く

模倣者の勝ちから n-同値へ

$L$ を関係記号だけからなる言語（有限でなくてよい）とする。$\bar a\in M^k$、$\bar b\in N^k$ が $\bar a\sim_n\bar b$ を満たせば、相異なる変数 $u_1,\dots,u_k$ と、自由変数が $u_1,\dots,u_k$ の中にあり量化子階数が $n$ 以下の任意の論理式 $\varphi$ について
$$ \mathcal M\models\varphi[\bar a/\bar u]\iff\mathcal N\models\varphi[\bar b/\bar u] $$
が成り立つ。特に $\bar a\sim_n\bar b$ ならば $(\mathcal M,\bar a)\equiv_n(\mathcal N,\bar b)$ である。

n と論理式についての二重の帰納法

要点：量化子階数 $n$ についての帰納法の中で、論理式の組み立てについての帰納法を行う。原子論理式は部分同型の定義そのもので、$\exists$ の場合は（行き）（帰り）で証拠の元を相手の構造へ移し、$n-1$ の場合に帰着する。

詳しい証明を開く

$n$ についての帰納法で、すべての $k$、$\bar a,\bar b$、$\bar u$ について示す。$n$ を固定し、$n$ 未満では主張が成り立つとして、量化子階数 $n$ 以下の論理式 $\varphi$ の組み立てについての帰納法を行う。

原子論理式：言語は関係記号だけなので、$\varphi$ は $R(u_{i_1},\dots,u_{i_r})$ か $u_i=u_j$ の形である。$\mathcal M\models R(u_{i_1},\dots,u_{i_r})[\bar a/\bar u]$ は $(a_{i_1},\dots,a_{i_r})\in R^{\mathcal M}$ のことなので、$\bar a\sim_n\bar b$ から $\bar a\sim_0\bar b$（模倣者の必勝戦略は、最初の局面で部分同型であることを含む。そうでなければ、最後の対応も部分同型でない）を使えば、def-efg-partial-iso から両辺が一致する。等号も同様である。

$\lnot\psi$、$\psi\ast\chi$：$\psi,\chi$ の自由変数は $\varphi$ の自由変数に含まれ、量化子階数は $n$ 以下なので、帰納法の仮定と充足関係の定義から従う。

$\varphi=\exists y\,\psi$：このとき $n\ge1$、$\operatorname{qr}(\psi)\le n-1$ である。$\psi$ に現れず $u_1,\dots,u_k$ のどれとも異なる変数 $z$ をとると、一階述語論理の記事の系「束縛変数の付け替え」により $\exists y\,\psi$ は $\exists z\,\psi'$（$\psi':=\psi[z/y]$）と論理的に同値である。$\psi'$ の自由変数は $u_1,\dots,u_k,z$ の中にあり、変数を変数に替えても量化記号は変わらないので $\operatorname{qr}(\psi')\le n-1$ である。$\mathcal M\models\exists z\,\psi'[\bar a/\bar u]$ とすると、ある $a\in M$ で $\mathcal M\models\psi'[(\bar a,a)/(\bar u,z)]$ である。lem-efg-back-and-forth の（行き）により $(\bar a,a)\sim_{n-1}(\bar b,b)$ となる $b\in N$ があり、$n-1$ についての帰納法の仮定（変数の列 $(\bar u,z)$ に適用）により $\mathcal N\models\psi'[(\bar b,b)/(\bar u,z)]$、よって $\mathcal N\models\exists z\,\psi'[\bar b/\bar u]$ である。逆向きは（帰り）を使って同様に示せる。

$\varphi=\forall y\,\psi$：$\forall y\,\psi$ は $\lnot\exists y\,\lnot\psi$ と論理的に同値で、量化子階数も等しいので、前の場合に帰着する。$\square$

この向きには言語が有限であることを使わない。逆向きには使う。

Hintikka 論理式と主定理

逆向きの証明では、局面 $(\bar a)$ が満たす量化子階数 $n$ 以下の性質をすべてまとめた 1 つの論理式を作る。$k\ge1$ のとき、変数が $v_1,\dots,v_k$ の中にある原子論理式 $R(v_{i_1},\dots,v_{i_r})$、$v_i=v_j$ の全体を $\mathrm{At}_k$ とする。$L$ が有限なので $\mathrm{At}_k$ は有限集合であり、$v_1=v_1$ を含むので空でない。その元を 1 列に並べておく。

Hintikka 論理式

$n,k\ge0$、$n+k\ge1$ について、論理式の集合 $H_{n,k}$ を次の再帰で定める。

$k\ge1$ のとき、$H_{0,k}$ は、部分集合 $A\subset\mathrm{At}_k$ ごとの論理式 $\theta_A:=\bigwedge_{\alpha\in A}\alpha\land\bigwedge_{\alpha\in\mathrm{At}_k\setminus A}\lnot\alpha$ の全体とする（連言は決めた並びの順にとる）。
$n\ge1$ のとき、$H_{n,k}$ は、空でない部分集合 $S\subset H_{n-1,k+1}$ ごとの論理式
$$ \theta_S:=\bigwedge_{\chi\in S}\exists v_{k+1}\,\chi\ \land\ \forall v_{k+1}\bigvee_{\chi\in S}\chi $$
の全体とする。
$L$ 構造 $\mathcal M$ と $\bar a\in M^k$ に対し、その Hintikka 論理式 $\eta^n_{\bar a}\in H_{n,k}$ を次で定める。$n=0$ では $A=\{\alpha\in\mathrm{At}_k:\mathcal M\models\alpha[\bar a]\}$ として $\eta^0_{\bar a}:=\theta_A$、$n\ge1$ では $S=\{\eta^{n-1}_{(\bar a,a)}:a\in M\}$ として $\eta^n_{\bar a}:=\theta_S$。

2 の連言と選言が有限で意味をもつには、$H_{n-1,k+1}$ が有限であることが要る。これは $n$ についての帰納法で分かる。$H_{0,k}$ の元は $\mathrm{At}_k$ の部分集合の個数 $2^{\lvert\mathrm{At}_k\rvert}$ 個以下であり、$H_{n,k}$ の元は $H_{n-1,k+1}$ の部分集合の個数以下である。また帰納法により、$H_{n,k}$ の元の自由変数は $v_1,\dots,v_k$ の中にあり、量化子階数は $n$ 以下である（$\chi$ の自由変数は $v_1,\dots,v_{k+1}$ の中にあり、$v_{k+1}$ は量化されている）。$\eta^n_{\bar a}$ の定義の $S$ は $M\ne\emptyset$ なので空でない。

Hintikka 論理式の 2 つの性質

$L$ を有限個の関係記号だけからなる言語、$n+k\ge1$、$\bar a\in M^k$、$\bar b\in N^k$ とする。

$\mathcal M\models\eta^n_{\bar a}[\bar a]$ である。
$\mathcal N\models\eta^n_{\bar a}[\bar b]$ ならば $\bar a\sim_n\bar b$ である。

n についての帰納法

要点：どちらも $n$ についての帰納法による。1 は各 $a\in M$ が $\exists$ の証拠になり、任意の $c\in M$ で選言の項 $\eta^{n-1}_{(\bar a,c)}$ が真になることから従う。2 は、$\eta^n_{\bar a}$ の $\exists$ の部分から（行き）、$\forall$ の部分から（帰り）を読み取ればよい。

詳しい証明を開く

1：$n=0$ では、$A$ の元は $\bar a$ で真、$\mathrm{At}_k\setminus A$ の元は偽なので、$\theta_A$ は $\bar a$ で真である。$n\ge1$ とする。各 $a\in M$ について、帰納法の仮定により $\mathcal M\models\eta^{n-1}_{(\bar a,a)}[(\bar a,a)]$ なので、$v_{k+1}$ に $a$ を割り当てれば $\exists v_{k+1}\,\eta^{n-1}_{(\bar a,a)}$ が $\bar a$ で真である。また、$v_{k+1}$ に任意の $c\in M$ を割り当てると、$\eta^{n-1}_{(\bar a,c)}\in S$ がそこで真なので、選言 $\bigvee_{\chi\in S}\chi$ が真であり、$\forall v_{k+1}\bigvee_{\chi\in S}\chi$ も $\bar a$ で真である。

2：$n=0$ では、$\mathcal N\models\theta_A[\bar b]$ は「$\alpha\in\mathrm{At}_k$ が $\bar b$ で真 $\iff\alpha\in A\iff\alpha$ が $\bar a$ で真」ということで、これは $a_i\mapsto b_i$ が部分同型であること、すなわち $\bar a\sim_0\bar b$ である。$n\ge1$ とし、lem-efg-back-and-forth の 2 条件を示す。（行き）$a\in M$ をとる。$\eta^{n-1}_{(\bar a,a)}\in S$ なので、$\mathcal N\models\exists v_{k+1}\,\eta^{n-1}_{(\bar a,a)}[\bar b]$ であり、ある $b\in N$ で $\mathcal N\models\eta^{n-1}_{(\bar a,a)}[(\bar b,b)]$ となる。帰納法の仮定により $(\bar a,a)\sim_{n-1}(\bar b,b)$ である。（帰り）$b\in N$ をとる。$\mathcal N\models\forall v_{k+1}\bigvee_{\chi\in S}\chi[\bar b]$ なので、ある $a\in M$ で $\mathcal N\models\eta^{n-1}_{(\bar a,a)}[(\bar b,b)]$ となり、帰納法の仮定により $(\bar a,a)\sim_{n-1}(\bar b,b)$ である。$\square$

Ehrenfeucht–Fraïssé の定理

$L$ を有限個の関係記号だけからなる言語、$\mathcal M,\mathcal N$ を $L$ 構造とする。任意の $n,k\ge0$、$\bar a\in M^k$、$\bar b\in N^k$ について
$$ \bar a\sim_n\bar b\iff(\mathcal M,\bar a)\equiv_n(\mathcal N,\bar b) $$
が成り立つ。特に、$G_n(\mathcal M,\mathcal N)$ で模倣者が勝つことと $\mathcal M\equiv_n\mathcal N$ は同値である。

Hintikka 論理式を相手の構造で読む

$\Rightarrow$ は prop-efg-soundness である。$\Leftarrow$ を示す。$n=k=0$ なら $\mathcal M\sim_0\mathcal N$ はいつでも成り立つ。$n+k\ge1$ とし、$(\mathcal M,\bar a)\equiv_n(\mathcal N,\bar b)$ を仮定する。$\eta^n_{\bar a}$ は自由変数が $v_1,\dots,v_k$ の中にある量化子階数 $n$ 以下の論理式で、lem-efg-hintikka の 1 により $\mathcal M\models\eta^n_{\bar a}[\bar a]$ である。仮定から $\mathcal N\models\eta^n_{\bar a}[\bar b]$ であり、lem-efg-hintikka の 2 により $\bar a\sim_n\bar b$ である。$\square$

初等同値のゲームによる特徴づけ

$L$ を有限個の関係記号だけからなる言語とする。$L$ 構造 $\mathcal M,\mathcal N$ が初等同値であるための必要十分条件は、すべての $n$ で $G_n(\mathcal M,\mathcal N)$ に模倣者が勝つことである。

文の量化子階数は有限

$\mathcal M\equiv\mathcal N$ ならすべての $n$ で $\mathcal M\equiv_n\mathcal N$ なので、thm-efg-main によりすべての $n$ で $\mathcal M\sim_n\mathcal N$ である。逆に、すべての $n$ で $\mathcal M\sim_n\mathcal N$ とする。文 $\sigma$ をとり $n:=\operatorname{qr}(\sigma)$ とすると、thm-efg-main により $\mathcal M\equiv_n\mathcal N$ なので、$\mathcal M\models\sigma\iff\mathcal N\models\sigma$ である。$\square$

thm-efg-main は OLT26 Theorem 25.23・Corollary 25.24（p. 389）に当たる。同書は Proposition 25.19（p. 388。有限な関係言語では量化子階数 $n$ 以下の文は論理的同値を除いて有限個）を使って証明している。上の Hintikka 論理式 $\eta^n_{\bar a}$ の構成は、この有限性を具体的な論理式として取り出したものである。$H_{n,k}$ が有限集合で、量化子階数 $n$ 以下の論理式の真偽はどれも $\eta^n_{\bar a}$ で決まる（thm-efg-main と prop-efg-soundness）ので、自由変数が $v_1,\dots,v_k$ の中にある量化子階数 $n$ 以下の論理式 $\varphi$ の論理的同値の類は、「$\varphi$ を満たす局面の Hintikka 論理式として現れる $H_{n,k}$ の元の集合」で決まる。したがって $n+k\ge1$ のとき、そのような論理式は、論理的同値を除いて $2^{\lvert H_{n,k}\rvert}$ 個以下である。

有限な線形順序

$m\ge1$ について、$L_m:=(\{1,2,\dots,m\},<)$ を通常の順序による $m$ 元の線形順序とする。言語は $\{<\}$ である。

長い有限線形順序は区別できない

$k\ge0$ とする。$m,p\ge 2^k-1$ ならば $L_m\equiv_k L_p$ である。

証明では、模倣者が「選ばれた点どうしの距離が等しいか、どちらも十分に長い」という状態を保つ。両端の外側に仮の点を置くと議論がそろう。

距離を保つか、どちらも長く保つ

要点：両端の外に仮の点 $0$ と $m+1$（$p+1$）を置き、選ばれた点どうしの距離が「等しいか、どちらも $2^r$ 以上」という条件 $C_r$ を考える。$C_r$ ならば $\sim_r$ であることを $r$ についての帰納法で示す。妨害者の点が入った隙間で、隙間の端からの距離を写すか、端から $2^{r-1}$ だけ離れた点を選べば、$C_{r-1}$ が保たれる。最初の局面では距離 $m+1,p+1$ がともに $2^k$ 以上なので $C_k$ が成り立つ。

詳しい証明を開く

$\bar a=(a_1,\dots,a_t)\in\{1,\dots,m\}^t$、$\bar b=(b_1,\dots,b_t)\in\{1,\dots,p\}^t$ に、仮の点 $a_{-1}:=0$、$a_0:=m+1$、$b_{-1}:=0$、$b_0:=p+1$ を添え、添字の集合を $J:=\{-1,0,1,\dots,t\}$ とする。整数 $r\ge0$ について、次の 2 条件を $C_r(\bar a,\bar b)$ と書く。

(a) すべての $j,l\in J$ で、$a_j< a_l\iff b_j< b_l$ かつ $a_j=a_l\iff b_j=b_l$。(b) すべての $j,l\in J$ で、$\lvert a_j-a_l\rvert=\lvert b_j-b_l\rvert$ であるか、$\lvert a_j-a_l\rvert\ge2^r$ かつ $\lvert b_j-b_l\rvert\ge2^r$ である。

主張：$C_r(\bar a,\bar b)$ ならば $\bar a\sim_r\bar b$。$r$ についての帰納法で示す。$r=0$ では、(a) を $j,l\ge1$ に使えば $a_i\mapsto b_i$ は等号と $<$ を保つので部分同型である。

$r\ge1$ とし、$q:=2^{r-1}$ とおく。lem-efg-back-and-forth の（行き）を示す（（帰り）は $L_m$ と $L_p$ の役割を入れ替えて同じである。$C_r$ は対称な条件である）。$a\in\{1,\dots,m\}$ をとり、$C_{r-1}((\bar a,a),(\bar b,b))$ を満たす $b$ を見つければ、帰納法の仮定から $(\bar a,a)\sim_{r-1}(\bar b,b)$ となる。$a$ がある $a_j$（$j\ge1$）に等しければ $b:=b_j$ とすればよい。そうでないとき、$0< a< m+1$ なので、$a_j< a< a_l$ で間にほかの $a_x$（$x\in J$）がない $j,l\in J$ がある。(a) により $b_j< b_l$ で、その間にもほかの $b_x$ はない。次のように $b$ を選ぶ。

$a_l-a_j=b_l-b_j$ のとき：$b:=b_j+(a-a_j)$。そうでないとき、(b) により $a_l-a_j\ge2q$、$b_l-b_j\ge2q$ である。$a-a_j< q$ なら $b:=b_j+(a-a_j)$。このとき $b_l-b> 2q-q=q$、$a_l-a> q$。$a_l-a< q$ なら $b:=b_l-(a_l-a)$。対称に $b-b_j> q$、$a-a_j> q$。$a-a_j\ge q$ かつ $a_l-a\ge q$ なら $b:=b_j+q$。このとき $b-b_j=q$、$b_l-b\ge q$。

どの場合も $b_j< b< b_l$ であり、組 $(a,a_j),(b,b_j)$ と組 $(a,a_l),(b,b_l)$ の距離は、等しいか、どちらも $q$ 以上である。新しい点を加えた $C_{r-1}$ を確かめる。(a) は、$a$ と $b$ が対応する隙間 $(a_j,a_l)$、$(b_j,b_l)$ にあることから従う。(b) は、もとの組については $2^r\ge q$ から従う。新しい点と $a_x$ で $a_x\le a_j$ のものについては $$ \lvert a-a_x\rvert=(a-a_j)+(a_j-a_x),\qquad \lvert b-b_x\rvert=(b-b_j)+(b_j-b_x) $$ と分ける。右辺の 2 つの項の組はそれぞれ「等しいか、どちらも $q$ 以上」なので（2 項目は $C_r$ の (b)）、和も「等しいか、どちらも $q$ 以上」である。$a_x\ge a_l$ の側も同様である。以上で主張が示された。

定理の証明：$t=0$ では $J=\{-1,0\}$ で、(a) は明らかであり、$m+1\ge2^k$、$p+1\ge2^k$ なので (b) も成り立つ。よって $C_k(\emptyset,\emptyset)$ が成り立ち、主張により $L_m\sim_k L_p$、thm-efg-main により $L_m\equiv_k L_p$ である。$\square$

偶奇は一階の文で書けない

順序の言語 $\{<\}$ の文 $\sigma$ で、すべての $m\ge1$ について「$L_m\models\sigma\iff m$ は偶数」となるものは存在しない。

2 つの長い順序を比べる

そのような $\sigma$ があったとし、$k:=\operatorname{qr}(\sigma)$ とする。$2^k$ と $2^k+1$ はどちらも $2^k-1$ 以上なので、thm-efg-linear-orders により $L_{2^k}\equiv_k L_{2^k+1}$ であり、$\sigma$ の真偽は両者で一致する。しかし $2^k$ は偶数、$2^k+1$ は奇数なので、仮定に反する。$\square$

同じ論法で、偶奇のほかにも「長さが 3 の倍数」などの算術的な条件は、有限線形順序の上の一階の文で書けない。量化子階数を固定すると、十分長い有限線形順序はすべて同じ文を満たすからである。

下限の $2^k-1$ は $k=2$ で外せない

$k=2$ では下限は $3$ である。$L_2$ と $L_3$ は、量化子階数 $2$ の文 $\exists x\,(\exists y\,(y< x)\land\exists y\,(x< y))$（「両側に元をもつ元がある」）で区別される。$L_3$ では $2$ がこれを満たし、$L_2$ ではどちらの元も一方の側にしか元をもたない。ゲームでは、妨害者は第 1 手で $L_3$ の $2$ を選び、模倣者が $L_2$ のどちらの元で応じても、第 2 手でその元の反対側にある $L_3$ の元を選べば勝つ。

反例：条件を外すと成り立たない

外す条件	反例	成り立たなくなること
thm-efg-main の「言語が有限」	1 項関係記号 $P_1,P_2,\dots$ の言語の構造 $\mathcal M,\mathcal N$（下の確かめ）	$\mathcal M\equiv_1\mathcal N$ から $\mathcal M\sim_1\mathcal N$ を導くこと
部分同型の「等号を保つ」	ex-efg-counting の $\mathcal M,\mathcal N$	「勝ち」を関係記号だけで判定したとき、模倣者の勝ちから $\mathcal M\equiv_2\mathcal N$ を導くこと
thm-efg-linear-orders の「$m,p\ge2^k-1$」	$L_2$ と $L_3$、$k=2$	$L_m\equiv_k L_p$
往復条件をもつ部分同型の族から同型を導くときの「可算」（OLT26 Theorem 25.16）	$(\mathbb Q,<)$ と $(\mathbb R,<)$	同型であること

反例の確かめ

1 行目：$N:=\{c_1,c_2,\dots\}$ とし、$c_i\in P_j^{\mathcal N}\iff i\ne j$ と定める（$c_i$ は $P_i$ だけを満たさない）。$\mathcal M$ は $N$ に新しい元 $c_0$ を 1 つ加え、$c_0$ はすべての $P_j$ を満たすとする（$c_i$ についてはそのまま）。妨害者が $\mathcal M$ から $c_0$ を選ぶと、模倣者の応答 $c_i$ は $P_i$ を満たさないので、$\mathcal M\sim_1\mathcal N$ でない。一方、量化子階数 $1$ の文は、自由変数が $x$ だけの量化記号のない論理式 $\chi(x)$ による $\exists x\,\chi$、$\forall x\,\chi$ を $\lnot,\land,\lor,\to$ で組み合わせたものである。$\chi$ に現れる $P_j$ は有限個なので、それに現れない $i$ をとれば、$c_i$ は $\chi$ に現れるすべての $P_j$ を満たし、$\chi$ に関しては $c_0$ と区別されない。よって $\mathcal M$ と $\mathcal N$ で「$\chi$ を満たす元があるか」「すべての元が $\chi$ を満たすか」は一致し、$\mathcal M\equiv_1\mathcal N$ である。prop-efg-soundness は有限性なしで成り立つので、壊れるのは逆向きだけである。
2 行目：ex-efg-counting で、勝ちの判定に $P$ だけを使い等号を見ないとすると、妨害者の 2 手に模倣者は $P$ の真偽をそろえて応じ続けられるので、模倣者が勝つ。しかし量化子階数 $2$ の文 $\exists x\,\exists y\,(\lnot x=y\land P(x)\land P(y))$ が両者を区別するので、$\mathcal M\equiv_2\mathcal N$ でない。
3 行目：ex-efg-bound で確かめた。
4 行目：ex-efg-dlo の一歩により、$(\mathbb Q,<)$ と $(\mathbb R,<)$ の間の有限な部分同型の全体は（行き）（帰り）の拡張をもつ族になる（とくにすべての $n$ で $(\mathbb Q,<)\sim_n(\mathbb R,<)$）が、濃度が違うので同型でない。可算な構造どうしでは、部分同型の族が往復条件をもてば同型であり（OLT26 Theorem 25.16、p. 387）、端点のない可算な稠密線形順序はすべて同型になる（カテゴリー性の記事の定理「Cantor の定理」）。一定の回数のゲームでの勝ちは同型を与えないので、両者は区別して扱う。

分野ごとの使われ方

モデル理論：2 つの構造の初等同値を示す手段として、完全な理論の判定や量化記号消去と並んで使われる。往復の議論を有限回で打ち切ったものなので、カテゴリー性の記事の往復論法とは同じ一歩の拡張を共有する。
有限モデル理論：有限構造の性質が一階の文で書けないことを示す標準的な方法である。cor-efg-parity のように、性質をもつ構造ともたない構造の組を量化子階数ごとに用意し、ゲームで模倣者が勝つことを示す。
計算との関係：文を固定すると、有限構造でのその文の真偽は、構造の大きさの多項式回の手順で決まる（Tarskiの真理定義の記事の定理「有限構造での真偽の計算」）。偶奇のように計算は易しくても一階の文で書けない性質があるので、EF ゲームが測るのは計算の難しさとは別の、表現力の限界である。