形式化方法

来自计算思维百科
跳转至: 导航搜索

德国数学家康托尔(G. Cantor,1845~1918)从1874年开始,对数学基础作了新的探讨,发表了一系列集合论方面的著作,从而创立了集合论。康托尔创立的集合论对数学概念作了重要的扩充,对数学基础的研究产生了重大影响,并逐步发展成为数学的重要基础。

然而不久,数学家们却在集合论中发现了逻辑矛盾,其中最为著名的是1901年罗素(B. Russell)在集合论概括原则的基础上发现的“罗素悖论”,从而导致了数学发展史上的第三次危机。

罗素悖论可以这样形式化地定义:Let R = {x|x∉x}  then R∊R ⇔R∉R。为了使人们更好地理解集合论悖论,罗素将“罗素悖论”改写成“理发师悖论”。其大意是,一个村庄的理发师宣布了这样一条规定:“给且只给村里那些不自己刮胡子的人刮胡子”。现在要问:理发师给不给自己刮胡子呢?如果理发师给自己刮胡子,他就属于那类“自己刮胡子的人”,按规定,该理发师就不能给自己刮胡子;如果理发师不给自己刮胡子,那么,他就属于那类“不自己刮胡子的人”,按规定,他就应该给自己刮胡子。由此可以推出两个相互矛盾的等价命题:(1)理发师自己给自己刮胡子,(2)理发师自己不给自己刮胡子。

为了消除悖论,奠定更加牢固的数学基础,20世纪初,逐步形成了关于数学基础研究的逻辑主义、直觉主义和形式主义三大流派。其中,形式主义流派的代表人物是大数学家希尔伯特(D. Hilbert)。他在数学基础的研究中提出了一个设想,其大意是:将每一门数学的分支形式化,构成形式系统或形式理论,并在以此为对象的元理论即元数学中,证明每一个形式系统的相容性,从而导出全部数学的相容性。希尔伯特的这一设想,就是所谓的“希尔伯特纲领”。

“希尔伯特纲领”的研究基础是逻辑和代数,主要源于19世纪,英国数学家乔治·布尔(G. Boole)所创立的逻辑代数体系(即布尔代数)。它的目标,其实质就是要寻找通用的形式逻辑系统,该系统应当是完备的,即在该系统中,可以机械地判定任何给定命题的真伪。

希尔伯特对实现自己的纲领充满信心。然而,1931年,奥地利25岁的数理逻辑学家哥德尔(K. Gödel)提出并证明了关于形式系统的“不完备性定理”,包括两条定量:(1) 任何一个相容的数学形式化理论中,只要它强到足以蕴涵皮亚诺算术公理,就可以在其中构造在体系中既不能证明也不能否证的命题。(2) 任何相容的形式体系不能用于证明它本身的相容性。该定理指出希尔伯特纲领中所描述的形式系统是不存在的,从而宣告了著名的“希尔伯特纲领”的失败。希尔伯特纲领的失败同时也暴露了形式系统的局限性,它表明形式系统不能穷尽全部数学命题,任何形式系统中都存在着该系统所不能判定其真伪的命题。

“希尔伯特纲领”虽然失败了,但它仍然不失为人类抽象思维的一个伟大成果,它的历史意义是多方面的。对计算学科而言,最具意义的是,希尔伯特纲领的失败启发人们应避免花费大量的精力去证明那些不能判定的问题,而应把精力集中于解决具有“能行性”的问题。