在以下内容中,我们陈述了定理的两种等价形式,并展示了它们的等价性。
稍后,我们将证明定理。这将按照以下步骤进行
- 将定理简化为句子(没有自由变量的公式)前束范式,即所有量词 ( 和 ) 位于开头。此外,我们将它简化为第一个量词是 的公式。这是可能的,因为对于每个句子,都存在一个等价的句子,其前束范式的第一个量词是 .
- 将定理简化为形式为 的句子。虽然我们不能简单地通过重新排列量词来做到这一点,但我们证明了证明这种形式的句子定理已经足够了。
- 最后,我们证明了这种形式的句子定理。
- 这将通过首先注意到这样的句子 要么是可证伪的,要么是在它成立的某个模型中存在;这个模型只是为构成 B 的子命题分配真值。这是由于命题逻辑的完备性,其中存在量词不起作用。
- 我们将这个结果扩展到更复杂和更长的句子,Dn(n=1,2...),它们从 B 建立起来,因此它们中的任何一个要么是可证伪的,因此 φ 也是可证伪的,要么它们都不是可证伪的,因此每个句子都在某个模型中成立。
- 我们最后利用 Dn 成立的模型(如果它们都不可证伪)来构建一个 φ 成立的模型。
定理 1. 在所有结构中都成立的公式都是可证的。
这是完备性定理的最基本形式。我们立即将其重新表述为更适合我们目的的形式
定理 2. 每个公式 φ 要么是可证伪的,要么是在某个结构中可满足的。
"φ 是可证伪的" 根据定义 意味着 "¬φ 是可证的"。
要查看等价性,首先要注意,如果定理 1成立,并且 φ 在任何结构中都不可满足,则 ¬φ 在所有结构中都成立,因此是可证的,因此 φ 是可证伪的,定理 2成立。另一方面,如果定理 2成立,并且 φ 在所有结构中都成立,则 ¬φ 在任何结构中都不可满足,因此是可证伪的;然后 ¬¬φ 是可证的,因此 φ 也是可证的,因此定理 1成立。
我们通过逐步限制需要证明 "φ 是可证伪的或可满足的" 的所有公式 φ 的类别来证明定理 2。在开始时,我们需要证明所有可能的公式 φ 在我们的语言中都是如此。但是,假设对于每个公式 φ,都存在某个从更受限制的公式类别C中提取的公式 ψ,使得 "ψ 是可证伪的或可满足的" → "φ 是可证伪的或可满足的"。那么,一旦这个断言(在上一句话中表达)被证明,就只需要证明 "φ 是可证伪的或可满足的" 对于属于类别C的 φ 即可。还要注意,如果 φ 与 ψ 可证地等价(即,(φ≡ψ) 是可证的),那么确实 "ψ 是可证伪的或可满足的" → "φ 是可证伪的或可满足的"(健全性定理需要证明这一点)。
存在标准技术可以将任意公式改写成一个不使用函数或常量符号的公式,但需要引入额外的量词;因此,我们将假设所有公式都不包含这些符号。在哥德尔的论文中,他使用了一个从一开始就没有函数或常量符号的一阶谓词演算版本。
接下来,我们考虑一个通用的公式 φ(不再使用函数或常量符号),并将前束范式定理应用于它,以找到一个范式的公式 ψ,使得 φ≡ψ(ψ 处于范式意味着,如果存在任何量词,则所有量词都位于 ψ 的开头)。现在,我们只需要证明定理 2对于处于范式的公式 φ 即可。
接下来,我们通过对所有自由变量进行存在量化来消除 φ 中的所有自由变量:如果,例如,x1...xn 是 φ 中的自由变量,我们形成 . 如果 ψ 在结构 M 中是可满足的,那么 φ 当然也是可满足的;如果 ψ 是可证伪的,那么 是可证的,那么 ¬φ 也是可证的,因此 φ 是可证伪的。我们可以看到,我们可以将 φ 限制为一个句子,即一个没有自由变量的公式。
最后,出于技术便利的原因,我们希望 φ 的前缀(即 φ 开头的一系列量词,处于范式)以一个全称量词开头,以一个存在量词结尾。为了在一个通用的 φ(受我们已经证明的限制)上实现这一点,我们使用 φ 中未使用的某个一元关系符号 F 和两个新的变量 y 和 z。如果 φ = (P)Φ,其中 (P) 代表 φ 的前缀,Φ 代表矩阵(φ 中剩余的无量词部分),我们形成 . 由于 显然是可证的,很容易看出 是可证的。
我们通用的公式 φ 现在是一个句子,处于范式,并且其前缀以一个全称量词开头,以一个存在量词结尾。我们将所有此类公式的类称为 R。我们需要证明的是 R 中的每个公式要么是可证伪的,要么是可满足的。给定我们的公式 φ,我们将同一种类的量词字符串一起分组到块中
我们定义 的度为 矩阵中全称量词块的数量,这些块由存在量词块隔开,如上所示。以下引理,它是 Gödel 从 Skolem 对Löwenheim-Skolem 定理的证明中改编而来,使我们能够大大降低需要证明定理的通用公式 的复杂度
引理。设 k>=1。如果 R 中每个度为 k 的公式要么是可证伪的,要么是可满足的,那么 R 中每个度为 k+1 的公式也是如此。
- 评论:取一个形式为 的 k+1 度公式 φ,其中 是 的剩余部分(因此它具有 **k-1** 度)。φ 表明,对于每个 x,都存在一个 y,使得 ...(某事)。如果有一个谓词 Q',使得对于每个 x,Q'(x,y) 为真当且仅当 y 是使(某事)为真的所需的一个,那就太好了。然后我们可以写一个与 φ 等价的 k 度公式,即 。这个公式确实与 φ 等价,因为它表明,对于每个 x,如果存在一个满足 Q'(x,y) 的 y,则(某事)成立,此外,我们知道确实存在这样的 y,因为对于每个 x',都存在一个满足 Q'(x',y') 的 y'。因此,φ 由此公式得出。同样很容易证明,如果该公式为假,则 φ 也为假。不幸的是,通常情况下,不存在这样的谓词 Q'。但是,这个想法可以被理解为以下引理证明的基础。
证明:令 φ 为一个 **k+1** 度公式;那么我们可以将其写为
其中 **(P)** 是 的前缀的剩余部分(因此它具有 **k-1** 度),而 是 的无量词矩阵。**x**、**y**、**u** 和 **v** 在这里表示变量的 *元组* 而不是单个变量;例如 实际上代表 ,其中 是几个不同的变量。
现在,令 **x'** 和 **y'** 为与 **x** 和 **y** 分别具有相同长度的先前未使用变量的元组,并令 **Q** 为先前未使用关系符号,其接受与 **x** 和 **y** 的长度之和相同的参数;我们考虑公式
显然, 是可证的。
现在,由于量词串 不包含来自 x 或 y 的变量,因此以下等价关系很容易用我们使用的任何形式化方法证明
由于这两个公式是等价的,如果我们将第一个公式替换为第二个公式,我们得到公式 Φ',使得 Φ≡Φ'
现在 Φ' 具有形式 ,其中 (S) 和 (S') 是某些量词串,ρ 和 ρ' 是无量词的,而且,此外,(S) 中的任何变量都不出现在 ρ' 中,(S') 中的任何变量都不出现在 ρ 中。在这种情况下,形式为 的任何公式,其中 (T) 是一个量词串,包含 (S) 和 (S') 中的所有量词,以任何方式交织在一起,但保持 (S) 和 (S') 中的相对顺序,都将等价于原始公式 Φ'(这是我们依赖的一阶谓词演算中的另一个基本结果)。也就是说,我们将 Ψ 如下构造
我们有 。
现在 是一个 **k** 次公式,因此根据假设,它要么是可证伪的,要么是可满足的。如果 在一个结构 **M** 中是可满足的,那么,考虑到 ,我们看到 也是可满足的。如果 是可证伪的,那么 也是可证伪的,它等价于 ;因此 是可证明的。现在我们可以在可证明的公式 中用其他依赖于相同变量的公式替换所有 Q 的出现。我们仍然会得到一个可证明的公式。(这是 一阶谓词演算 的另一个基本结果。根据对演算所采用的特定形式主义,它可以被看作是“函数替换”推理规则的简单应用,如哥德尔的论文中所述,或者可以通过考虑 的形式证明,在其中用具有相同自由变量的其他公式替换所有 Q 的出现,并注意到在替换后所有形式证明中的逻辑公理仍然是逻辑公理,并且所有推理规则仍然以相同的方式适用。)
在这个特定情况下,我们用公式 替换 中的 Q(x',y')。这里 (x,y|x',y') 表示我们不是写 ψ,而是写了一个不同的公式,其中 x 和 y 被替换为 x' 和 y'。注意 Q(x,y) 被简单地替换为 。
然后变成
并且该公式是可以证明的;因为否定符号下和符号后面的部分显然是可以证明的,而否定符号下和符号前面的部分显然是φ,只是将x和y替换为x'和y',我们看到是可以证明的,而φ是可证伪的。我们已经证明了φ要么是可满足的要么是可证伪的,这结束了对引理的证明。
请注意,我们不能从一开始就使用代替Q(x',y'),因为在这种情况下将不再是一个良构式公式。这就是为什么我们不能天真地使用出现在证明之前的注释中的论证。
如上文引理所示,我们只需要证明关于R中度数为1的公式φ的定理。φ不可能是度数为0,因为R中的公式没有自由变量并且不使用常数符号。因此,公式φ的一般形式为
现在我们定义一个关于元组的自然数的k排序,如下:应该成立,如果要么,要么,并且在字典序中先于。[这里表示元组的项之和。] 将此排序中的第n个元组表示为。
将公式 设置为 。然后将 设置为
引理:对于每个 n,。
证明:用数学归纳法证明 n;我们有 ,其中后面的等价关系成立是因为变量替换,因为元组的排序使得 。这里的每个合取项显然都来自 φ。
对于基本情况, 显然也是 φ 的推论。因此,引理 得证。
现在,如果对于某个n, 是可证伪的,那么 φ 也是可证伪的。另一方面,假设对于任何n, 都是不可证伪的。那么,对于每个n,都有一种方法可以将真值分配给不同的子命题 (按其在 中首次出现的顺序排列;这里“不同”是指不同的谓词,或不同的绑定变量)在 中,使得当每个命题以这种方式评估时, 为真。这是由基础命题逻辑 的完备性推出的。
现在我们将证明,存在这样一种对 的真值分配,使得所有 都是真的: 在每个 中以相同的顺序出现;我们将通过一种“多数投票”的方式归纳定义对它们的通用分配:由于有无限多种分配影响,要么有无限多种分配使 为真,要么有无限多种分配使它为假,而只有有限多种分配使它为真。在前一种情况下,我们选择 在一般情况下为真;在后一种情况下,我们选择它在一般情况下为假。然后,从无限多种使 被分配与一般分配中相同的真值的n 中,我们以相同的方式选择对 的通用分配。
这个一般赋值必须导致每个 和 都为真,因为如果其中一个 在一般赋值下为假,则对于所有n > k, 也将为假。但这与以下事实相矛盾:对于 中出现的有限的一般 赋值集合,存在无限多个n,其中使 为真的赋值与一般赋值相匹配。
现在,从这个使所有 为真的赋值出发,我们构建语言谓词的解释,使得 φ 为真。模型的宇宙将是自然数。每个 i 元谓词 应该对自然数 为真,当且仅当命题 在一般赋值中为真,或者它未被赋值(因为它从未出现在任何 中)。
在这个模型中,每个公式 ,根据构造为真。但这意味着 φ 本身在模型中为真,因为 遍历所有可能的自然数 k 元组。所以 φ 是可满足的,我们完成了。
我们可以将每个 Bi 写成 Φ(x1...xk,y1...ym),其中一些 x 可以称为“第一个参数”,一些 y 可以称为“最后一个参数”。
以 B1 为例。它的“最后一个参数”是 z2,z3...zm+1,对于这些变量中 k 个变量的每种可能组合,都存在某个 j 使得它们作为“第一个参数”出现在 Bj 中。因此,对于足够大的 n1,Dn1 具有这样的性质:B1 的“最后一个参数”以它们中每种可能的 k 个组合形式,作为“第一个参数”出现在 Dn 中的其他 Bj 中。对于每个 Bi,都存在一个具有相应性质的 Dni。
因此,在满足所有 Dn 的模型中,存在对应于 z1、z2... 的对象,并且这些对象的每个 k 个组合都以“第一个参数”的形式出现在某个 Bj 中,这意味着对于这些对象的每个 k 个 zp1...zpk,都存在 zq1...zqm 使得 Φ(zp1...zpk,zq1...zqm) 成立。通过取仅包含这些 z1、z2... 对象的子模型,我们得到一个满足 φ 的模型。
第一定理:对于任何一致的正式、可计算枚举的理论,该理论证明了基本的算术真理,可以构造一个在该理论中不可证明但为真的算术命题。也就是说,任何能够表达基本算术的有效生成的理论都不可能同时既一致又完备。
第二定理:对于任何包含基本算术真理以及关于形式可证性的某些真理的正式递归可枚举(即有效生成的)理论 T,T 包含其自身一致性的陈述当且仅当 T 不一致。
假设存在一台计算机,并且形式逻辑可以表示为计算机程序,那么从计算机科学的基本引理中很容易证明哥德尔不完备定理。
1. 奎因引理—任何计算机程序都可以包含一个子程序,该子程序会打印出整个程序的代码。这允许任何程序将自身写入字符串变量,或写入足够大的大整数。
- 证明:让打印子程序是一个标准的奎因,并包含包含所有其余代码的附加数据。
2. 停机问题引理:不存在一个计算机程序PREDICT(P),它接受程序P的代码,并预测P是否最终会停机。
- 证明:编写程序SPITE,它将自身打印到变量 R 中,然后计算PREDICT(R)。如果答案是R 会停机,那么 Spite 进入一个无限循环。如果答案是R 不会停机,那么SPITE 停机。由于 R 实际上是伪装的SPITE,所以无论PREDICT说什么,答案都是错误的。
不完备定理:假设一个公理系统描述了整数(或任何其他离散结构),并且它具有足够的操作(加法和乘法就足够了)来描述计算机的工作。那么该系统要么不一致,要么不完备。
- 证明:编写DEDUCE 来推导出公理系统的全部结果。让DEDUCE 将其自身的代码打印到变量 R 中,并在系统内部的计算机嵌入中搜索定理R 永远不会停机。只有当DEDUCE 找到这个定理时,它才会停机。
- 如果公理系统证明了DEDUCE 不会停机,那么它是不一致的。如果该系统是一致的,那么DEDUCE 不会停机,并且公理无法证明它。
- 这个论证并没有明确地证明不完备性,因为一个一致的公理系统仍然可以证明-不一致定理,即DEDUCE 会停机(即使它没有停机),而且没有矛盾。
- 所以编写ROSSER:ROSSER 将其代码打印到 R 中,并在推论中搜索 1. R 打印了一些内容或 2. R 从未打印过任何内容。如果它找到了 1,那么它会在不打印任何内容的情况下停机。如果它找到了 2,那么它会向屏幕打印 "Hello World!" 并停机。
- 如果公理系统是一致的,那么它既不能证明ROSSER 最终会打印一些内容,也不能证明其否定ROSSER 不会打印任何内容。所以,无论它关于DEDUCE 的结论是什么,公理系统都是不完备的。
为了证明第二个不完备定理,请注意,公理的一致性证明了DEDUCE 不会停机,所以公理系统不能证明其自身的一致性。