本文使用 Zhihu On VSCode 创作并发布

各位朋友七夕快乐！

上一篇文章Gödel完备性定理 —— 一阶谓词逻辑演绎系统 Part I中笔者介绍了一阶谓词逻辑的语言和演绎系统，并粗略讨论了Gödel完备性定理的一些意义。这篇文章我们将完整证明完备性定理。并在文末简要讨论Löwenheim–Skolem定理及其衍生出的Skolem悖论。

重述Gödel完备性定理如下：

设

换而言之，一切一阶逻辑的真命题都是可证明的。

可证明性是依赖于演绎系统的。我们采用上篇文章引入的演绎系统

和2种演绎规则：

我们先在一个限定的情况下证明这个定理：

• 不含等号
  （这时我们只有公理A1~A5）；
• ，
  。即只考虑前提和结论都不含自由变量的情况。

在证明弱化的完备性定理后，我们会讨论如何推广这两种情况。

一致性，极大一致性，可满足性

在命题逻辑完备性证明（命题逻辑演绎系统的可靠性与完备性）中使用过这些概念。复述定义如下：

• 一致的，若不存在
  使得
  和
  同时成立。
• 极大一致的，若它是一致的，且对任意
  ，都有
  或
  。
• 可满足的，若存在模型
  使得
  对每个
  都成立。
  可满足与
  存在一个模型同义，笔者会自由替换使用这两个说法。

和命题逻辑一样，我们的核心是证明：[定理0] 一致的

。

如果假设这个结论，完备性定理可以自然由它推出。（过程见命题逻辑演绎系统的可靠性与完备性末尾）

见证集

Henkin在1949年对Gödel完备性定理的证明中，引入了一个所谓见证性(witnessing)的概念：

见证的，若：对于所有只含有

我们把定理0的证明拆成两大模块：

• [定理1] 极大一致并具有见证性的
  是可满足的

  。

• [定理2] 若所有极大一致并具有见证性的
  是可满足的，则所有一致的
  是可满足的

  。

项模型，定理1的证明

在这个小节我们始终假设

Henkin创造性地引入项模型(term model)的概念：

考虑

• 论域
  ;
• 谓词指派：对于谓词符号
  ,
  成立当且仅当
  ;
• 函数指派：对于函数符号
  ，
  ;
• 常数指派：对于常数符号
  ,
  。

我们要证明这个构造出来的项模型确实是满足

设

[引理1.1] 对每个项

对

的长度用归纳法。

假设结论对长度小于

的项成立。考虑长度为

的项

。

• 若
  ，则
  。
• 若
  ，则
  。
• 若
  ，则
  。由归纳假设，
  。

[引理1.2] 对每个公式

对

的长度用归纳法。

假设结论对长度小于

的项成立。考虑长度为

的项

。

• 设
  是原子公式，则
  ，其中
  。有

• 设
  ，其中
  。有

• 设
  ，其中
  。有

• 设
  ，其中
  。这是唯一不显然的情况。

先证

方向：假设

且

。设

是将

中所有

替换为

得到的公式。于是

。由

的极大一致性，有

。由下面的引理1.2.1和肯定前件，得到

。由

的见证性，存在

使得

。定义

以及赋值

。于是

。由归纳假设，有

，即

。注意到

和

是

-等价的，而

不是

的自由变量，于是有

。这与

矛盾。

方向：假设

且

。则存在与

-等价的

使得

。定义

由归纳假设，有

。令

的定义同前，则有

和

。因为

，由A4和MP得

。但是前面已经证了

，这与

的一致性矛盾。

[引理1.2.1]

[定理1'] 设

对任意

，因为

是句子，

对所有

成立。由引理1.2，

对所有赋值

成立。于是

。于是

。

定理2的证明

在这个小节我们始终假设

对于一切

。

[引理2.1] 设

设

是

的证明。令

是出现在这个证明中的前提的集合。于是

同时也是

的证明，并且

是有限集。

设

是一个未出现在

中的变量。我们将归纳证明

对

成立。假设对

有

。

• 若
  是公理A1, A2, A3中的一个，则显然
  也是对应的公理。于是
  。
• 若
  是公理A4，
  。在
  中
  关于
  是自由的，由于
  不出现在
  或
  中，在
  中
  关于
  仍是自由的。有
  ，这仍是公理A4。于是
  。
• 若
  是公理A5，
  ，由于
  不出现在
  或
  中，且
  ，有
  。这仍是公理A5。于是
  。
• 若
  , 那么由假设
  未出现在
  中。于是
  。
• 若
  由
  和
  (
  )通过肯定前件得到。则
  由
  和
  通过肯定前件得到。由归纳假设有
  。
• 若
  由
  (
  )通过全称普遍化得到。则
  由
  通过全称普遍化得到。由归纳假设有
  。 这样就归纳完毕。我们证明了
  . 接下来有

[引理2.2] 设

假设

不一致的。存在

且不含常量

，使得

且

。 接下来有

这与

的一致性矛盾。

[引理2.2.1] 若

见Gödel完备性定理 —— 一阶谓词逻辑演绎系统 Part I

[引理2.3] 设

证明与命题逻辑完全相同，见命题逻辑演绎系统的可靠性与完备性。

在开始证明定理2之前，为了应用引理2.2我们需要另一个可数的常数符号集。这里的做法是重新标号：对

[引理2.4]

显然。

[定理2'] 存在

（在命题逻辑中我们用了Zorn引理证明一致集包含在极大一致集当中，这对于更熟悉代数的笔者来说是自然的，但实际上是overkill。由于我们选取的符号集是可数的，不需要Zorn引理，简单的归纳就能证明。这里同理。同时我们也建立Gödel完备性定理弱于Zorn引理这一声明。） 、

根据引理2.4对

中的句子的常量重新标号，使得每个奇数编号

都不在

中出现。

注意到由于

的符号集是可数的，有

。因此

也是可数的。设

是其的一个枚举。我们归纳地定义

(

) 如下：

• ；
• 假设
  (
  ) 已经被定义，我们定义：

由引理2.3，若

一致，则

也一致。

• 假设
  (
  ) 已经被定义，我们定义
  如下：
  • 若
    ，根据我们的构造存在常量
    未在
    中出现。定义
    。这时有
    。由引理2.2，若
    一致，则
    也一致。
  • 对于其他情况（
    或
    ），定义
    。

这样我们构造的每个

(

)都是一致的。令

。显然根据上面的构造

是具有见证性的，我们要证明它是极大一致的：

假设

不一致，则存在

使得

且

。这两个证明都只有有限长度，因此存在有限子集

使得

且

。这说明

是不一致的。但是存在

使得

，这与

的一致性矛盾。因此

是一致的。

的极大性是显然的：对

，要么

要么

。因此要么

要么

。

对于

引理1.2是不成立的。考虑

对于这个问题的修补，解决办法是将等号视作一种等价关系。我们考虑项模型的商模型。为此，我们需要先证明等号构成等价关系。

在下面的引理3.1~3.3中，设

[引理3.1] 自反性：

设

未出现在

中。

[引理3.2] 对称性：

设

未出现在

中。先证

：

由演绎定理，有

。然后证

。

[引理3.3] 传递性：

设

未出现在

中。先证

。

应用两次演绎定理，得

。然后证

。

由前面三个引理，我们可以在

显然与闭项等价的项仍是闭项。考虑商集

考虑项模型的商模型

• 论域
• 谓词指派：对于谓词符号
  ,
  成立当且仅当
  ;
• 函数指派：对于函数符号
  ，
  ;
• 常数指派：对于常数符号
  ,
  。

读者可以自行使用公理A7验证这个商模型是良定义的。

剩下的证明与原证明一致。我们于是证明了Gödel完备性定理对包含等号的一阶逻辑语言

从句子到公式的推广

我们证明了：

[Gödel完备性定理，弱形式] 设

我们希望把这个结论推广到

我们需要处理前提和结论中的自由变量。思路是把每个出现的自由变量用常量替换。为此我们依然需要对常量符号集做重新标号。

对

设

设

对这个式子中每个自由变量

应用

紧致性定理

[紧致性定理]

在有了定理0后，「可满足性」与「一致性」就完全等价了。紧致性定理建立了「有限可满足性」与「可满足性」的等价，它是从完备性定理立刻得到的推论。它的核心是任意一个证明的长度总是有限的。

注意到尽管紧致性定理依赖于完备性定理，但是紧致性定理的表述实际上不依赖于演绎系统的选取。

一个方向是显然的。另一方向，假设

的任意有限子集都有模型但是

没有模型。那么

是不一致的，存在

使得

且

。然而这两个证明的长度都是有限的，因此存在有限子集

使得

且

。于是

是不一致的。即

没有模型，矛盾。

Löwenheim–Skolem定理，Skolem悖论

[向下Löwenheim–Skolem定理] 若

至多可数的模型。

在完备性定理的证明中，我们证明了存在极大一致且具有见证性的

使得

。

满足项模型的商模型

。显然它的论域

是至多可数的。

向下Löwenheim–Skolem定理发表后，Skolem提出了所谓的Skolem悖论：总所周知我们常用的ZF集合论是一个一阶逻辑的理论。它的公理有：

• 外延公理：
• 配对公理：引入一个二元函数符号
  ，称为两个元素的配对集，满足
• 并集公理：引入一个一元函数符号
  ，称为集合的并集，满足
• 幂集公理：
• 分离公理模式：设
  ，且
  。有
• 空集公理：引入一个常量符号
  ，称为空集，满足
• 无穷公理：
• 正规公理：
• 替代公理模式：设
  ，且
  。有
  ，其中
  是
  的缩写。

根据向下Löwenheim–Skolem定理，ZF集合论存在一个可数模型，也就是一个 「可数ZF集合论」，其中全体集合是可数的！而大家在数学分析中熟知的Cantor定理，声称

如果全体集合是可数的，怎么可能存在不可数集呢？

笔者不是逻辑学专业的学生，对这个问题的理解比较粗浅。笔者认为这是因为我们定义「可数集」的方式不同。从原始定义来说，我们称集合