2.4. Godel 完备性定理

很显然, 这一节的主要目的是像证明零阶语言即命题逻辑的可靠性和完备性一样, 试着证明一阶逻辑的可靠性与完备性. Godel 于 1929 年首次得到了完备性的证明, 并在 1930 年公之于世. 我们将要给出的证明方法则是 Henkin 在 1949 年提出的. 看到这些人物的名字, 读者大约能猜到这个定理并不好证.

首先, 我们还是证一下可靠性. 由于语言更复杂了, 公理的数目大大增多, 可靠性也没有之前那么显然. 先来看一个引理.

引理 2.4.0.1 (替换引理). 如果项 $t$ 可以在公式 $φ$ 中无冲突地替换变元 $x$ , 则 $(M, s) ⊨ φ_{t}^{x}$ 当且仅当 $(M, s_{s (t)}^{x}) ⊨ φ$ .

证明. 还是对公式 $φ$ 实行归纳.

1.	$φ$ 形如 $P (t_{1}, t_{2}, ..., t_{n})$ . 此时 $(M, s) ⊨ P (t_{1}, t_{2}, ..., t_{n})_{t}^{x}$ 当且仅当 $(s ((t_{1})_{t}^{x}), s ((t_{2})_{t}^{x}), ..., s (t_{n})_{t}^{x}) \in P^{M}$ 当且仅当 $(s_{s (t)}^{x} (t_{1}), s_{s (t)}^{x} (t_{2}), ..., s_{s (t)}^{x} (t_{n})) \in P^{M}$ 当且仅当 $(M, s_{s (t)}^{x}) ⊨ P (t_{1}, t_{2}, ..., t_{n})$ .
2.	$φ$ 形如 $t_{1} \approx t_{2}$ . 与上类似.
3.	$φ$ 形如 $\forall y (ϕ)$ . 此时若 $x$ 不在 $φ$ 中自由出现, 则由自由变元决定性显然. 下讨论自由出现的情形: 注意到无冲突替换要求 $y$ 不在 $t$ 出现且 $t$ 在 $ϕ$ 中也可以无冲突替换, 这说明对任何 $d$ 都有 $s (t) = s_{d}^{y} (t)$ . 又注意到 $φ_{t}^{x} = \forall y (ϕ_{t}^{x})$ , 可如下做连续等价推导: $(M, s) ⊨ φ_{t}^{x}$ 当且仅当对所有的 $d$ , $(M, s_{d}^{y}) ⊨ ϕ_{t}^{x}$ 当且仅当 (归纳假设) 对所有的 $d$ , $(M, (s_{d}^{y})_{s_{d}^{y} (t)}^{x}) ⊨ ϕ$ 当且仅当对所有的 $d$ , $(M, (s_{d}^{y})_{s (t)}^{x}) ⊨ ϕ$ 当且仅当对所有的 $d$ , $(M, (s_{s (t)}^{x})_{d}^{y}) ⊨ ϕ$ 当且仅当 $(M, s_{s (t)}^{x}) ⊨ ϕ$ .
4.	$φ$ 形如 $\neg ϕ$ . 此时 $(M, s) ⊨ φ_{t}^{x}$ 当且仅当 $(M, s) \neq ⊨ ϕ_{t}^{x}$ 当且仅当 $(M, s_{s (t)}^{x}) \neq ⊨ ϕ$ 当且仅当 $(M, s_{s (t)}^{x}) ⊨ φ$ .
5.	$φ$ 形如 $ϕ \to ψ$ . 类上.

$□$

下面来证明可靠性.

定理 2.4.0.2 (可靠性定理). 一阶逻辑是可靠的. 换言之, $Σ ⊢ φ$ 蕴含 $Σ ⊨ φ$ .

证明. 首先, 分离规则保持有效性是显然的, 因此只需要证明每条公理都普遍有效 (valid). 换言之, $\emptyset ⊨ φ$ .

由于公理有好几种, 而且还允许任意全称概括, 我们需要把这个定理归纳地拆成几个部分来证明.

(1) 第一组公理, 即从命题逻辑中继承的公理的有效性: 只需注意到赋值在所有素公式 (没有逻辑连接词的公式) 上的取值可以决定它在所有公式上的取值.

(2) 第二组公理: 我们已知的是 $(M, s) ⊨ \forall x (φ)$ , 欲证的则是 $(M, s) ⊨ φ_{t}^{x}$ , 而根据替换引理只要证 $(M, s_{s (t)}^{x}) ⊨ φ$ , 而这只要按定义展开条件中的全称量词, 然后选取 $d = s (t)$ 即可.

(3) 第三组公理: 拆开 $\forall$ 的定义, 在每个 $d$ 上面分离, 显然.

(4) 第四组公理: 拆开 $\forall$ 的定义, 由自由出现变元的决定性显然.

(5) 第五组公理: 显然.

(6) 第六组公理: 考察所有满足 $x \approx y$ 的模型与赋值, 不难归纳得出它在每个项上都可以将任意个 $x$ 替换为 $y$ 而不改变真假, 进而原子公式, 进而素公式, 进而全体公式.

最后还要证明,

φ

普遍有效当且仅当它的某个全称概括

\forall x (φ)

普遍有效, 而这由普遍有效的定义不难证明.

$□$

接下来证明完备性定理. 我们当然还是模仿在命题逻辑中使用的方法, 先使用以下引理.

引理 2.4.0.3. 一阶逻辑完备当且仅当任意一个一致的公式集都是可满足的.

其证明与命题逻辑中的证明也类似, 这里略去. 下面再证明三个可能用到的元定理.

引理 2.4.0.4 (常数概括引理). 若 $Γ ⊢ φ$ , 而常元符号 $c$ 不在 $Γ$ 中出现, 则存在同样不在 $Γ$ 中出现的变元符号 $y$ , 使得 $Γ ⊢ φ_{y}^{c}$ . 更进一步, 还存在一个 $Γ ⊢ \forall y φ_{y}^{c}$ 的不包含 $c$ 的推演序列.

证明. 我们先证明前面. 考虑 $Γ ⊢ φ$ 的推演序列 $(φ_{0}, φ_{1}, ..., φ_{n} = φ)$ . 有限个公式只出现有限个变元, 所以我们随便拿一个没出现在这些公式中的变元 $y$ , 不难发现 $((φ_{0})_{y}^{c}, (φ_{1})_{y}^{c}, ..., (φ_{n})_{y}^{c} = φ_{y}^{c})$ 是 $Γ$ 到 $φ_{y}^{c}$ 的一个推演序列.

下面验证更进一步的部分. 由于推演序列是有限长度的, 我们一定有一个

Γ_{0} \subseteq Γ

为有限集,

Γ_{0} ⊢ φ

, 进而

Γ_{0} ⊢ φ_{y}^{c}

, 进而直接从这里就能由概括公理得出

Γ_{0} ⊢ \forall y (φ_{y}^{c})

, 而这一步也没有加入新的常数符号, 所以

Γ ⊢ \forall y φ_{y}^{c}

的这个推演序列没用到

c

.

$□$

引理 2.4.0.5 (循环替换引理). 如果变元 $y$ 不在公式 $φ$ 中出现, 则变元 $x$ 可以在公式 $φ_{y}^{x}$ 中无冲突地替换 $y$ , 且 $(φ_{y}^{x})_{x}^{y} = φ$ .

证明. 只要无冲突替换成立, 由简单的字符串操作就不难证明最后的式子. 而由于

φ_{y}^{x}

里根本不出现

x

, 无冲突替换性由简单的归纳就能证出来.

$□$

引理 2.4.0.6 (约束变元替换引理). 如果有公式 $φ$ , 变元 $x$ 和项 $t$ , 则存在公式 $φ^{'}$ , 它和 $φ$ 只有某些约束变元不一样, 而且满足

(1) $φ ⊢ φ^{'}$ , $φ^{'} ⊢ φ$ ;

(2) $t$ 可以在 $φ^{'}$ 中无冲突地替换 $x$ .

证明. 固定 $t$ 和 $x$ , 我们递归地构造 $φ^{'}$ . 对未提到的情况, 我们构造的 $φ^{'}$ 都是完全不改变句子结构的, 原子公式甚至不改变句子.

对于 $φ$ 形如 $\forall y ϕ$ 的情况, 我们由归纳假设选一个 $ϕ^{'}$ 然后再选一个 $t$ 和 $x$ 和 $φ$ 和 $ϕ^{'}$ 中都没出现过的变元 $z$ , 定义 $φ^{'} = \forall z (ϕ^{'})_{z}^{y}$ .

现在只需要递归证明这个构造确实合理. 这里只录入最重要的量词情况的 (1) 的证明, 别的都很简单留给读者自己证明.

首先根据归纳假设, $ϕ ⊢ ϕ^{'}$ , 于是 $\forall y ϕ ⊢ \forall y ϕ^{'}$ , 又因为 $z$ 不出现, 而 $\forall y ϕ^{'} ⊢ (ϕ^{'})_{z}^{y}$ , 概括得到 $\forall y ϕ^{'} ⊢ \forall z (ϕ^{'})_{z}^{y}$ , 于是 $\forall y ϕ ⊢ \forall z (ϕ^{'})_{z}^{y}$ .

另一方面, 有归纳假设

ϕ^{'} ⊢ ϕ

. 显然有

\forall z (ϕ^{'})_{z}^{y} ⊢ ((ϕ^{'})_{z}^{y})_{y}^{z}

, 由

z

不出现可用循环替换得到

\forall z (ϕ^{'})_{z}^{y} ⊢ ϕ^{'}

, 进而

\forall z (ϕ^{'})_{z}^{y} ⊢ ϕ

, 最后由

y

不在左边自由出现可以概括为

\forall z (ϕ^{'})_{z}^{y} ⊢ \forall y ϕ

.

$□$

现在我们准备充分, 向完备性定理发起挑战.

定理 2.4.0.7 (Godel 完备性定理). 一阶逻辑是完备的.

证明. 只要证明一致则可满足. 假定有一个一致的公式集 $Γ$ , 我们自然的想像命题逻辑一样得到极大一致集, 然后构造一个结构, 最后得到一个赋值, 来满足这个公式集. 以下默认理论有等词, 因为没有等词的理论显然更简单.

Step1. 扩充得到极大一致集

为了能最后能得到结构, 我们必须给这个极大一致集附带一些额外的东西. 具体而言, 我们向原来的语言 $L$ 中加入可数多个新的常元符号 $c_{1}, c_{2}, ...$ , 从而它们不在 $L$ 的任何公式中出现. 我们记 $L_{C}$ 为扩充后的语言.

首先, $Γ$ 在 $L_{C}$ 中一致. 证明是用反证法, 若它变得不一致了, 那把推演序列里的新常元用常数概括引理改成变元, 就会得到 $Γ$ 在 $L$ 中不一致的证据, 矛盾.

接下来添加 Henkin 公理. 我们 (由可数性) 列举 $L_{C}$ 中全体 (公式, 变元) 的有序对为 $(ϕ_{1}, x_{1}), (ϕ_{2}, x_{2}), ...$ . 我们递归地令

1.	$θ_{1}$ 为 $\neg\forall x_{1} ϕ_{1} \to \neg (ϕ_{1})_{c_{i_{1}}}^{x_{1}}$ , 其中 $c_{i_{1}}$ 是第一个不在 $ϕ_{1}$ 中出现的新常元.
2.	$θ_{k + 1}$ 为 $\neg\forall x_{k + 1} ϕ_{k + 1} \to \neg (ϕ_{k + 1})_{c_{i_{k + 1}}}^{x_{k + 1}}$ , 其中 $c_{i_{k + 1}}$ 是第一个在 $ϕ_{1}, ..., ϕ_{k}, ϕ_{k + 1}, θ_{1}, ..., θ_{k}$ 中都没出现过的新常元符号.

我们记 $Θ = {θ_{1}, θ_{2}, ...}$ , 然后来验证 $Γ \cup Θ$ 一致.

反证. 如果不一致, 由证明序列的有限性一定可以找到一个最小的 $n$ 使得 $Γ \cup {θ_{1}, ..., θ_{n + 1}}$ 不一致. 由反证法元定理, 这指出 $Γ \cup {θ_{1}, ..., θ_{n}} ⊢ \neg θ_{n + 1}$ . 假定 $θ_{n + 1} = \neg\forall x ϕ \to \neg ϕ_{c}^{x}$ , 则 $Γ \cup {θ_{1}, ..., θ_{n}} ⊢ {\neg\forall x ϕ, ϕ_{c}^{x}}$ , 由定义 $c$ 不在左边出现, 于是常数概括得到 $Γ \cup {θ_{1}, ..., θ_{n}} ⊢ \forall x ϕ$ , 这与 $n$ 极小是矛盾的.

类似 Lindenbaum 定理, 我们通过枚举句子做 $L_{C}$ 中 $Γ \cup Θ$ 的极大一致扩张 $Δ$ , 并且从过程中得到它对语法蕴含封闭 (即 $Δ ⊢ ϕ$ 指出 $ϕ \in Δ$ ).

Step2. 构造无等词公式的解释

这个结构非常有趣, 因为这个结构就是我们语言里面的东西.

记 $L_{C}$ 上所有项的集合为 $M$ , 定义二元关系 $E^{M}$ 为 $(t_{1}, t_{2}) \in E^{M} \leftrightarrow (t_{1} \approx t_{2}) \in Δ$ , 对谓词 $P$ 定义 $(t_{1}, t_{2}, ..., t_{n}) \in P^{M} \leftrightarrow (P (t_{1}, t_{2}, ..., t_{n})) \in Δ$ , 对函数 $f$ 定义 $f^{M} (t_{1}, t_{2}, ..., t_{n}) = (f (t_{1}, t_{2}, ..., t_{n}))$ , 对常数 $c$ 定义 $c^{M} = c$ , 得到结构 $M$ . 最后定义初始赋值 $s$ 把变元 $x$ 变到它自己这个项 $x$ 上面, 并令其扩展, 得到结构 $M$ 上的赋值 $s$ .

注意, 这个 $E$ 也可以当成是我们给 $L_{C}$ 添加的一个新的二元谓词.

我们证明: 对任意公式 $φ$ , $(M, s) ⊨ φ^{'}$ 当且仅当 $φ \in Δ$ , 其中 $φ^{'}$ 是在 $φ$ 中把等词 $\approx$ 换成 $E$ 得到的公式.

(1) 通过对项归纳不难得知 $s (t) = t$ .

接下来对公式 $φ$ 实行归纳, 证明 $(M, s) ⊨ φ^{'}$ 当且仅当 $φ \in Δ$ . 我们还是只证明最复杂的量词情形, 把其他简单情形交由读者自行完成. 假设 $φ = \forall x ϕ$ .

(2) 从左向右; 由定义 $(ϕ, x)$ 有一条对应的 Henkin 公理 $θ = \neg\forall x ϕ \to \neg ϕ_{c}^{x}$ . 注意 $(\forall x ϕ)^{'} = \forall x ϕ^{'}$ , 我们有 $(M, s) ⊨ \forall x ϕ^{'}$ 蕴含 $(M, s_{c}^{x}) ⊨ ϕ^{'}$ 由替换引理蕴含 $(M, s) ⊨ ϕ_{c}^{' x}$ 蕴含 $(M, s) ⊨ (ϕ_{c}^{x})^{'}$ 由假设蕴含 $ϕ_{c}^{x} \in Δ$ 蕴含 $\neg ϕ_{c}^{x} \neq \in Δ$ 由封闭性和 Henkin 公理蕴含 $(\neg\forall x ϕ) \in Δ$ 蕴含 $\forall x ϕ \in Δ$ .

(3) 从右向左: 我们来证明逆否. 若 $(M, s) \neq ⊨ \forall x ϕ^{'}$ , 我们想证明 $\forall x ϕ^{'} \neq \in Δ$ . 条件中拆掉 $\forall$ 的定义已经给我们了一个反例项 $t$ , 满足 $(M, s_{t}^{x}) \neq ⊨ ϕ^{'}$ . 运用约束变元替代引理, 选择一个 $ψ$ , 它与 $ϕ$ 的差别只有约束变元, 而且 $t$ 在 $ψ$ 中可以无冲突地替代 $x$ . 做连续推导: $(M, s_{t}^{x}) \neq ⊨ ϕ^{'}$ 由语义等价推出 $(M, s_{t}^{x}) \neq ⊨ ψ^{'}$ 由替换引理推出 $(M, s) \neq ⊨ ψ_{t}^{x}^{'}$ 由归纳假设就得到 $ψ_{t}^{x}^{'} \neq \in Δ$ 推出 $\forall x ψ \neq \in Δ$ 推出 $\forall x ϕ \neq \in Δ$ .

Step3. 构造一般公式的解释

注意上面已经证明了无等词公式的完备性. 由于等词和元语言的等于不一样, 直接做会出事, 我们要考虑一个商结构. 首先, 读者不难验证, $E$ 是 $M$ 上的一个等价关系, 且和每个谓词和函数都是相容的 (即相等的东西判断/映射到同一个东西).

我们重新定义结构 $U$ 的论域为 $M / E$ , 谓词 $P$ 对应 $([t_{1}], [t_{2}], ..., [t_{n}]) \in P^{U} \leftrightarrow P (t_{1}, t_{2}, ..., t_{n}) \in Δ$ , 函数 $f$ 对应 $f^{U} ([t_{1}], [t_{2}], ..., [t_{n}]) = [f (t_{1}, t_{2}, ..., t_{n})]$ , 常元 $c$ 对应 $c^{U} = [c]$ . 定义初始赋值 $S (x) = [x]$ , 然后令其自然地延拓为赋值. 我们只要证明:

对任意公式 $φ$ , $(U, S) ⊨ φ$ 当且仅当 $φ \in Δ$ .

归纳验证是惯常的归纳, 注意我们可以引用

M

中已经证明的结论来简化过程.

$□$

评注. 注意, 以上讨论的是可数语言, 证明中未曾用到选择公理; 如果讨论的语言是任意的, 我们就需要选择公理来进行公式的枚举.

名字空间

视图

2.4. Godel 完备性定理