结构
线性序 + 两图
直觉：每多玩一轮，Spoiler 就能把「还看得出差别的区间」再对半切一次；能被区分的长度随轮数翻倍，于是阈值是 2k−1。
图的 EF 博弈没有像线性序那样的闭式判据，只能对每对具体结构、每个 k 逐一穷举（工坊里的 AI 正是这么做的）。这也在提示：「能不能分辨」本身依赖于我们面对的是一族什么样的结构。
桌上摆着两个结构 A 和 B（可以是有序的数列，也可以是两张图）。Spoiler（挑衅者）想证明它们不一样，Duplicator（模仿者）想证明它们一样。每轮：Spoiler 在任一边点一个元素，Duplicator 在另一边点一个回应，并且已经配好对的元素之间必须保持结构一致——数序里谁大谁小要对得上，图里谁连着谁要对得上（这叫部分同构）。玩 k 轮；Duplicator 撑到最后就赢。
关键洞察是：Duplicator 撑过 k 轮，等价于「没有任何一个用 k 个量词写成的逻辑命题能把 A、B 区分开」。一个关于「猜」的游戏，被证明等于一个关于「逻辑表达能力」的定理。
法国数学家 Roland Fraïssé 在 1954 年的论文 «Sur quelques classifications des systèmes de relations» 里，为了给「关系结构」分类，发明了来回法（méthode de va-et-vient）：你挑一个元素，我挑一个对应的元素，如此来回，看能撑多久。他用这套方法刻画了今天称作 Fraïssé 极限 的齐次结构——比如「稠密线性序」「随机图」都是这种意义上「最规矩」的结构。
波兰裔数学家 Andrzej Ehrenfeucht 在 1961 年发表 «An application of games to the completeness problem for formalized theories»（载于 Fundamenta Mathematicae），把来回法正式写成了有输赢的两人博弈，并把「回合数」和「逻辑公式的量词个数」精确对齐。今天这套游戏就叫 Ehrenfeucht–Fraïssé 博弈，是模型论的标准工具。
那张穷举表里的「阈值 1、3、7、15」，正是这条对齐关系的一个漂亮推论。
若两个结构在所有（一阶逻辑）句子上都取相同的真假，称它们初等等价，记 A ≡ B。把句子按量词秩分层，就得到一列越来越细的等价关系 A ≡₀ B, A ≡₁ B, A ≡₂ B, …。埃伦福伊希特的定理说：A ≡ₖ B ⟺ Duplicator 在 A、B 上赢 k 轮。
于是就可以反过来用：每当 Duplicator 有 k 轮必胜策略，就说明「任何量词数 ≤ k 的一阶命题都区分不开这两个结构」。
20 世纪后半叶，人们开始问：「计算」这个动作，能用逻辑写出来吗？描述复杂性把可计算性翻译成逻辑的可定义性：Fagin 定理（1974）说 NP = 存在二阶逻辑（∃SO）；Immerman 与 Vardi（均 1982）证明：在带序的有限结构上，PTIME = 一阶逻辑 + 最小不动点（FO(LFP)）。
但请注意那个「+ 最小不动点」——光有一阶逻辑 FO 是远远不够的。用 EF 博弈（或它的变体）可以证明：像「图是否连通」「能不能到达」这类性质，根本写不成一阶逻辑的句子——Duplicator 总能撑住。这就是「FO 与 PTIME 之间的鸿沟」：要让逻辑拥有与多项式时间同等的算力，必须额外给它一个递归/迭代的机制。逻辑与计算之间这座桥该怎么搭，至今仍有未解之谜。
所以下次玩这个游戏时不妨记住：你手里那只「窥探之眼」，同时也在丈量一阶逻辑能看多远。