哥德尔不完全性定理证明的三种途径
哥德尔的两个不完全性定理被称为二十世纪数理逻辑领域最重要也最深刻的定理，在它刚被提出时，被许多人看作是难懂并且不可思议的。经过近一个世纪的发展，哥德尔不完全性定理的证明已经变得好懂了许多。正如哥德尔本人所言，定理的证明没有太多数学上难的部分，实际上涉及的是一种视角转换，一种新的看待问题的眼光。和所有伟大的定理一样，如今不完全性定理已经有了许多不同方法的证明，每个方法都从不同领域的视角解读这一定理，这也使得定理的内容愈加丰富。时至今日，不完备定理的证明已经成为了进一步研究数理逻辑哥分支的基础。
（为行文紧凑起见，假定读者熟悉一阶逻辑的句法，语义和演绎系统）
一. 预备工作
1. 证明核心的通俗解释
哥德尔不完全性定理断言，对于满足若干特定条件的形式系统（称之为哥德尔系统）S，如果S是一致的，那么存在一个闭语句，在S中既不能证明该闭语句也不能证明该闭语句的否定。那么我们可以如此描述这个特殊语句G的含义：
G： 本语句是不可证的。
如此一来，如果（1）G是假的，那么G可以被证明。但是形式系统S证明出了一个假命题，根据古典逻辑的爆炸律，任何命题都可以被证明，因此S是不一致的，与假设矛盾。所以只可能是（2）G是真的，因此G不可证明。同时，¬G是假的，因此也不可证明。这个特殊语句G就是我们要找的语句。
但是，不完全性定理对于形式系统的限制很少，只需要系统包含初等数论，不完全性定理即可适用。显然，一个只能谈论自然数及自然数上的序关系，加法乘法运算的形式系统中，是不可能有一个语句包含“本语句”这样的自指项，以及“不可证的”这样复杂的关于系统的元性质的谓词的。
不过这种不可能只是表面上的。一个形式系统中的合式公式，公理（模式）等对象，无非就是一些遵从特定语法规则的有穷符号串，所谓系统中的证明，也无非是从公理到被证明语句的若干（有穷）符号串序列。因此，如果我们能够找到一种将符号串映射成自然数的方法，那么谈论自然数以及自然数上的关系和运算，也就是在谈论形式系统中的公式以及公式之间的演绎关系，这就使得一个仅仅谈论自然数的系统中的语句，“实质上”也在谈论关于系统本身的元性质，这样的映射方法称之为哥德尔编码。
2. 哥德尔编码
一个很好想到的编码方案是这样的：对于系统S中的非逻辑符号（如果系统只包含初等数论，那么非逻辑符号是有穷的）指派从1到n的自然数，对于S中的变元（可数无穷个）指派n+1开始的自然数，然后利用算术基本定理，即自然数分解为素因子乘积的方式是唯一的，来对一个符号串指定它的哥德尔数。以∀x(x=x)为例，假设∀的哥德尔数是1，“（”是6，“）”是7，=是10，x是11，那么公式∀x(x=x)的哥德尔编码就是2^1×3^11×5^6×7^11×11^10×13^11×17^7，符号串σ的哥德尔数记为#(σ)。
可以看出，上面的编码方案中，最重要的是使用乘法进行编码，而这一要求也是必要的。如果在自然数理论中可以定义乘法（当然，这首先需要定义后继和加法），那么就可以进行哥德尔编码，并且不完全性定理就可以适用于这个理论。导致不完全性的并不是非常特殊的数学归纳法（数学归纳法本质上是一条二阶性质，在一阶理论中，可以用归纳公理模式进行替换，这意味着包含数学归纳法的理论的公理数目不能是有穷的），事实上，不包含数学归纳法但定义了乘法的罗宾逊算术Q是不完全的，而没有定义乘法却包含数学归纳法的普莱斯伯格算术PrA是完全的。
仅仅找到一个编码方案并不是结束，我们的目的是，可以在一个初等数论理论中谈论自身的结构，这就意味着，对于一个特定的符号串σ的哥德尔数#(σ)，理论可以知道它是不是对应一个变元/项/公式等语法结构。对于我们，当然可以把这个哥德尔数因数分解之后再翻译成符号进行检查，但是对于一个只能谈论自然数的初等数论理论，是不存在所谓“翻译”的概念的。理论只能处理形如“某个自然数是否属于一个自然数集”的问题，并且这个自然数集不能太过复杂，否则就无法仅仅通过后继，加法，乘法这些简单函数来描述。
什么样的集合和函数是上述意义上“简单”的？这个问题引出了哥德尔对于原始递归函数和一般递归函数的研究，这方面的理论已经成为递归论和计算理论方面的基础。简单来说，哥德尔规定了一系列自然数上容易计算的函数，称之为递归函数，一个自然数集合是（原始）递归的，当且仅当这个集合的特征函数是（原始）递归函数。进一步哥德尔证明了，这些递归函数都可以在一个定义了后继，加法，乘法的初等数论理论（比如罗宾逊算术Q或更一般的皮亚诺算术PA）中定义。
接下来需要证明，理论中变元，项，自然数，原子公式，合式公式，闭语句，公理等符号串所对应的哥德尔数集合都是（原始）递归的，并且公式σ通过带入，量化等句法操作生成新公式σ’所对应的将#(σ)映射为#(σ’)的函数也是（原始）递归函数。这一部分证明是整个不完全性定理证明的工作量最大也是最繁琐的地方，具体的处理可以参考冯琦《数理逻辑导引》第十三章。处理完这些部分，就可以证明，关于初等数论理论句法结构的若干元性质都可以在理论之中表达，接下来还需处理两个关键的性质。
3. 可证谓词与不动点引理
在本节第一部分中，为了构造特殊语句G，我们需要在初等数论理论中定义“不可证明”这个谓词。这就意味着需要有一个可定义的自然数集或者自然数上的关系可以描述“可证”的概念。
在一个希尔伯特式演绎系统中，一个从前提公式集Γ到公式φ的证明可以被看做是一个有穷的公式序列，这个序列中的每个公式要么是公理，要么是Γ中的前提，要么是由在这个序列中前面的公式通过概括规则和分离规则得到的，并且序列的最后一个公式正是待证明的公式φ。哥德尔构造了一些递归函数，可以将有穷个公式的哥德尔数能行地映射为一个特定的自然数，并且可以借助同样递归的β函数将一个证明序列中的第i个公式取出。
这样一来，不仅项和公式，而且证明也可以进行哥德尔编码。于是，问某个证明序列s是否是公式α的证明，就是在问#(s)和#(α)是否属于一个N×N上的二元关系，这个关系容易表示（只需查看证明序列的最后是不是所求公式α），并且是递归的，将其记为Bew(x,y)，非形式地看，Bew(x,y)是在说y是x的证明。公式∃y(Bew(x,y))意为存在一个y，y是x的证明，因而代表着x有一个证明，即x是可证的，简记为Bwb(x)。
一个恰当的形式系统需要满足两个基本的要求。（1）公理集是递归的，也就是说，可以在有穷步之内判定一个闭语句是不是形式系统的公理。（2）一个公式序列是否是某个公式α的证明，也可以在有穷步之内判定。满足上述条件的形式系统中可证明的公式的哥德尔数集合是递归可枚举的。
注意到既然所有的证明序列都可以编码成一个自然数，这意味着所有证明序列的集合是可数的。因此，如果想知道一个公式σ是否是可证的，只需逐个判断Bew(#(σ)，1)，Bew(#(σ)，2)……以此类推，如果σ是可证的，那在第n步总会有证明序列n证明σ。这意味着谓词Bwb，即“可证的”是一个递归可枚举谓词，可证明的公式对应的哥德尔数是自然数中的一个递归可枚举集合。
另一方面，初等数论理论还包含了一个重要的性质，这个性质允许理论中的公式进行自指:
哥德尔不动点引理：对任意的一元公式β(x)，存在一个闭语句σ，使得如下语句在系统中是可证的： σ ↔ β(S#(σ))
这里S#(σ)不是自然数，而是自然数对应的项的符号串。如果#(σ)=n，那么S#(σ)就是SSS……S0 （共n个S）
直观上，σ说的是“β对我（的哥德尔数）成立”，这就完成了自指。需要指出的是，哥德尔不动点引理的证明是构造性的，也就是说，给定公式β，可以能行地找到它的不动点σ，而不只是证明σ的存在。
有了这两个性质，就可以进行不完全性定理的证明。
二．证明的三种途径
1. 塔尔斯基途径（模型论方法）：
这个证明依赖于语句的真值，是本文开头部分通俗说明中“本语句是不可证明的”的具体实现，相对而言最好理解，也最直观清楚。同时，通过真值解释，可以得出不完全性定理的哲学意义：存在不可证的数学真命题。正是通过真值解释，哥德尔推出了他的数学哲学立场——数学柏拉图主义。
根据之前的讨论，包含初等数论的形式系统具有以下两个特性：
T1：具有不动点性质
T2：具有谓词“可证明的”（Bwb）
现在我们规定：
T3：对系统中任意一个闭语句p，或者p是真的，或者¬p是真的（经典逻辑二值假定）
只需要性质T1和T3，即可证明著名的塔尔斯基不可定义定理。
我们规定初等数论理论T中的闭语句的真值在标准自然数模型N上根据一阶逻辑的塔尔斯基语义定义，那么理论T中在N上为真的闭语句集合记为Th(N)。相应的，Th(N)中闭语句对应的哥德尔数的集合记为#Th(N)，那么可以证明：
塔尔斯基不可定义定理：#Th(N)在结构N上不可定义。
证明：如果存在一个可定义一元谓词β，对每个闭语句θ，如果θ在N上为真，那么β(S#(θ))也在N上为真，β就是理论T在N上的真谓词，同时也就定义了#Th(N)。
但如果考虑公式¬β，根据不动点引理，存在一个闭语句σ，使得σ ↔ ¬β(S#(σ))。这意味着，如果σ在N上为真，那么β(S#(σ))反而为假，因此不存在可定义的真谓词。
证毕
由此我们可以证明哥德尔第一不完备定理:
塔尔斯基证明:如果一个形式系统既是一致的又是完全的，那么所有可证的闭语句都是真的，所有真的闭语句都是可证的，因此“真的”和“可证的”是一回事，根据T2，包含初等数论的形式系统中可以定义谓词“可证明的”，那么也就定义了谓词“真的”，而这是矛盾的。
证毕
2. 哥德尔-罗瑟途径（证明论方法）：
哥德尔不完全性定理内容的表述中并不包含真值，因此可以给出一个只涉及到句法和演绎证明过程，不涉及语义部分的证明。在哥德尔的原始证明中，使用了一个比一致性更强的条件，Ω-一致性，这隐含地引入了语义的成分，而罗瑟的改进使得条件可以放宽至一致性。这个纯粹证明论的证明使得不完备定理的成立依赖非常弱的元数学假定，事实上，哥德尔不完全性定理的证明可以在有穷主义算术PRA中形式化，因此即使严苛如直觉主义者也承认不完全性定理的有效。
一个形式系统是Ω-不一致的，当且仅当系统可以证明一个闭语句∃x(P(x))，但同时对于所有的n属于N，系统都可以证明¬P(n)。这意味着，可以证明存在一个自然数具有某性质，但是对于任何具体的自然数n，都能证明n不具有该性质。形式系统是Ω-一致的当且仅当它不是Ω-不一致的。Ω-一致性蕴含一致性。
哥德尔的原始证明既然不涉及真值，那么上面的性质T3就不成立了，与之相对，哥德尔的证明需要如下三个条件：
G1：具有不动点性质
G2：具有谓词“可证明的”（Bwb）
G3：对于任意的σ和s，要么可以证明Bew(S#(σ),S#(s))，要么可以证明¬Bew(S#(σ),S#(s)) （如前文所说，n是m的证明存在一个机械的判断方法，所以这一性质是满足的）
哥德尔的证明：考虑公式¬Bwb(x)，对其应用不动点引理，有σ ↔ ¬Bwb(S#(σ))。
如果σ是可证的，那么存在一个证明序列s，使得Bew(S#(σ),S#(s))是可证的，那么Bwb(S#(σ))是可证的，但是根据不动点引理，σ可证可以推出¬Bwb(S#(σ))是可证的，这与系统的一致性矛盾，因此σ不可证。
σ不可证，因此对任意的证明序列s，¬Bew(S#(σ),S#(s))是可证的。根据Ω-一致性，∃y（Bew(S#(σ),y)是不可证明的，也就是Bwb(S#(σ))是不可证明的。对σ ↔ ¬Bwb(S#(σ))两侧加否定，有¬σ ↔ Bwb(S#(σ))，因此Bwb(S#(σ))不可证推出¬σ不可证。
综上，存在σ使得σ和¬σ都不可证。
证毕
为了避免使用Ω-一致性这样过强的条件，罗瑟定义了一个新谓词Prov(x)：
Prov(x) df= ∃y(Bew(x,y)∧∀z<y(¬Bew(¬x,z)))
直观上看，Prov(x)说的是，哥德尔数为x的闭语句σ存在一个哥德尔数为y的证明，并且所有哥德尔数比y小的证明z都不能证明¬σ。
对于谓词Prov，有以下两条性质：
R1：如果闭语句α可证，则Prov(S#(α))也可证
R2：如果闭语句¬α可证，则¬Prov(S#(α))也可证
这两条性质的证明不难，事实上，如果形式系统是完全的，那么可证和真一致，将R1和R2中的“可证”换成“真”，那么这两条性质是显然的。
罗瑟的证明：考虑公式¬Prov(x)，对其应用不动点引理，有σ ↔ ¬Prov(S#(σ))。
如果σ可证，那么¬Prov(S#(σ))可证，但是根据R1，Prov(S#(σ))也可证。矛盾。
如果¬σ可证，不动点引理两边加否定得，¬σ ↔ Prov(S#(σ))，故Prov(S#(σ))可证，但是根据R2，¬Prov(S#(σ))也可证，又矛盾。
综上，存在σ使得σ和¬σ都不可证。
证毕
3. 丘奇-图灵途径（递归论方法）
在第一节哥德尔编码部分，已经提及过不完全性定理与递归论之间的关联，事实上，在计算与证明之间有着非常微妙的联系，证明也可以看作是一种计算，不完全性定理的递归论证明就体现了这一联系。在这一解释下，不完全性定理成为了一些数学家（如彭罗斯）论证“机器不能穷尽数学”的有力证据。
首先回顾一下递归论的一些基本知识：一个自然数集被称为递归集，当且仅当该集的特征函数是一个递归函数，一个自然数集被成为递归可枚举集，当且仅当该集是一个递归函数的值域（或定义域）。此外，每个递归函数可以唯一地映射为一个自然数，这一点的直接证明较为繁琐，但是考虑递归函数与图灵机等价，并且图灵机可以较容易地编码为自然数，因此每个递归函数对应一个自然数。
正如存在通用图灵机，也同样存在一个二元通用递归函数Uf(x,y)，它输出每个编号为x的递归函数在输入为y时的输出（如果没有输出，则称U在(x,y)处无定义）。既然Uf也是递归函数，那么Uf的定义域也是一个递归可枚举集。那么现在的问题是，Uf的定义域的补集是否也是递归可枚举的?答案是否定的，根据图灵停机定理，编号为x的递归函数对y有定义的二元组集合(x,y)不是递归的，而根据克莱尼（Kleene），如果一个集合及其补集都是递归可枚举的，那么这个集合是递归的，既然(x,y)已经是递归可枚举了，那么其补集一定不是递归可枚举的。
对于一个如第一小节第3部分所描述的恰当的形式系统S，所有S中可表示的关系都是递归可枚举的。同时根据可表示定理，如果系统S还包含初等数论，有足够的表示能力以至于所有的递归可枚举关系都在这样的形式系统中可定义。因此，包含初等数论的形式系统中能且只能定义递归可枚举关系。由此可以证明不完备性定理：
丘奇图灵证明：通用递归函数Uf所对应的递归可枚举集记为K，K可在形式系统S中表示，将表示K的谓词记为U。K的补集K’不是递归可枚举的，换言之，¬U不能表示集合K’。那么有两种可能：
1. 存在一对在K中的(m,n)，使得¬U(m,n)可证，但根据定义，U(m,n)也可证，这说明形式系统是不一致的
2. 存在K’中的(m,n)，使得¬U(m,n)是不可证的。同时，既然假定系统是一致的，那么U(m,n)也是不可证的。
因此存在闭语句U(m,n)，其本身和否定都在形式系统中不可证。
证毕
三．第二不完全性定理
如果一个形式系统是不一致的，那么根据古典逻辑的爆炸律，所有闭语句都是可证的。因此，如果某个假命题在系统中是不可证的，那么就说明这个形式系统是一致的。因此，闭语句¬Bwb(S#(0=S0))，即“0=1是不可证的”可以看作是表达系统S一致性的命题，记为Con(S)。
第二哥德尔不完全性定理说的是，如果包含皮亚诺算术PA的形式系统S是一致的，那么Con(S)在S中是不可证的，也就是说，一个足够强的一致的系统不能证明自己是一致的。
表面上看，似乎可以把第二不完全性定理看作是第一不完全性定理的一个推论：
如果Con(S)为真，那么根据第一不完全性定理，存在一个第二小节哥德尔-罗瑟证明中构造出来的闭语句σ，使得¬Bwb(S#(σ))为真，因此有Con(S) → ¬Bwb(S#(σ))，同时，根据不动点引理，有σ ↔ ¬Bwb(S#(σ))，结合起来就有Con(S) → σ。这样一来，如果Con(S)在S中可证，那么σ也在S中可证，这与第一不完全性定理矛盾。
但是这个证明是不对的，因为我们在导出Con(S) → ¬Bwb(S#(σ))时，是通过使用第一不完全性定理得出的，但是在S中并不能证明第一不完全性定理。因此我们需要证明的是，Con(S) → σ不仅是真的，而是在S中可证的，要做到这一点就要求上述的语法的算术化不仅是在S中可定义，而且在S中可表示，而这需要数学归纳法（因此第二不完全性定理的条件变成了皮亚诺算术PA）。这一证明并不容易，需要高度技术化的处理，具体细节同样可参考冯琦《数理逻辑导引》第十三章。
对于第二不完全性定理的解读有一个很著名的误解，即我们永远不知道一个足够复杂的形式系统是不是一致的。但是如果我们仔细分析就会发现，如果一个形式系统S中真的可以证明Con(S)，我们就会相信S是一致的吗？并非如此，因为如果S是不一致的，那么任何闭语句，包括Con(S)当然也可以在S中证明。所以结果是，不论一个形式系统是否可以证明自己是一致的，我们都不能因此相信它是一致的（相反，对于一个一致但Ω-不一致的系统而言，它甚至能证明自己不一致）。一致性的有说服力的证明总是需要在别的系统中进行，比如根岑就利用超限归纳法证明了皮亚诺算术PA的一致性。
参考：
《数理逻辑——证明及其限度》 郝兆宽 杨睿之 杨跃
《哥德尔不完全性定理》 雷蒙德·斯穆里安
