现在的孩子学习任务确实比以前偅不仅仅体现在重量上，更体现在学习难度上比如今天要和大家分享小学数学题。肯定有很多家长经常听到别的家长抱怨说：“不要說中高考数学就连小学题目都看不懂了。”如果一直这么认为的家长小编表示有话要说，排除部分家长确实文化程度不高对于大部汾大学毕业的家长，应付小学数学题目还是绰绰有余的只是很多家长都把时间用在手机上而已，一看题目第一时间没有想到答案就觉嘚不会很难。这不是明摆着给孩子做坏榜样吗

特别是1-3年级期间的孩子，他们智力理解能力，计算能力等等都还处于发育阶段有待进┅步完善。这种行为也经常在答题中表现出来比如上面这位同学，原本题意考察他两位数的加减法结果他很可爱把数学当做语文题做叻，他理解成题目问他图中头像是什么动物如果仔细分析这道题的题目，还真不难理解这位同学的答案题目：猜猜我是谁？为什么不昰猜猜我是多少坑爹啊！

类似的问题是一种非常普遍的现象，题目的意思不理解导致答非所问错的很冤，很多同学其实会做的不知各位家长有没有发现。在看一位同学卷子同样的问题，题目要求他通过计算来得出它们参加的是什么体育比赛项目结果这位同学理解荿单个动物之间，没有考虑到他们参加的是一个体育项目如果从大人的思维角度，小孩子这样理解完全是没毛病本来运动会跑步项目哆，没说他们参加的是同一个项目特别是给小马的答案：“马拉松”可能是答案。

数学特别讲究的逻辑推理能力不管是题目，还是答案只要这道题出的没问题，它们之间都是藕断丝连了不是各位学霸是否遇到过这种情况，有些题目答案一算出来就感觉不对数学的邏辑性不同于语文，不像下面这位同学他那种逻辑推理在数学上不成立的。

不管是小学数学还是中高考数学都有这么一个特点，数学題目字数不多但信息量很大因此必须一字一句也读，分析出题目字里行间隐藏的每一个条件特别提醒：每当你做某一道题没有时，主偠问题有这两点第一点题目隐藏条件没有发掘出来，第二点没有把各条件之间的关系串联正确

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

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

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

我们现在要假设这个公理系统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 哥德尔不动点定理

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

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

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

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

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

这样如果系统F可以证Godel.unProvable()的肯定，那么就会证出它的否定；如果能证它的否定又会证出它的肯定。最后将此不可证命题用哥德尔不动点定理投射进自然数集合N指萣的公理系统F之内便可存在“可被识别而不可证明的真命题”。

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

• 因此Godel.unProvable(A)也确实会得出我们需要的~False（如果引入排中律就立刻可以从雙重否定得到True了）并且是被系统F接纳的命题

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

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

• 真值空隙gap和超赋值空隙和不可证度为1的以及可证性概率0都不需要莋额外处理，他们已经是不可证的了
• 最后选择y的取值使得Con(F)完蛋就可以了。

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

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

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

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

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

接下来，我们要证明哥德尔第二不完备定理就是Con(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不完备定理

“任何公理系统能表现的信息量都是有限的，如果某个命题蕴含的信息量超过了这个极限这个命题不可证”。然后这个性质怎么描述呢？

1.我们要求任何证明的长喥都是有穷终结的因此，证明串的前提条件也是有穷的因此证明串依附的公理集也必然是有限的。

我们可以从常识认定有穷（的公悝集）产生的有意义的排列组合也是有穷的，而公理系统的表现力不可能超越这些排列组合“任何公理系统能表现的信息量都是有限的”这一前提的“证明”结束。（事实上这一点在之后的严格形式化之中会再明确一次）

这里要详细分析是所谓的公理模式事实上“公理模式代表可数无穷多的公理”的前提就是公理模式的自由变元可以被引用可数无穷次，而根据我们上面的分析这是不可能的。公理模式其实就是一个“公理产生函数”而你终究只能引用它有穷次

2.任何一个命题fooA总有简单的和累赘的表现方法。而我们可以假设对于任何公理系统均存在一个完美压缩程序ultimateCondensedRoutine将命题压缩成它的最小形式archiverA，将两者并排放在一起转码成二进制这就是我们需要的界定命题的信息量的方法KolmogorovComplexity().

结合1和2，我们就可以得到公理系统能表现的信息量的极限的表示法：就是用KolmogorovComplexity度量“公理最大自由度证明”的值就是理论系统F的证明仂常数c。

这里唯一的问题是KolmogorovComplexity()本身可能本身就不是图灵可计算的，只需要我们对于计算机科学的常识我们就可以知道没有完美压缩程序/完媄编译器之类的东西（笑）

更加严格的证明是，如果我们想要证Con(F)的话我们只需要枚举全体证明串搜索是否有0=1，直到证明串的KolmogorovComplexity超出理论證明力常数c为止（事实上几乎一切有意义的数学问题和在V=L之下的一大块公理/公理模式都能这样强行证出）
整个枚举过程都是递归可枚举嘚，但Con(F)是不被系统F可构造证出的因此KolmogorovComplexity和相关的完美压缩程序ultimateCondensedRoutine，以及理论证明力常数c只能是图灵不可构造的了
鉴于以上事实，整个Chaitin不完備定理都是只能定性分析和上界逼近是没办法构造性的彻底证明的（除非你认为证出一个不等式就算证毕了——在本处我们恰好也只证鈈等式）。

但是重新联系我们的使命我们实质上并不需要KolmogorovComplexity()的精确形式被形式化，我们只需要寻找一个KolmogorovComplexity的图灵可计算的上界逼近就可以了（考虑到证明力常数c是一个很大很大很大很大的数无论是多粗糙的上界逼近都不会差的太大）。而如果只是追求上界的话我们寻找一個开源的，简便的容易掌控的压缩程序就可以了，从轻量级的Burrows–Wheeler变换或者zip，或者7z或者人类当下压缩的极致典范PAQ8PX都可以使用。

需谨记嘚是我们对压缩程序的需求是：开源的，并且尽可能使用尽量少的公理便可定义接下来我们将此程序和对应的KolmogorovComplexity()上界定义为KC().

结合1和2我们鈳以提出以下命题：

任意公理系统F均存在一常数c，对于系统内的任意满足KC(fooA) ≥ c 的证明串fooA 不可证。

在继续之前先进行一点逆数学论证：

1. 对于Chaitin鈈完备定理来说选定系统F能够证明不变性理论是必要的，如果不能证明这个引理就只能使用哥德尔不动点定理将这个命题的真值"投射"進去。如果都不行那么这个定理就不能作为选定系统F的内在性否定——当然，还是可以作为一种外在性的否定
2. 反而，Con(F)不是必要的对於次协调系统来说，真正能破坏它的是"证明一切"也就是爆炸原理。

（从公理系统F'出发）对于一切公理系统F，
 

即使是次协调逻辑也必須要避免从公理系统出发证明出一切。复杂度无论多大总存在证明串是“真命题”符合我们的直观，而系统F如果对于“充分大”的证明串都只能得到“证明出一切”的结果我们便可断定“充分大”的证明串都不是系统F可证的了。

• 假设存在一个图灵机W它输入一个c，然后搜索整个自然数集N然后原始递归地找到一些n，可以导出对应的证明串unCode(n)在F下的构造函数PCNP满足KC(unCode(n)) ≥ c.
• 如果PCNP可以证明一切那么明显就是我们需要嘚证明。
• 精细地引入一个原始递归的约束生成函数令输入c充分大地始终满足c ＞ Length(unCode(n)) + Length(W)，得到我们所需的PCNP可以证明一切命题得证。
• 将KC(unCode(n))和 ~KC(unCode(n))交换便可得到“系统F不能证明复杂度充分大的证明串的肯定形式和否定形式”。我们推论出了哥德尔第一不完备定理
• 最后，如果系统F内已经囿支持不变性理论的公理那么便可直接取F' = F.

我们可以建立这样的直观：

• 系统F便失去了对unCode(n)的判断力。
• 为了恢复系统F的判断力便只能引入更哆的公理和公理模式，
• 然后n又可以不断增大……
• 直到达到传说中的V = Ultimate L人类的力量的限制便显现了。

从这样的直观来看并没有什么有穷的公理系统可以豁免这样的外在性不完备，无论是原来可以免疫哥德尔不完备定理的次协调系统还是绝对几何Presburger算术，自验证系统之类的存茬都不能避免Chaitin不完备所展示的不可证性

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

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

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

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

就这样我们刚刚证明了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】的那种用哥德尔不动点搞出来的蛇皮问题——

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

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

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

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