计算机科学逻辑/查询证明

部分同构

定义（关系型 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-可着色性
- 等等。

...