有限模型论/FO EFM

使用 Ehrenfeucht-Fraisse 游戏来证明（不）可表达性的方法由以下定理给出

定理

令 P 为有限 σ 结构的一个性质。则以下等价

• P 在 FO 中不可表达
• 对于每个 k $\in \mathbb {N}$ 存在两个有限 σ 结构 ${\mathfrak {A}}_{k}$ 和 ${\mathfrak {B}}_{k}$，使得以下两个条件都满足
  • ${\mathfrak {A}}_{k}\equiv _{k}{\mathfrak {B}}_{k}$
  • ${\mathfrak {A}}_{k}$ 具有 P，而 ${\mathfrak {B}}_{k}$ 不具有 P

备注

• 因此，使用 EFM 的工作原理大致如下
  • 选择一个 k
  • 构建两个结构 - 一个具有该性质，另一个没有 - 它们足够大，使得复制者在 k 元 EFG 中获胜
  • 证明这可以随着 k 的增加而扩展
• 因此，不可表达的性质（即检查它的努力）必须以某种方式随着 k 的增加而“扩展”。

示例

• 首先选择两个线性序，例如 A ={1, 2, 3, 4} 和 B ={1, 2, 3, 4, 5}。对于一个两步的 Ehrenfeucht 游戏，D 显然会获胜。这为我们提供了两个满足上述条件的结构，其中 k = 2，性质具有偶数基数（A 具有而 B 没有）。现在我们必须将其扩展到所有 k $\in \mathbb {N}$。从上面的例子中，我们知道，在基数为 $2^{k}$ 或更高的线性序中，D 具有获胜策略。因此，我们根据 k 选择基数，使 |A| = $2^{k}$ 且 |B| = $2^{k}$+1。因此，我们为每个 k 都找到了一个偶数 A 和一个奇数 B，其中 D 具有获胜策略。因此（根据推论），对于有限的 σ 结构的线性序，具有偶数/奇数基数是不能在 FO 中表达的性质。