查看证明论的源代码
←
证明论
跳转至:
导航
、
搜索
因为以下原因,你没有权限编辑本页:
你刚才请求的操作只对属于该用户组的用户开放:
用户
您可以查看并复制此页面的源代码:
'''证明论'''([[英语]]:Proof theory),研究数学证明的[[数学]]理论。[[数理逻辑]]的分支[[学科]],又称'''元数学'''。数学中的证明一向是逻辑学家研究的对象,但证明论是数学家D.[[希尔伯特]]于20世纪初期建立的,目的是要证明公理系统的无矛盾性,希尔伯特提出一整套严格的方案,规定只能用有限长的证明,要无可辩驳地给出整个数学的无矛盾性。他打算先给出公理化的算术系统的无矛盾性,再证明数学分析,集合论的无矛盾性。但1931年,[[K.哥德尔]]证明:一个包含公理化的算术的系统中不能证明它自身的无矛盾性。这就是著名的哥德尔不完备性定理。这个结果使希尔伯特方案成为不可能。但1936年,[[G.根岑]]降低了希尔伯特的要求,允许使用无穷长的证明,证明了算术公理系统的无矛盾性。到1960年,数学分析的一些片断的无矛盾性也被证明。20世纪60年代以后,证明论不再局限于无矛盾性的证明。数学证明中的结构,证明的复杂性,数学中不可判定问题都成为证明论的研究课题,1977年,[[J.帕里斯]]发现算术理论中的一个自然的而又是不可判定的命题,这是一个重大发现。它使算术中自然的不可判定命题的研究越来越受人注意。 古代哲学家[[亚里士多德]]对证明就有过研究。20世纪初,[[D.希尔伯特]]正式创立证明论。以前,要证明非欧几何的无矛盾性,人们把[[非欧几里得几何学|非欧几何]]的无矛盾性化归到[[欧几里得几何学|欧氏几何]])的无矛盾性,再把欧氏几何的无矛盾性通过[[解析几何学|解析几何]])化归到实数论的无矛盾性,又把实数论的无矛盾性化归到自然数论的无矛盾性,最后把自然数论的无矛盾性化归到集合论的无矛盾性。但罗素悖论使集合论出现了矛盾,数学陷入困境。为证明数学的无矛盾性,数学家们展开了激烈的辩论。 在这种情况下,希尔伯特推出他的一整套方案,希望能够从根本上证明数学的无矛盾性(见希尔伯特计划)。希尔伯特提出要把整个数学当作研究对象,需要一种简单明了可靠的元理论来做工具。他要求元语言必须具有有穷性,只承认无穷集合是不断生成的一个过程,不承认存在已经完成的无穷集合。希尔伯特要求用元语言将数学完全形式化、公理化,使数学的推演变成符号的变换。这样只要能够证明从数学公理出发不能推出0≠0来,就可以断定数学没有矛盾了。 希尔伯特计划提出不久,W.阿克曼用这个计划证明,只要对归纳规则加上一点点限制,得到的初等数论就是无矛盾的。这一成果给人们很大希望,沿着希尔伯特指引的方向,希望能够证明不加限制的初等数论无矛盾,再证明数学分析无矛盾,进而证明整个数学无矛盾。 K.哥德尔用这样的思路为初等数论(此处是指被称为皮亚诺算术的一种一阶逻辑系统)的符号编码,使其中每个符号、每个公式和每个公式序列都对应唯一一个编码。每个编码都可以在有限步内找到对应的公式。然而哥德尔却在这样的系统中找到一个命题A,并证明A既不能在系统中被证明,其否定命题(﹁A)也不能被证明。这就是著名的哥德尔第一不完全性定理。利用第一不完全性定理,哥德尔进一步证明,一个形式系统如果含有这种初等数论,并且是无矛盾的,则它的无矛盾性不可能在这一系统内部加以证明。这就是哥德尔第二不完全性定理。见不完全性定理。 哥德尔不完全性定理宣告希尔伯特计划的失败。但希尔伯特仍然是元数学理论的开创者。证明论还是在不断地发展。 ===参见=== *[[数学]] *[[数学基本条目]] [[Category:数学]] [[Category:数理逻辑]] [[Category:中文词典]] [[Category:Z音词语]] [[Category:证]]
返回
证明论
。
导航菜单
个人工具
创建账户
登录
名字空间
页面
讨论
变种
查看
阅读
查看源代码
查看历史
操作
搜索
导航
首页
最近更改
随机页面
工具箱
链入页面
相关更改
特殊页面
页面信息
扫描二维码可以用手机浏览词条