計算機科學邏輯/查詢證明

部分同構

定義（關係型 S-結構上的部分同構）

令 ${\mathfrak {A}}$ 和 ${\mathfrak {B}}$ 是關係型 S-結構，p 是一個對映。則當以下所有條件成立時，稱 p 為從 ${\mathfrak {A}}$ 到 ${\mathfrak {B}}$ 的部分同構：

dom(p) $\subset$ A 且 codom(p) $\subset$ B
對於每個 $a_{1}$ ， $a_{2}$ ： $a_{1}$ = $a_{2}$ 當且僅當 p( $a_{1}$ ) = p( $a_{2}$ ).
對於每個來自 S 的常量符號 c 和每個 a：a = c 當且僅當 p(a) = c
對於 S 中的每個 n 元關係符號 R 和 $a_{1}$ , ..., $a_{n}$ : $R^{\mathfrak {A}}$ $a_{1}$ ... $a_{n}$ 當且僅當 $R^{\mathfrak {B}}$ $p(a_{1})$ ... $p(a_{n})$

其中 $a_{*}$ $\in$ A, $b_{*}$ $\in$ B.

備註

也就是說， ${\mathfrak {A}}$ 和 ${\mathfrak {B}}$ 上的偏同構是在透過選擇 dom(p) 和 codom(p) 並分別“修剪”常量和關係而獲得的子結構上的（普通）同構。

示例

令 S = {<} 在 A = {1, 2, 3} 和 B = {3, 4, 5, 6} 上以“通常”方式定義。那麼 $p_{1}$ ，其中 1->3 和 2->4，是一個偏同構（因為 1 < 2 並且 p(1) < p(2)），同樣 $p_{3}$ ，其中 2->3 和 3->6，以及 $p_{2}$ ，其中 1->6，也是。而 $p_{4}$ ，其中 1->6 和 2->3（因為 1 < 2 但 p(1) 不小於 p(2)），以及 $p_{5}$ ，其中 2->5 和 3->5，都不是偏同構。

設 S = {R}，其中 $R^{\mathfrak {A}}=\{(1,2),(2,3),(3,4),(4,1)\}$ （一個“正方形”）和 $R^{\mathfrak {B}}=\{(1,2),(1,3),(3,4),(3,5)\}$ （一個“二叉樹”）。A = {1, ..., 4} 和 B = {1, ..., 5}。那麼 p: {1, 2, 3} -> {1, 3, 4} 其中 1 -> 1，2 -> 3，3 -> 4 是從 ${\mathfrak {A}}$ 到 ${\mathfrak {B}}$ 的一個區域性同構，因為 {(1, 2), (2, 3)} 變成了 {(1, 3), (3, 4)}。注意，如果 $R_{\mathfrak {B}}$ 還包含例如 (4, 1)，那麼 p 就不是區域性同構。

設 S = {<} 在 A = {1, 2, 3, 4, 5, 6} 和 B = {1, 3, 5} 上以“通常”的方式定義。那麼 p 其中 2 -> 3 和 4 -> 5 定義了一個區域性同構。注意例如 $\exists _{x}(x<4\land 2<x)$ 在 ${\mathfrak {A}}$ 上成立，但 $\exists _{x}(x<p(4)\land p(2)<x)$ 在 ${\mathfrak {B}}$ 上不成立。也就是說，通常情況下，帶有量詞的句子的有效性不會被保留。因此，為了保留這種有效性，我們需要比區域性同構更強的東西。這主要就是 Ehrenfeucht-Fraisse 遊戲要提供給我們的。

定義

假設我們有兩個結構 ${\mathfrak {A}}$ 和 ${\mathfrak {B}}$ ，每個結構都沒有函式符號，但具有相同的關係列符號集，並且有一個固定的自然數 n。

那麼 Ehrenfeucht-Fraisse 遊戲就是一個具有以下屬性的遊戲

元素
- 一個位置是一對序列 α 和 β，兩者長度均為 i，i $\in$ 0, ..., n
- 起始位置是空序列對（i = 0）
- 遊戲結束當且僅當 α 和 β 的長度都為 n
- 玩家是“破壞者” S 和“複製者” D
移動
- 移動輪流進行
- S 先移動
- S 從 A 或 B 中選擇一個尚未被選中的元素（在第一次移動中不相關）
- D 從另一個集合中選擇一個元素，即如果 S 從 A 中選擇了一個元素，那麼 D 必須從 B 中選擇一個元素，反之亦然。
獲勝與資訊
- D 獲勝當且僅當最終位置透過將 α 和 β 的第 i 個元素（對於所有 i）進行對映來定義區域性同構。
- 否則 S 獲勝
- 兩個玩家都完全瞭解這兩個結構，也知道之前所有進行的移動

備註

示例

設 A = {1, 2, 3}，B = {1, 2}，S = { < }，其中“<”以“通常”的方式定義。在這裡，玩家 S 可以透過在第一次移動中選擇 2，並在第二次移動中根據 D 的第一次移動以以下方式進行響應來獲勝：如果 D 選擇了 1，他響應 1；如果 D 選擇了 2，他響應 3。在這兩種情況下，D 都無法繼續。他可能擁有同構的結構，例如 {2, 3} 和 {1, 2}，但由移動序列定義的對映是扭曲的，即它將 2 對映到 2（第一次移動）並將 3 對映到 1，因此不是區域性同構。

設 A ={1, 2, ..., 9}, B ={1, 2, ..., 8}, S ={ < }, 其中 '<' 按“通常”方式定義。那麼，S 最佳的玩法是什麼？如果 S 從 A 中選擇 1，D 從 B 中選擇 1，剩下的遊戲本質上與之前相同，只是少了一個元素，而且已經進行了一步。但是我們可以透過一步操作獲得更好的結果：在 A 中選擇 5，D 就被迫在 B 中選擇 5（或 4），這會讓 S 剩下兩種可能的繼續方式：要麼進行 {1, 2, 3, 4} vs {1, 2, 3, 4} 的遊戲，這將明顯導致 D 的勝利，要麼進行 {6, 7, 8, 9} vs {6, 7, 8} 的遊戲。選擇後者，S 最快的獲勝方式是 7 - 7，8 - 8，最後是 9，四步獲勝。由於雙方都沒有更好的玩法，因此如果 n > 3，S 對於上述結構將獲勝。

標題
以下是一個 (流行的) Ehrenfeucht 遊戲的示例性表示：從兩個序列中，S 獲勝當且僅當連線匹配字母的線交叉（如果 D 根本可以找到匹配），例如，S 在三步之後獲勝

...

定義

函式 qr(φ) 被稱為 φ 的量詞秩當且僅當

$qr(\varphi )=0$ , 對於原子 φ
$qr(\varphi _{1}\land \varphi _{2})=qr(\varphi _{1}\lor \varphi _{2})=max(qr(\varphi _{1}),qr(\varphi _{2}))$
$qr(\lnot \varphi )=qr(\varphi )$
$qr(\forall \varphi )=qr(\exists \varphi )=qr(\varphi )+1$

備註

示例

句子 $\forall _{x}(\exists _{y}((\lnot x=y)\land xRy))\land (\exists _{y}((\lnot x=z)\land zRx))$ 的量詞秩為 2。
前束正規化中的句子 $\forall _{x}\exists _{y}\exists _{y}((\lnot x=y)\land xRy)\land ((\lnot x=z)\land zRx)$ 的量詞秩為 3。注意它等價於上面的句子。

...

定理

令 ${\mathfrak {A}}$ 和 ${\mathfrak {B}}$ 是關係詞匯表中的兩個結構。那麼以下等價：

備註

考慮 Ehrenfeucht-Fraisse 博弈來判斷表達性的基礎是根據上面定理的以下推論：

推論

令 P 是有限 σ-結構的一個性質。那麼以下等價：

P 在 FO 中不可表達
對於任意 k $\in \mathbb {N}$ $\in \mathbb {N}$ ，存在兩個有限 σ-結構 ${\mathfrak {A}}_{k}$ ${\mathfrak {A}}_{k}$ 和 ${\mathfrak {B}}_{k}$ ${\mathfrak {B}}_{k}$ ，使得以下兩個條件都滿足：
- ${\mathfrak {A}}_{k}\equiv _{k}{\mathfrak {B}}_{k}$
- ${\mathfrak {A}}_{k}$ 具有性質 P，而 ${\mathfrak {B}}_{k}$ 不具有性質 P。

示例

首先，選擇兩個線性序，例如 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 表達。
一般來說，圖是研究 FO 表達性的一個熱門物件。例如，可以證明以下性質在 FO 中不可定義：
- 連通性
- 迴圈性
- 平面性
- 哈密頓性
- n-可著色性
- 等等。

...