# 第15章：也许为真——但你无法证明！ 本章标题听上去像是小毛贼可能对警察说的话。但实际上，它宣称了过去100年里逻辑学中另一个最重要的结果。（快速警告：前面的章节中我使用了小写字母 ($$a,b$$ 等等) 表示语句。本章我将使用大写字母($$A,B$$ 等等)表示语句，以避免任何可能与数字的混淆。） 莱布尼茨不是逻辑学史上唯一有雄心壮志计划的逻辑学家。另一个人物是20世纪最重要的数学家之一，大卫·希尔伯特（David Hilbert，1862-1943），生活和工作于哥廷根。其计划通常称作**数学基础的希尔伯特纲领**（Hilbert Program in the Foundations of Mathematics），该纲领试图证明数学是一致的，即证明在数学中永远不会证明形如 $$A$$ 且$$\neg A$$ 的东西。1920年代，数学家仍然处于发现罗素悖论（我们在第5章见过）及其他同类悖论带来的震惊之中。这类悖论冲击到数学最核心的部分。希尔伯特想确保这种事情以后再也不会发生。 我们在这里要稍微小心一点。对一致性的证明当然也是数学证明。若数学是不一致的，或许它终究可以证明其一致性。事实上，若使用的逻辑是我们在第2章中见过的那种，若数学是不一致的，则它能证明一切！正如我们在那里见到的，在这种逻辑中，任何命题都可以从矛盾中得出。因此，对一致性的证明必须在某种特别安全的数学推理中完成。希尔伯特称这种推理为**有穷的**（finitary）。不过这与我们要讲的内容并不相关。 有关的是下面这些。要证明某个东西是一致的，你首先要对它有个确切的了解。如果你要运用数学证明它，你要对数学有个精确的界定。因此，作为其主要主要纲领的预备步骤，希尔伯特需要为数学提供一个恰当的公理系统，从而证明其一致性。 一个公理系统由一组**公理**（axioms）构成。公理是无需证明即可被接受的东西。（公理集可以是有穷的，也可以是无穷的。但如果是无穷的，则我们要能识别某个东西是不是公理。具体而言，需要有一个算法来判定这件事。）该系统中的一个**证明**（proof），就是一个陈述序列，其中每个陈述要么是一条公理，要么可以从前面的陈述通过推演得到。该系统的**定理**（throrems），就是每个证明最末尾的陈述。于是，定理就是从公理出发，最终能推演得到的东西。 公理化方法是数学中的一个古老方法。它被古希腊数学家欧几里得（Euclid，公元前 4 世纪中叶至 3 世纪中叶）应用于几何。不过，有点奇怪的是，直到 20 世纪，该方法才在数学中被广泛应用。在此之前，数学中被公理刻画的部分，就只有几何（或者更准确地说，是各种几何；19世纪初，数学家已经知道除了欧几里得几何之外的其他几何——非欧几何）和抽象代数的某些部分。 希尔伯特的宏伟计划则要求所有数学都被公理化。即，我们需要一个公理系统，其所有定理恰好是所有真的数学论断（无论人们如何理解数学中的真是什么）。这种公理系统的存在性，被或许是20世纪最著名的逻辑学家、奥地利数学家哥德尔（Kurt Gödel，1906-1978）反驳了。哥德尔表明，别说整个数学，就是对数学中关于自然数（0，1，2，…）的部分，也无法提供这样一种公理系统。数学中的这部分通常被称作**算术**（arithmetic）。因此，哥德尔证明的是，即使有公理系统可以刻画算术的*部分*真理，也没有公理系统可以刻画算术的全部真理。正如逻辑学家所说，该公理系统必定是**不完全的**（incomplete）。 有了我们在第14章学到的东西，哥德尔的结果就可以以相当直接的方式证明。证明仍然是归谬法。考虑一个能谈论数并能表达对数的操作（加、乘等）的符号语言。这种语言并不难得到。在该语言中可表达如下陈述：编码为$n$的程序输入 $$i$$ 后会终止。（要证明这一点需要费点功夫，但并不难。）称该陈述为 $$S\_{ni}$$。现在假设存在一个完备的关于算术的公理系统，即一个其所有定理恰好是该语言中所有真陈述的公理系统。于是就存在一个判定 $$S\_{ni}$$ 是否为真的算法：我们只要以一种系统的方式开始证明所有定理即可，确保任何可被证明的迟早被证明。（不难设计这样一个程序。）这样，迟早要么得到 $$S\_{ni}$$ 的证明，要么得到 $$\neg S\_{ni}$$ 的证明，从而判定上述问题。（我们可能不知道要多久才能完成，但这不重要）。但第 14 章的停机定理告诉我们，不存在一个算法能判定这件事。因此，不存在这样的公理系统。 我刚刚概述的证明并非哥德尔本人的证明。事实上，哥德尔的证明出现于 1931 年，而图灵证明停机定理是在 5 年之后。但哥德尔的证明和图灵的证明一样精巧——如果说不是更精巧的话——而且也使用了某种自指。哥德尔证明的概要如下。 假设我们在有一个其语言有足够表达能力的算术公理系统。该系统的所有定理都为真，但它可能无法证明该语言中**所有**真的陈述，因此它可能是不完全的。该语言的一个数学陈述就是一段文本。正如我们在第 14 章指出的，这样的陈述可以被编码为一个数。一个计算机程序就是一个陈述序列，同样正如我们在第14章指出的，它也可以被编码为一个数。但一个数学证明也只是一个陈述序列，因而也可以以相同方式编码为一个数。 现在考虑这个陈述：$$x$$ 是编码为 $$y$$ 的陈述的证明（的编码）。该陈述本身是一个关于数的陈述，它可以表达为该语言中的一个语句 $$Prov(x,y)$$。并且，只要该系统的公理足够强，就有： * 若 $$m$$ 的确是编码为 $$n$$ 的定理的证明（的编码），则 $$Prov(m,n)$$ 可在该公理系统中被证明。 要证明这些事情实际上相当难，需要一些可观的数学。但它可以做到，正如哥德尔所证明的。 说编码为 $$y$$ 的陈述是可证的，即是说它存在一个证明：$$\exists xProv(x,y)$$。但是——这是哥德尔证明的真正巧妙之处——通过一个精巧的构造，我们可以找到一个本质上形如 $$\neg\exists xProv(x,n)$$ 的语句，其编码恰好是 $$n$$ 本身！该陈述相当于说，本陈述（在系统中）不可证。称该语句为 $$G$$（代表哥德尔）。 现在，假设 $$G$$，即 $$\neg\exists xProv(x,n)$$，在该公理系统中是可证的。那就有个数 $$m$$ 是 $$G$$ 的某个证明的编码。这样，$$Prov(m,n)$$ 就为真，因而在公理系统中是可证的（根据上面的 $$\bullet$$）。但由此可得 $$\exists xProv(x,n)$$ 是可证的。于是该公理系统就是不一致的。假设系统要是一致的，则 $$G$$ 就是不可证的。但如此一来它就是真的，因为它恰好就是说它自己不可证！因此，该语言中有真的语句在系统中无法被证明。这样，算术就没有完全的公理系统。 哥德尔定理——无论它是如何证明的——明确表明了公理化方法在数学中的限度（这不是说公理化方法不应该被使用：事实上，如今公理化方法比以往任何时候都更加是数学方法的主要部分）。特别的，它给了希尔伯特纲领致命一击。算术无法被公理化——更不用说整个数学了。哥德尔的结果已被认为有很多哲学上的后果，包括关于数的本质，我们关于数的知识，甚至是人类心灵的本质。争论仍在继续，我们这里就不展开了。 让我再次以提出关于该定理的一个问题结束。我给的两个证明在数学上是无可辩驳的。但两个证明都做了一个假定（希尔伯特当然认为——或至少希望——它是成立的）：即关于数的真陈述，以及刻画其任何部分的公理系统是一致的。这在哥德尔的证明中是相当明确的假定，而我也在第一个证明中给出了。该证明假定 $$S\_{ni}$$ 和 $$\neg S\_{ni}$$ 中**恰好有一个**会出现，从而确定事情是如此还是那般。但如果系统是不一致的，这就不再成立：可能两个一起出现，使得事情悬而不决！ 现在，正如有些读者可能看到的，哥德尔证明中使用的语句 $$G$$ 很像我们在第 5 章见过的说谎者悖论的表亲。两个都对某个语句，即它自己，说了它不具有某个关键性质。事实上，有一个关于可证性的悖论与说谎者悖论密切相关。考虑如下语句：**本语句不可证**。假设它是可证的，则它是真的。因而它是不可证的。因此（据归谬法），它不可能是可证的。但我们刚刚证明了这一点，因此它**是**可证的！ 如果我们试图对语句 $$G$$ 在其公理系统中进行这种推理，则它无法在该系统中再现。或许令人惊讶的是，若系统是一致的，则可证的都是真的这一论断并不能在系统中得到证明。（这一点由德国数学家Martin Löb（1921-2006）在 1955 年证明，因而通常称作 **Löb定理**。）因此该悖论无法用于证明公理系统的不一致性。然而，它确实表明，自指悖论就藏在算术周围。考虑到这一点，人们或许不应该如此自信地认为，关于数的真理是一致的。 > 本章要点 > > * 一个算术公理系统是完全的，若它能证明其语言中的所有真语句。 > * 没有其语言具有足够表达力的公理系统是完全的。 > * 该结论可由停机定理推出。 > * 它也可以通过考虑本质上相当于说本语句（在系统中）不可证这样的语句而证明。 尾声：哥德尔第二不完全性定理 本章我们考察的结果有时称作哥德尔**第一**不完全性定理。在证明这一结果的同时，哥德尔还证明了另一个结果，称作第二不完全性定理。它本质上表明了，如我我们有一个我们考察过的那种一致的公理系统，则它无法证明被认为表达了该系统一致性的语句——只要该系统是基于我们在第2章中看到的逻辑。事实上，有了 Löb 定理，可以很容易证明这一点。 首先，注意到既然系统能证明 $$\neg 0=1$$，那么若它还能证明 $$0=1$$，则它就是不一致的。反过来，若它是不一致的，则它能证明 $$0=1$$，因为从矛盾可以推出任何结论，这是我们在第 2 章中提到的。因此，系统是一致的一个简单说法是说它无法证明 $$0=1$$。 现在，设 $$A$$ 是该语言中的任何语句，记其编码为 $$\langle A\rangle$$ ，则 Löb 定理更精确一点的表述如下： * 若系统能证明语句 $$\exists xProv(x,\langle A\rangle)\to A$$，则它也能证明语句 $$A$$。 即： * 若系统无法证明语句 $$A$$，则它无法证明语句 $$\exists xProv(x,\langle A\rangle)\to A$$。 因此，作为特例，若它无法证明 $$0=1$$，则它无法证明： * $$\exists xProv(x,\langle 0=1\rangle)\to 0=1$$ 换言之，若它是一致的，则它无法证明 $$\exists xProv(x,\langle 0=1\rangle)\to 0=1$$。 但这样一来它就也无法证明 $$\neg\exists xProv(x,\langle 0=1\rangle)$$，因为无论 $$C$$ 是什么，$$A\to C$$ 都可以由 $$\neg A$$ 推出（如第 7 章中的真值表显示的，若 $$A$$ 为假，则 $$A\to C$$ 为真）。因此若系统是一致的，则它无法证明 $$\neg\exists xProv(x,\langle 0=1\rangle)$$，即（无法证明）它**是**一致的。这就是哥德尔第二不完全性定理。 该定理给了希尔伯特纲领第二个打击。回顾一下，该纲领的目标首先是公理化数学，然后其次是证明该公理系统是一致的。这样的证明当然是数学证明，因而在系统自身内可以实现。第一不完全性定理表明，纲领的第一步不可能实现。 --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://wxflogic.gitbook.io/logic/chapter15.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.