本文使用 Zhihu On VSCode 创作并发布
笔者计划分为两篇文章。这一篇介绍笔者对Gödel完备性定理的理解以及这个定理的若干应用。下一篇文章完整地证明Gödel完备性定理。
Part II在这里：Gödel完备性定理 —— 一阶谓词逻辑演绎系统 Part II
一阶谓词逻辑语言
和命题逻辑语言相比，谓词逻辑语言有更精细的结构。我们能讨论变量，谓词与函数。具体来说，我们的语言
![]() (FOPC stands for First-Order Predicate Calculus)具有如下符号：
变量符号：
![]()
函数符号：
![]() (右上角的数字
![]() 表示
![]() 元函数，这是一种纯粹为了省事的写法，下同)
谓词符号：
![]()
常数符号：
![]()
逻辑连接符：
![]()
括号
![]() 和逗号
![]()
量词：
![]()
等号：
![]() (为了和元语言(metalanguage)的等号
![]() 作区分，这里谓词逻辑的等号上面加一个点)
注意等号本质上也是一个特殊的谓词，这里把它单列出来是为了讨论方便。
注意这里一阶(first-order)限制了我们只能对变量使用量词，也就是数学上「对于所有的
![]() ，有......」这样的语句是不能写成一阶逻辑的语言的，因为这里对谓词使用了全称量词。特别地，
标准的自然数模型的定义是二阶的，因为数学归纳法是一个二阶性质(second-order property)。
关于
![]() 的唯一可读性定理，证明可以参见一阶谓词逻辑的唯一可读性定理。这里还有一个需要注意的概念是
自由变量(free variable)和
约束变量(bound variable)。通俗地说，约束变量就是没有被
量化(quantified)的变量，也就是没有放在某个量词里的变量；而自由变量则反之。一个
![]() 的公式如果不含任何自由变量，则称为一个
句子(sentence)。
在命题逻辑中，我们通过给每个命题符号赋值(assignment)，使命题逻辑语言的句子具有真值。一阶谓词逻辑更复杂一些：我们需要首先考虑一个模型(model)
![]() 。
![]() 包括
论域(domain)
![]() ，
对每个函数符号
![]() 指派一个函数
![]()
对每个谓词符号
![]() 指派一个函数
![]()
对每个常数符号
![]() 赋值
![]() 。
而一阶谓词逻辑中的赋值(assignment)，则是对每个变量符号
![]() 赋值
![]() 。
考虑一个公式
![]() ，如果存在一个模型
![]() 和赋值
![]() 使得
![]() 的真值为
![]() ，则记作
![]() 。如果
![]() 是一个句子，则显然它的真值与赋值
![]() 无关。此时简单记作
![]() 。这里
![]() 称为满足
![]() 的一个模型。如果
![]() 对每个模型都为真，则记作
![]() 。
举个栗子，考虑一个一阶语言
![]() ，其中
![]() 是一个二元函数符号，
![]() 是一个常数符号。考虑一组公式：
![]()
我们知道，任何满足
![]() 的模型
![]() 称为一个
群(Group)，这里的二元函数
![]() 一般记作乘法。
在引入演绎系统前，我们还需要一个介绍一个换元法则。我们需要如下拗口的定义：设
![]() 是一个项(term)，
![]() 是一个变量符号，
![]() 是一个公式(formula)。称
在
![]() 中
![]() 关于
![]() 是自由的
，如果在
![]() 中每个自由出现的
![]() 都没有被一个在
![]() 中的变量所量化。这时，我们可以把
![]() 中所有自由出现的
![]() 替换为
![]() ，记作
![]() 。
（通俗地说，一个项是不含有任何谓词符号，等号和量词的公式；严格的定义请参考一阶谓词逻辑的唯一可读性定理）
让笔者尝试解释这个定义的必要性。考虑
![]() 和
![]() 。这里
![]() 在
![]() 中是自由的，但是
![]() 在
![]() 中被
![]() 所量化，而
![]() 也同时出现在
![]() 中。如果强行换元，那
![]() 就变成了
![]() ，这显然和原来的
![]() 能表示的语义完全不一样。但是如果考虑
![]() ，这里就能做换元
![]() ，因为
![]() 在
![]() 中没有出现。
![]() 是合法的。
现在请读者尝试验证如下规则：
设
![]() 是公式，在
![]() 中
![]() 关于
![]() 是自由的，有
![]() 。
演绎系统
![]()
我们在之前的文章中介绍过命题逻辑的演绎系统
![]() 。它在一阶谓词逻辑中扩展成演绎系统
![]() （这个名字似乎在笔者用的讲义之外非常不常见...）它有7种公理：
![]()
和2种演绎规则：
![]()
上面的
![]() 是任意公式，
![]() 是任意项，
![]() 是任意变量符号。
这个演绎系统的A1, A2, A3和MP是我们在命题逻辑中所熟知的，而A4, A5, A6, A7和
![]() 是新引入的。
如果从前提
![]() 出发可以证明
![]() ，则记作
![]() 。
演绎系统
![]() 的证明
和命题逻辑的演绎系统
![]() 一样，一个
![]() 的证明是指一串公式
![]() ，其中每个
![]() 要么属于
![]() ，要么是7种公理之一，要么是通过MP由某个
![]() 和
![]() (
![]() )得到，要么通过
![]() 由某个
![]() (
![]() )得到。并且
![]() 。
和
![]() 类似，
![]() 中也有
演绎定理(Deduction Theorem)：
设
![]() ，
![]() 。若
![]() ，则
![]() 。
它的证明和命题逻辑几乎一模一样（命题逻辑演绎系统的可靠性与完备性），只是在归纳的时候多了一个情况，即全称普遍化，该情况需要用到公理A5。读者可以自行补全细节。
我们在命题逻辑演绎系统的可靠性与完备性中证明了
![]() 的完备性。也就是对于任意命题逻辑的重言式(tautology)，总是存在一个从A1, A2, A3和MP出发的证明。因此，在谓词逻辑的证明中，事实上任何命题逻辑的重言式都能直接使用而无需单独证明。
在一些数理逻辑的教科书中，谓词逻辑的公理系统将全体命题逻辑的重言式作为公理使用。这样做的优势是trivialize命题逻辑的完备性定理。当然，一些数学家希望从尽可能少的公理模式出发得到全部重言式。因此就有了此文中采用的公理系统。
我们举一个栗子来看
![]() 的证明。
设
![]() 且
![]() ，求证
![]()
由演绎定理，只要证
![]() .
![]()
四个核心定理
设
![]() ，
![]() 。
可靠性定理(Soundness Theorem)： 若
![]() ，则
![]() 。
Gödel完备性定理(Gödel's Completeness Theorem)：若
![]() ，则
![]() 。
紧致性定理(Compactness Theorem)：
![]() 有模型当且仅当
![]() 的任意有限子集都有模型。
Löwenheim–Skolem定理：若
![]() 是一致的，则它有一个论域至多可数的模型。
完备性定理的意义
声明：本段属于笔者的学习感想，对其中一些名词或者论述的专业性不作保证，如有纰漏恳请指教。
在命题逻辑中，我们可能会感觉到一个演绎系统的存在是不必要的。比如一个公式
![]() ，如果我们想验证它是「对的」，只需要列出
![]() 和
![]() 的真值表，逐一验证公式的真值即可。何必从3条公理出发费尽心思构造一个「证明」？我们说命题逻辑语言中的公式是
有限可验证的(finitely verifiable)。
然而在一阶谓词逻辑中，即使一个简单的句子
![]() ，我们也不能通过枚举一切的模型来验证它的真值。因此一个演绎系统的存在似乎是必要的。也就是我们利用有限多的公理和前提尝试写出一个有限长的证明。如果我们能证明Gödel完备性定理，那么任意永真的句子都存在一个有限长度的证明。也就是理论上我们能通过暴力枚举所有可能的证明的方式，在有限时间内找到这个证明。（然而如果这个句子不是永真的，则不能在有限时间内枚举找到证伪。）
Gödel完备性定理还有两个很强的推论：紧致性定理和Löwenheim–Skolem定理。紧致性定理是证明一个数学命题不属于一阶逻辑的有力工具。比如
![]() 和
![]() 的Archimede性质就不是一阶逻辑的命题；自然数的数学归纳法也不是一阶逻辑的命题。Löwenheim–Skolem定理则保证了非标准模型的存在：ZFC集合论基于一阶逻辑语言，存在无限种模型满足无限公理声称的归纳集。这其中除了标准模型的自然数，还有诸如(在标准ZFC意义下)不可数的非标准模型的「自然数」等等。
关于紧致性定理有个著名的栗子。我们熟悉的任何域都有代数闭包的证明是由Artin给出的，这个证明基于Zorn引理；事实上任何域都有代数闭包只需要用到一阶逻辑的紧致性定理，而紧致性定理事实上是弱于选择公理的。可以参考：Is the statement that every field has an algebraic closure known to be equivalent to the ultrafilter lemma?
Gödel完备性定理是一阶逻辑的强大之处。然而对于更复杂的系统，完备性就失去了。我们有著名的Gödel第一不完备定理：通俗地说，一个蕴含Peano算数（即自然数）的有效公理化的一致的形式系统中，一定存在既不能被证明也不能被证伪的命题。
|