如何证明一个数学命题的不可证性？ 第1页

匿名……还是实名吧。实名反对以上所有回答。人家问怎么证不可证，就回答怎么证的途径就好了，写那么多有的没有干什么……

1. 讨论的基础：证明的编码和解码，哥德尔不动点定理
2. 灾难的开始：哥德尔第一不完备定理、塔斯基真不可定义定理、哥德尔第二不完备定理
3. 语言的天劫：柴廷不完备定理
4. 证明论的伊始：更有意义的不可证性
5. 不可证性的终结

讨论的基础

证明的编码和解码

首先讨论任何东西都需要有一个讨论基础，这叫做公理系统。

我们现在要假设这个公理系统F里面至少有初等算术（不懂的就当公理系统至少存在小学数学就好了），这样的话，我们就可以将所有的公式和推导编码成自然数了，也就是所谓的哥德尔编码，当然我们也可以将自然数反过来对应成公式和推导。

基于对计算机科学的基本常识，我们很容易就能理解为什么能够将证明编码成数字——因为我们就是对于计算机上的代码这样做的。而你如果需要更加精细的编码方式的话，这里可以给出一个方案：
首先将空集公理宣告的空集的基数编码成零，0的后继编码成1.
所有的公理，公设，缩写符号都赋予一个奇质数.
自由变元和所有的公理模式编码成2的p次，q次，r次……幂.
最后 就是证明串的编码。
根据算术基本定理即刻可得编码的分解是唯一的因此编码对应的证明串也是唯一的。

自然地，不是每一个自然数都对应有意义的推导和公式，但我们只需构造一个原始递归函数ProofCheck(Axiom,Proof)验证自然数对应的证明串是否合法即可；合法证明串的起始就是证明的前提，证明串的终结就是证明的结论。显然刚才提到的证明串编码函数Code(Axiom,Proof)，解码函数unCode(Axiom,nat)，解码验证函数ProofCheck(Axiom,Proof)也对应一个自然数，并且基于中学数学的常识，我们用自然数集就足以得到公理系统F的所有证明。

在别的文章里面，也有将unCode(ProofCheck())写作Provable()的，也就是所谓的“证明函数”。但是我写这篇文章的目的是在coq下证明这一切，因此不占用已有的定义。

接下来我们尝试在不钦定“真”的意义的情况下进行讨论，于是我们将在各方均接受的直觉主义下工作。然后，引入两个定义。

• False(A)，教科书上写作¬A这里写作~A，汉语读作否定，使命为从A出发推导出矛盾，定义为在系统F下推导出0=1.
• Con(F)，汉语读作系统F一致，使命为系统F之内没有矛盾，定义为不存在一个证明从系统F出发得到0=1.

因为无矛盾律的要求，这个命题显然是一个真命题，但是属于一个可证命题还是一个公理，我们姑且放在一边。

引理1 哥德尔不动点定理

你学会了加法和乘法就等于学会了编码，是时候来一点实践了！我们现在来证明哥德尔不动点定理。

证明： 对于系统T内任意函数F(x), 皆存在证明串A, 使得A <-> F(|A|).
|A|的定义就是Code(T, A).

1. 当T足够强时我们可以定义apply(|A(x)|, |B(x)|)=|A(|B(x)|)|.
2. 对于任意F(x), 定义G(x)为F(apply(x, x)).
3. 定义A为G(|G(x)|).
4. A <-> G(|G(x)|)
<-> F(apply(|G(x)|, |G(x)|)
<-> F(|G(|G(x)|)|)
<-> F(|A|)

证毕.

灾难的开始

哥德尔第一不完备定理

现在我们先证明所谓的哥德尔第一不完备定理：

Godel.unProvable()，使命为“本命题不可证”。然后，不可证这个性质怎么描述呢？

• 枚举全体自然数集N内对应的一切合法证明串的终结。刚才，已经见证了unCode(ProofCheck())是原始递归的。当输入为Godel.unProvable()的时刻，这个枚举函数不会停机，除非输入~Godel.unProvable()也停机。
• 如果N内有合法证明串可以Godel.unProvable()为终结的话那么也会存在一个串以公理集作前提0=1为终结。（导出矛盾）
• 可以系统F内取出一个Godel.unProvable(F)的证明，当且仅当可以在系统F内取出~Godel.unProvable()的证明。

显然，如果要构造出这个性质，问题的关键在于构造验证证明串合法的对应概念ProofCheck()。ProofCheck()的构造难度虽然不如之前在群里面讨论的“在coq里面构造一个coq”，但是定理检查器也不是什么好构造的的概念，想要自己一个人重新造轮子的朋友请三思。

以上的说法在直觉主义下不是等价的，但是我们只需要牢记我们的使命是构造适当的形式，使得Godel.unProvable() <-> ~Godel.unProvable(). 这样，如果系统F可以证Godel.unProvable()的肯定，那么就会证出它的否定；如果能证它的否定，又会证出它的肯定。最后将此不可证命题用哥德尔不动点定理投射进自然数集合N，指定的公理系统F之内便可存在“可被识别而不可证明的真命题”。

最后，必须进行一些逆数学（Reverse mathematics）上的论证。

• 首先，公理集必须足以支撑编码函数的存在。如上所述，我们只用到了加法和乘法——事实上如果没有乘法，无法将关键的Godel.unProvable()编码。
• 然后，公理集必须见证哥德尔不动点定理的成立，否则无法将刚才所造的不可证命题投射进自然数集，使得其被公理系统识别为真命题。
• 公理集F内必须有Con(F)。也就是说公理集F是一致的
• 最后，为了避免使用排中律和钦定“真”这一谓词的定义，我们用双重否定取代“真”，三重否定取代“假”。

       设Godel.unProvable.main(Axiom Z, nat n)的定义为 当Z -> ProofCheck(Z, unCode(Z, n))) -> False成立的时刻给出~False 并有Godel.unProvable(A) <-> ~Godel.unProvable(A). 我们将Godel.unProvable.main(F,Code(F,A))缩写成Godel.unProvable(A).     

现在开始我们的证明。

• 引入Con(F+Con(F))，取出Con(F)。
• Godel.unProvable(A) <-> ~Godel.unProvable(A)两边加双重否定，有~~Godel.unProvable(A) <-> ~~~Godel.unProvable(A).
• 如果有F -> Godel.unProvable(A) 立刻有F -> Godel.unProvable(A) -> ~~Godel.unProvable() -> ~~~Godel.unProvable(A).得到矛盾，忤逆了Con(F)。
• 因此Godel.unProvable(A)在F上不可证。
• 这刚好就是我们需要的，因此我们在F+Con(F)下构造出了Godel.unProvable(F,n)的证明。
• 最后只需要见证Godel.unProvable(A)被系统F接纳，也就是Godel.unProvable(A) <-> A .其中A是一个证明串，援引之前已经证明的哥德尔不动点定理即可得证。
• 因此Godel.unProvable(A)也确实会得出我们需要的~False（如果引入排中律就立刻可以从双重否定得到True了）并且是被系统F接纳的命题。

我们还可以将命题增强为Godel.unProvable(A)独立于系统F，"独立"本来就是枚举系统里面的每一个真值所以不需要排中律。同样的，

• 如果有F -> ~Godel.unProvable(A)
• 立刻有F -> ~Godel.unProvable(A) -> ~~~Godel.unProvable(A) -> ~~Godel.unProvable(A).
• 然后同理可证。

对于其他并非次协调的多值逻辑系统也是同样的处理。

• 真值空隙gap和超赋值空隙和不可证度为1的以及可证性概率0都不需要作额外处理，他们已经是不可证的了。
• 然后调整Godel.unProvable(A)的定义为True(A,x) <-> True(A,y)的函数（当A的真值是x的时候，当且仅当可以推出A的真值是y），x遍历每一个真值和超赋值。
• 最后选择y的取值使得Con(F)完蛋就可以了。

之所以这里不用合取而是用蕴含是因为某些非经典逻辑的合取析取公理都是改过的……唯有用蕴含和爆炸原理最安全。

次协调逻辑免疫哥德尔第一不完备和第二不完备因为它们根本不需要Con(F).

塔斯基真不可定义定理

利用同样的方法证明塔斯基真不可定义定理。这里只考虑标准逻辑的情况——我们无需在直觉主义逻辑中关心真谓词，因为真的定义T原则依赖排中律而直觉主义逻辑不适用。理所当然的次协调逻辑也不会有这个问题。

设系统F存在一个Tarski.True(),使得对于F内每一个公式A存在Tarski.True(g(A)) -> A，其中A是一个证明串。

我们同样运用哥德尔编码和哥德尔不动点定理，见证一个说谎者语句sayLie()，使命为“本命题是假命题”，定义为，见证存在一个sayLie()在F之内，当且仅当Tarski.True(sayLie(A)) -> ~A。引入Con(F)，就得到Tarski.True不可在F内定义。

我们可以注意到这只是Godel.unProvable()的另外一种形式。而在标准逻辑中，塔斯基真不可定义定理便尤为重要：因为塔斯基真不可定义，所以保真的哥德尔编码集不递归，编码集不递归因而F非决定，F非决定引入丘奇图灵论题，因而F有命题不可证，因而F不可证Con(F)。

哥德尔第二不完备定理

接下来，我们要证明哥德尔第二不完备定理，就是Con(F)不可证。

• 我们刚刚已经见证F+Con(F)内有定理Con(F) -> Godel.unProvable(A)。
• 如果F -> Con(F)
• 就有F -> Godel.unProvable(A)
• 又有Godel.unProvable(A) -> ~Godel.unProvable(A)
• 因此有F -> ~Con(A)
• 这忤逆了公理Con(F+Con(F))，因此Con(F)在F上不可证。

然后我们可以得到证明论的一个结论，就是能够证Con(F)的系统W一定比系统F强。顺便地，因为Con(F)成立就意味着存在一个F的模型，我们定义Con(F+Con(F+Con(F+……)))意味着存在F的一个可数传递模型。

这个所谓的“强”只是证明论意义上的强，并不是真的代表系统F的一切内定理都被系统W接纳。如评论所述，PA和PRA+超限归纳互相都有对方证不出的命题（PA无超限归纳PRA无量词），但是PRA+超限归纳 -> Con(PA).

Chaitin不完备定理

我们在此处将Kolmogorov复杂度（算法复杂度，算法熵）定义为表达一个字符串所需要的最短证明串的长度。

我们可以无忧无虑的推而广之，一个数字的算法熵就是生成数字的最短公式的长度；一个证明串的算法熵就是它的最短版本的证明的长度。

一个给定对象的算法熵和它的描述方法的选取无关。

2021年2月节略：本人之前的证明这个定理的方法是：

公理集是有限的，公理集导出的递归可证定理集是无限的，但是最短定理集是有限的，所以能证的算法复杂度有上界。将不变性定理作用于这个最短定理集，便可得到所需的上界。这个上界就是理论的终极上界。

最终导出结论：绝对几何，Presburger算术，自验证系统、次协调逻辑之类的系统对于免疫这种意义下的不完备是无能为力的。如果HOD猜想成立，那么V = Ultimate L便是人类可得到的证明力上界最大的理论。

但正如 @ZS Chen 所述的那样，这其实只是一阶逻辑的语法导致的基本结论，并不需要Chaitin不完备定理，通过这个通路证明Chaitin不完备定理完全是小材大用。

这里直接引回 @ZS Chen 的Chaitin不完备解释：

• GC(x)的定义是"存在一个自然数y, 自然数x的最短生成公式是y, 并且y大于z^[1]",
• GC(n)中的"n"是一个形如"s....s0"的PA语言中的一个常项。
• 对比ω-不一致的定义: "T是ω-不一致的, 当且仅当有某个语句P(x)使得对于每个自然数s....s0, T都能证明P(s....s0), 但是T也能证明[存在x, ~P(x)]".
• Chaitin定理的所描述的现象就有点像这个的对偶: "T能证明[存在x, GC(x)], 但是对于每个自然数s....s0, T都不能证明GC(s....s0)".

此外，将原有的我自己证的不变性定理换成别人的更通俗的版本 @ALENAVENGER；关于自然数的命题总是符合直觉主义的要求，不变性定理也同样，但如同Chaitin定理所强调的那样，具体的理论上界的值不会是递归可证的。

一般的科普书或者民科通常会到此结束。但是很明显，目前为止我们都是在什么“这句话不可证”“这句话是假话”“这句话是不能用少于二百三十三个汉字定义的话”之类的车轱辘话【3.1】里面打转，这对证明我们希望证明的有意思的结论，比如说连续统假设可证不可证，选择公理可证不可证，一点帮助也没有。为了解决这个问题，我们引入一个概念，“翻译”。

既然只需理论包含初等代数（严格来说，我们应该工作在有穷主义算术下，也就是PRA的带量词版本 ），就可以给理论内的证明串给予一个编码，而编码又可以还原为证明串；然后，两个不同理论T1、T2之内的语言L1、L2，就可以期望存在一个原始递归函数使得L1上的每一个编码可以唯一存在地赋予给L2；这就是翻译了。

当这个翻译的存在性成功确立起来之后，我们就终于可以开始证明有意思的命题是不是不可证了。

• 假设~Con(F+A)，也就是说系统F+A下存在一个到0=1的有穷证明
• 对证明运用翻译函数，我们现在原始递归地得到了F下到0=1的有穷证明
• 现在我们得到了~Con(F+A) -> ~Con(F)
• 引入Con(F)
• 假设不成立，立刻可得Con(F) -> Con(F+A)

就这样，我们刚刚证明了A的不可证否性并且在有穷主义算术之下完成了这一系列操作！

刚才的证明目标又叫做相对一致。我们刚才的讨论之中没有诉诸模型直观，实际上存在大量相对一致结果是不能用刚才的手段证明出来的，因为以上的证明等效于对集合论全集V的“削减”，令其更加“贫乏”，因此这种翻译构造方法又被称为内模型法。

比如你刚刚证完了“ZFC所有的集合都是可构造的（V=L）是不可证否的”，然后你想要证不可证是，但是因为V=L的模型限制你是证不出来的，因为你不能在ZFC其内假设存在一个L的真扩张同时保持Con(ZFC)。

但是我们又必须迈过这个门槛，否则我们无法证明任何不可构造集的存在性是不可证否的，这意味着无法研究非良基集合，大基数集合，选择公理不成立的情况，ect。

为了研究比V更“丰富”的理论，我们需要寻求V的可数传递扩张模型，这种外模型的手段就是传说中的力迫法。

按照直觉主义的观点，在系统F内Con(F)不可证就不能承认有F的模型，就更加不用说考虑F的可数传递模型，甚至是可数传递模型的扩张模型。但是在另一方面，我们并不需要真正的考虑整个系统F的超穷总体，而只需要考量系统F的足以容纳理论翻译函数和0=1通过的有穷片段。为了构造性地见证这个可数传递模型的扩张，我们只需要考量

系统F内的任意有穷集合P均存在系统F内的另一有穷集合Q，使得Q的任意关于系统F的可数传递模型M都可扩张为F+~A的可数传递模型N。

而如果这个见证完成，便可以得到如同Con(F) -> Con(F+A)的证明一般得到我们想要的不可证是Con(F) -> Con(F+~A)，到此便可得到A独立于T这个结论——完全版本的不可证。

而寻求这些集合间关系的构造就是力迫 了。因为F上力迫语言L*的定义将确保F+~A的全部性质在P内被满足，并且令假设存在的F+~A上的0=1证明串通过它自身原始递归地翻译到F上，因此只需要构造出原始递归函数L*和相关的原始递归理论翻译函数便可在有穷主义算术之下完成这一系列证明。

最后就是说明一下怎么“终结”不可证性。显然人们并不关心【3.1】的那种用哥德尔不动点搞出来的蛇皮问题——

• 诸如Con(F+Godel.unProvable(Con(F+Godel.unProvable(……))))显然并没有什么卵用
• 诸如Tarski.True(F+Tarski.True(F+Tarski.True(……)))的问题是可以通过类型论分割阶段解决的，还能用三值逻辑，语义分析等。实在不行就回到直觉主义真值下工作咯（掀桌子）
• 我们刚刚已经用有穷主义算术（实际上要求可以降低到Con(HA)）的有穷片段就表征了Con(F+Con(F+Con(F+……))).
• 对于Chaitin不完备定理来说……人类如果延续到可以看得到要研究证明长度长达BusyBeaver(748)的证明的一天的话（这是ZFC的证明力上界常数），肯定已经发明出大圣杯了，不要闲的蛋疼研究那个时代的人类的数学问题。

而除了【3.1】之外，内模型法和力迫法是用来产生相对一致性（不可证否/不可证是）的唯二方法。不可证性的另外一个重要疑虑就是，我们担心如果随意引入有意义的不可证命题到系统之内的话，会导致系统内的已经证毕的问题的真值发生变化。而如果命题O的真值免疫内模型法和力迫法的更改，那么O就是实际完备的。一阶算术是实际完备的。

而引入大基数公理可以提升模型的证明论强度，消灭有意义的不可证命题的不可证性，使得二阶算术完备，证出可构造实数集以及投影集的决定性，乃至证出Con(ZFC)。但是连续统假设是三阶算术上的强力问题，而大基数的力量很有可能是有极限的（我们不能无限的寻求反射论证获得更“强”的大基数），因此我们不能寻求大基数公理来解决连续统假设。

另外一方面，我们注意到V=L是实际完备的，因此寻找可构造集L的扩张 —— Ultimate L，使之包括我们“最”强的大基数公理，在这个终极的系统Ω下我们便得到了最强的证明论强度并且任何有营养的问题都是实际完备的。如果这个纲领得以完成，力迫法的使命也可得以完结，系统内除了公理集再也没有有营养的问题是不可证的，这个计划便是内模型计划。

参考

1. ^ z只是一个随便取的PRA可计算的大数，默认是10↑10. 没有特别的迹象表明不允许要求降低到EFA可证大数