有限模型論/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 中表達的性質。