数学形式化与哥德尔定理

数学从诞生起就开始了形式化的进程，欧几里得《几何原本》是数学形式化第一次总结，欧几里得用逻辑方法整理几何知识，建立了数学中第一个演绎体系，从定义公理出发抽象地研究了空间形式和关系. 算术一开始就是形式化，初等代数是算术的推广. 代数的进步有赖于符号体系的建立，16世纪韦达在丢番图(Diophantus，约246—330，古希腊数学家)的基础上引入了符号文字，代数成为各种数量以至多项式计算的理论，数学运算更加形式化，超脱了任何特殊数字的观念.

19世纪以前，数学形式化进程相对缓慢. 19世纪以后，由于数学分析的算术化，非欧几何、群论、布尔代数等一系列学科出现，数学形式化进程加快了.

虽然欧几里得所撰《几何原本》，已经相当抽象、相当脱离现实，但可以看出，其中的几何对象(点、线、面)是现实几何形体的理想化，其中的公理是这些对象直观上明显的关系. 可以说《几何原本》的形式与内容仍然是统一的; 由于非欧几何的相容性受到怀疑，所以在把非欧几何系统化的时候，必须保证它的定理没有一个不是从公理严格地推演出来的. 形式与内容都有，但内容就难被局外人所理解了. 而数学家却主张，必须提供有效性仅仅依赖于逻辑形式的证明，而为了达到这个目的，必须以一种非常抽象的方式来表述几何.

希尔伯特致力于数学形式化，在他的《几何基础》中，成功地建立了完善的欧氏几何公理体系. 从五组公理出发来确定基本概念的性质，并把它们作为推理的基础，逻辑地推演出欧氏几何的全部定理，把欧氏几何公理体系发展成为形式化的公理体系. 与以往相比，希尔伯特的公理化体系具有两个本质的飞跃: 首先是几何对象上达到了更深刻的抽象. 点、线、面的定义没有特定的具体内容，它们之所以成为讨论的中心，仅仅是由于它们与所选择的公理的关系; 其次，明确提出了对公理系统的基本逻辑要求，即①相容性; ②独立性; ③完备性. 这样，《几何基础》不仅具备了严密的逻辑基础而且逐步渗透到数学他领域.

自1904年起，希尔伯特在多次讲演中提出并立阐释过自己关于数学基础的观点，后来又在《数学逻辑基础》[1]中对形式主义纲领作了系统的与全面的论述. 其要旨是: 将数学彻底形式化为一个系统，在这个形式系统中，人们必须通过逻辑的方法来进行数学语句的公式表述，并用形式的程序表示推理: 确定一个公式——确定这个公式蕴含另一个公式——再确定这第二个公式，依此类推，数学证明便由这样一条公式的链构成. 在这里，语句只有逻辑结构而无实际内容，从公式到公式的演绎过程不涉及公式的任何意义. 希尔伯特认为，一旦实现上述目标，不仅解除了悖论对数学的威胁，而且也从直觉主义的攻击下挽救了经典数学，数学基础问题也就得到彻底解决. 数学因此而无懈可击.

希尔伯特把确立形式系统的相容性为首要任务，并提出了一套直接证明形式系统相容性的设想，这套设想被称之为“证明论”或“元数学”，是上述纲领的核心. 希尔伯特希望用元数学来论证对象理论的相容性，从而给出形式系统所代表的经典数学无矛盾性的绝对性证明，进而使整个数学都公理化，为整个科学描绘一幅谐合的景象.

然而，希尔伯特的元数学仍是朴素的、非形式化的，基本上仍使用日常语言. 现在，需要做的是使元数学也形式化.

1931年，奥地数学家哥德尔(K.Godel，1906—1978)发表题为《论＜数学原理＞[2]及有关系统中的形式不可判定命题》的论文. 作者沿着希伯特曾设想的路线，选定一种方法用自然数把基本形式对象数字化，例如，按以下方法给每个符号配一个奇数

还可以给每个证明公式序列配上唯一的哥德尔数，设a1， a2，…，ak是这个序列中相继的公式序列的哥德尔数，那么2a1， 3a2，…是这个证明公式序列的哥德尔数.由于项和公式是符号串，证明和演绎是符号串的有限序列，所以它们都有哥德尔数. 这样，哥德尔就把关于形式系统内对象的断定(命题)，巧妙地转换为关于自然数的断定.

哥德尔在他的论文中证明了下面的定理:

哥德尔第一不完全性定理 任一足以包含自然数算术的形式系统，如果是相容的，则它一定存在一个不可判定的命题，即存在某一命题A与A的否定在该系统中皆不可证.

哥德尔第二不完全性定理 对于包含自然数系统的任何相容的形式体系，这种相容性在该系统内是不可证明的.

上述两个定理统称为哥德尔不完全性定理. 在证明这个定理时，哥德尔的做法，就是使元数学算术化，通过哥德尔配数法把元数学的命题变成算术命题，理论的判定问题变成计算问题. 哥德尔正是用这种方法证明: 形式系统中存在着真的但不可证的命题，从而证明了形式系统的不完全性. 这种探讨的一个重要动因，就是形式系统的相容性问题，而这项否定性结果却带来了数学基础研究的划时代变革.

首先，第一次分清了数学中“真”与“可证”是两个不同的概念，可证明的例题固然是真的，但真的命题却不一定是可证明的. 对形式系统来说，“可证”是可以机械地实现的，“真”则需要进一步的思想能动性以及超穷工具，这一来突破了人们对数学真理的传统理解，把对数学真理的认识推向了崭新的层次.

第二，哥德尔不完全定理使希尔伯特想要一劳永逸地解决数学相容性的努力落了空. 因为“基于形式化的研究方法，能否对古典数学的相容性进行构造性证明，以及如果可能的话，又可以解决到什么程度，这样一个问题并没有解决”.

第三，哥德尔在证明第一不完全性定理时，肯定下列命题的公式是可推演的: ①系统对分离法则封闭; ②系统对用项代换个体变元封闭; ③当N是一个自然数并且f是一个原始递归函数时，形如f(N) =0的公式真值蕴含这个公式的可推演性. 成为算法理论或可计算理论的起点，它引导图灵提出了理想计算机概念，为电子计算机的研制提供了理论基础.

第四，哥德尔定理指出了形式化数学的局限性，但并不意味着公理化方法的消亡. 相反，哥德尔的结果极大地促进了希尔伯特“证明论”的发展. 由于指出了有限方法的不可能，人们在放宽工具限制的情况下，创造了“超限归纳法”等一些新方法，解决了一批证明论问题，使数理逻辑在新的起点上获得了新的发展.

数学的形式化使数学脱离其内容，对于数学发展来说并非坏事. 形式化的一个重要作用，是有助于数学的发明、创造. 这是由于可以从已有的数学结构中得到借鉴和启发，便于人们发现数学的前沿边界，为探索未知的数学形式结构提供类比的基础，掌握待解决问题的症结.

社会需要是推动数学发展的动力，而数学理论内部发展的需要，是推动数学发展更为重要的动力. 经验形式上的理论是走不远的. 数学家采用的方式是在已有形式基础上加以推广，得到更加一般的形式，这是数学家们共同享有的精神实体. 在这里他们所处理的是思维对象，而不是物质对象，没有内容的束缚，没有形式与内容的反复，只是从形式到形式，到更一般抽象的形式，其结果造成了数学形式脱离了内容，以及数学形式先于其内容的局面. 尽管从一个抽象等级向更抽象等级的过渡不是轻而易举的事，而数学家们乐此不疲，只要迈出一步，就是创造. 这种不顾实际存在，不管传统的教条，专注于数学形式，本质上是种精神，是几千年来的传统精神、数学的发展靠的是这种精神. 每个数学概念、定理的确切表述、新理论的开创、新学科的建立、实际问题的解决，等等，都是这种数学精神的大发扬，从而大大地推动着数学的发展.

数学的这种形式化工作，事实证明是非常必要的，成就是辉煌的. 如果没有数学事先为物理准备好工具，物理学新理论的建立是茫然的; 如果没有矩阵理论，广义相对论和量子力学就毫无意义; 如果没有这么多数学工具，供科学选用，自然科学的进步也是一句空话，即使是社会科学、经济学、历史学，等等，数学也是耀眼的光环.

在数学中，特别是在纯粹数学中，概念可以脱离实际，形式可以脱离内容，而且唯有如此，现代数学才能蓬勃发展. 也为哲学内容添了新篇章.

[1] 这两部专著是希尔伯特与其助手阿克曼、伯奈斯分别合著的.

[2] 罗素.A·N·怀特海合著.《数学原理》(共3卷)，1910—1913年出版