Ehrenfeucht–Fraïssé 博弈

一个存在量词请求一个见证。假如左侧公式 $\mathrm{\exists }y\psi (\overline{x},y)$ 为真，挑战者可以把左侧见证当作下一步选点；应答者必须在右侧找到一个点，让余下的公式仍看不出差别。全称量词可经否定转成存在量词，因此允许挑战者从两边发起请求，恰好对应真假保持所需的两个方向。

量词秩给出的资源是“选完一个见证之后，还能向内追问几层”。布尔联结词可以把许多检查并列起来，但不会增加后续选点的深度。游戏据此用轮数衡量观察能力，不要求应答者提前给出整个结构之间的同构。

从获胜策略到公式一致 ​

对公式结构归纳，并同时考虑所有足够大的剩余轮数。原子公式由部分同构保证；否定和合取直接沿用归纳结论。一个能赢 $k$ 轮的策略截断后也能赢更少轮数，所以这些布尔步骤不消耗轮数。

设 $\mathrm{qr}(\mathrm{\exists }y\psi )\le k$，且 $\mathcal{A}\models \mathrm{\exists }y\psi [\overline{a}]$。取见证 $a\in A$，让挑战者选择它；获胜策略给出应答 $b\in B$，并从扩展位置继续赢 $k-1$ 轮。因为 $\mathrm{qr}(\psi )\le k-1$，归纳假设给出

右侧因此也有存在见证。若存在句先在 $\mathcal{B}$ 为真，就让挑战者从 $\mathcal{B}$ 选其见证，同理得到反向。全称量词由 $\mathrm{\forall }y\psi \equiv \mathrm{\neg }\mathrm{\exists }y\mathrm{\neg }\psi$ 处理，正向证明完成。

有限秩类型为什么只有有限种 ​

反向证明的难点是：如果某个选点没有合适应答，怎样用一个有限公式表达这种失败？不能为无限结构中的每个候选应答各写一个排除条件，再取无限合取。有限关系签名使我们能够按有限种公式类型归类候选点。

对每个元组长度 $n$，令 ${\mathrm{At}}_n$ 为变量 $x_1,\dots ,x_n$ 上的全部原子公式。它是有限集：项只有变量，关系符号也只有有限多个。零秩类型由这些原子的真值表确定。对每个可实现的真值表 $\tau$，写出其特征公式

“可实现”指存在某个 $L$-结构及其中的元组具有该真值表；不满足相等关系规律的表无需保留。于是得到有限族 $H_{0,n}$，每个位置恰好满足其中一个公式，并且该公式决定所有零秩公式的真假。

这里采用明确的语法约定：空合取为布尔常量 $\mathrm{\top }$，空析取为 $\mathrm{\perp }$，二者的量词秩都为 $0$。因此，当 $n=0$ 且没有零元关系时，${\mathrm{At}}_0$ 为空，$H_{0,0}=\{\mathrm{\top }\}$。这些常量仅表达恒真、恒假，不增加观察结构的能力；不能把此处的 $\mathrm{\top }$ 换成带量词的 $\mathrm{\forall }x(x=x)$ 后仍声称它的秩为 $0$。

现在假设已对所有元组长度构造有限族 $H_{r,n}$，其中每个公式的秩不超过 $r$，且唯一刻画一个秩 $r$ 类型。对位置 $(\mathcal{A},\overline{a})$，记录它的零秩类型 $\tau$，以及在追加一个元素时实际出现的类型集合

这个位置对应的下一秩特征公式为

对束缚变量作必要改名，避免捕获。前半部分要求 $S$ 中的每种类型确实出现，最后一项排除 $S$ 外的类型。由于 $H_{r,n+1}$ 有限，$S$ 只有有限种可能，公式中的合取与析取也都有限；其秩至多为 $r+1$。只收集可实现的 $(\tau ,S)$，便得到 $H_{r+1,n}$。

还须证明这个记录确实决定全部秩至多 $r+1$ 的公式。对这类公式作结构归纳：原子由 $\tau$ 决定，布尔组合继承其子公式的真值；对 $\mathrm{\exists }y\psi$，内部公式的秩至多为 $r$，根据上一秩的归纳假设，它在每个 $\theta \in H_{r,n+1}$ 上有固定真值。因此存在句为真，当且仅当 $S$ 中至少有一种类型使 $\psi$ 为真。全称量词同理。反过来，不同 $(\tau ,S)$ 被相应的特征公式区分，所以这一构造恰好给出有限种秩 $r+1$ 类型。

从公式一致构造获胜策略 ​

设当前位置满足 ${\equiv }_k$，且 $k>0$。若挑战者选择 $a\in A$，取扩展位置 $(\mathcal{A},\overline{a},a)$ 在 $H_{k-1,n+1}$ 中的特征公式 $\theta$。因为

当前的 $k$ 秩一致性保证右侧也满足这个存在句。选取右侧任一见证 $b$，扩展位置便满足 ${\equiv }_{k-1}$。挑战者从右边选点时交换两侧，使用同一论证。

将该规则逐轮应用，剩余轮数从 $k$ 降到 $0$，每一步都保留相应秩的一致性；零秩一致性正是原子事实一致。每个可能的挑战都存在这种应答，因此它定义了获胜策略，而不只是事后为某一条对局寻找匹配。至此，EF 定理的两个方向都得到证明。

有限线性序中的间隙策略 ​

令 $L_n=(\{1,\dots ,n\},<)$ 为纯严格线性序，签名仅含 $<$。定义

我们证明一个充分条件：若 $n,m\ge T_k$，则应答者在 $L_n$ 与 $L_m$ 上能赢 $k$ 轮。

把已选的不同元素按顺序排列，它们将每个序分成若干间隙，包括最左和最右的外侧间隙。间隙大小只数尚未选中的元素；端点没有预先选定。策略始终保持选中点的对应保序，并在剩余 $r$ 轮时保持如下不变量：每对对应间隙大小相等，或者二者都至少为 $T_r$。开始没有选点，唯一间隙就是整个论域，因此假设保证不变量成立。

如果挑战者选旧点，就回应它原来的对应点；间隙不变，而阈值下降，不变量仍成立。若选新点，设它在大小为 $N$ 的间隙中留下左侧 $\ell$ 个、右侧 $u$ 个未选元素，于是 $\ell +u+1=N$。令 $t=T_{r-1}$。下面的规则对从任意一边发起的选择都适用。

• 若两个间隙同样大，在另一边复制这个点距左端的偏移量，得到完全相同的两个子间隙。
• 若两边大小都至少为 $T_r=2t+1$，且 $\ell <t$，就复制左侧偏移量 $\ell$。两边新产生的左间隙相等，右间隙都至少为 $t$。
• 若两边都大且 $u<t$，则从右侧复制偏移量 $u$，得到相等的右间隙和都至少为 $t$ 的左间隙。
• 若 $\ell ,u\ge t$，就选择另一边的一个点，使它左右也都至少剩 $t$ 个元素；另一间隙至少有 $2t+1$ 个元素，故这样的点存在。

这些情形覆盖所有新点选择。在大间隙中，$\ell <t$ 和 $u<t$ 不可能同时发生，否则 $N=\ell +u+1<2t+1$。在复制小侧的情形，另一侧之所以仍足够大，是因为从一个至少含 $2t+1$ 个元素的间隙中只移去一个点和少于 $t$ 个元素。所有未被切分的间隙也继续满足下降后的阈值。因此不变量逐轮保持，到 $r=0$ 时选中点仍保序且保持相等关系，正好构成纯序语言中的部分同构。

七个点与八个点：逐轮检查 ​

取 $n=7,m=8,k=3$。因为 $T_3=7$，上述策略保证三轮获胜。下面展示其中一条对局；元组按轮次记录，间隙则按选中点的左右次序记录。

第二轮双方都在 $4$ 右侧选点。这个间隙在两边分别有 $3$ 与 $4$ 个元素；选择 $6$ 后，左子间隙都只含 $5$，右子间隙分别含 $7$ 和 $7,8$。它们虽不一样大，却都足以承受最后一轮。第三轮的最终对应为 $4\mapsto 4,6\mapsto 6,7\mapsto 8$，保留了三个点之间的每个大小关系。

图中两次切分后，所有不等大的对应间隙仍达到剩余轮数所需的阈值。实心圈是已选点，虚线连接对应点，括号标出未选元素的数量；图只画这条对局的前两轮。无论最后一轮选择 $8$、其他新点还是旧点，前述分类规则都能给出应答，这才是三轮获胜的依据。

阈值附近确实能出现区别 ​

七点和八点三轮不可区分，不意味着六点和七点也如此。定义“$z$ 左侧至少有三个点”和“$z$ 右侧至少有三个点”的公式

严格线性序的传递性保证，前者给出 $u<v<w<z$，后者给出 $z<u<v<w$。每个公式的秩为 $2$，故句子

的秩为 $3$。它在 $L_7$ 中可由 $z=4$ 见证，在 $L_6$ 中为假，因为左右各三个点加上中心点至少需要七个点。由 EF 定理，六点和七点不存在三轮应答者获胜策略。这也显示量词嵌套能通过左右分支表达比“逐个量化所有点”更有效的计数条件。

定理的适用范围 ​

固定 $k$ 的游戏等价并不推出同构：$L_7$ 与 $L_8$ 就连基数也不同。它们也不满足完全相同的一阶句子，例如“至少有八个不同元素”能够区分二者，只是它不可能具有三以内的量词秩。每个有限轮数各有一个策略，也不能未经证明就拼成无限轮的同一个策略。

有限签名和没有函数项是本页有限类型证明的实质条件。若允许任意深度的函数项，即使变量个数固定，原子公式也可能已有无限多个；无限关系签名同样破坏原子公式集合的有限性。更一般语言中的 EF 定理需要另外说明规则与假设，不能直接沿用这里“有限合取所有类型”的步骤。

纯有限线性序无法用一阶句子定义奇偶性 ​

假设有一个纯序语言的一阶句子 $\phi$，恰好在所有偶数大小的有限非空线性序中成立。它的量词秩是某个有限整数 $k$。取 $q=max\{k,1\}$，考虑 $L_{2^q}$ 与 $L_{2^q+1}$：前者大小为偶数，后者为奇数，而且两者大小都至少为 $T_q$。

间隙策略保证两者在 $q$ 轮内不可区分，EF 定理因而保证它们对所有秩不超过 $q$ 的句子真值相同，尤其对 $\phi$ 相同。这与奇偶性要求矛盾。因此不存在这样的一阶句子。

该结论针对只有 $<$ 的语言，以及涵盖任意有限大小的整个结构类。若只允许有界大小，便可以逐一列出所需的基数；若增加能够编码奇偶信息的谓词、适当的算术结构或计数量词，所研究的语言已经改变，需要重新分析表达力。

从语义递归到不可定义性证明 ​

EF 方法的一般用法是：假设某个性质由一个句子定义，把该句子的秩记为 $k$；再为任意 $k$ 构造一对在目标性质上不同、但应答者能赢 $k$ 轮的结构。真正需要设计的是适合该结构类的不变量。本例中不变量是间隙内尚未选中的元素数量，递推式 $T_r=2T_{r-1}+1$ 则精确描述一个新点把未来选择空间切成两半的代价。

这与模态互模拟公理库模态互模拟Modal bisimulation · Kripke bisimulation用原子一致与沿可达边的 forth、back 条件比较两个 Kripke 模型的模态行为。的见证匹配思路相通，但观察能力不同。普通模态博弈沿可达边移动，EF 博弈允许在整个论域中任选元素，并保留选中元组的全部原子关系与相等事实。因此要先确定语言和游戏规则，再讨论哪种不可区分性适合目标问题。