[拼音]：zhengminglun

[外文]：proof theory

数理逻辑的一个分支。它最初的目的是想证明数学的协调性，后来逐渐推广到探求一般的公理系统的协调性。数学中使用反证法时需要肯定数学的协调性。在证明欧几里得平行公设不能由别的公理推出时，也就是证明平行公设的独立性时，又需要肯定使用新公设的非欧几何的协调性，这便要求人们对数学的一部分（非欧几何）的协调性作出严格的探讨与证明。这种协调性的证明起初是靠化归方法获得的，即把非欧几何的协调性化归于欧几里得几何的协调性，然后依次化归于实数论的协调性、自然数论的协调性，之后化归于 论的协调性。这是所谓相对协调性的证明。但是， 论的协调性比之自然数论的协调性更不明显，而且由于 论悖论的发现，表明了未经改造的素朴 论也是不协调的。经过改造的严格公理化的 论产生以后，虽然排除了已被发现的悖论，但还不能保证数学理论里不再出现逻辑矛盾，而 论的协调性问题又不能化归于其他数学理论。同时，D.希尔伯特认为在物理世界里是找不到 论的模型的。为了解决这个协调性问题，他于20世纪20年代提出了著名的“希尔伯特方案”。由这个方案产生了证明论。

证明论的根本做法是：把所探讨的理论系统（例如数学）完全形式化，作为研究对象，叫做对象理论。对象理论被当作没有内容的，只是根据一定语法规则由一些被称做字母的基本符号组成的一些符号序列，这些符号序列根据一定变形规则而变化。如果能够导出 A和塡A两个符号序列，指经过解释后表示互相矛盾的两个命题，则说这理论是不协调的；如果无论怎样变形都不能得出这种符号序列，便说这理论是协调的。证明论的目的是探讨怎样的理论是协调的，怎样的理论是不协调的，尤其是要证明，数学作为对象理论是协调的。证明论还涉及到一种被称为元理论的理论，它必须是有内容、有意义的。这样，证明论就有了 3个理论，即：

（1）希望证明其协调性的那个没有形式化的直观的理论。它是有内容有意义的。它不是对象理论，只是对象理论的来源。

（2）对象理论。它是通过把所研究的理论完全形式化而得到的。它被当作没有内容意义的，只是对一些符号序列作各式各样的变形，是研究的对象。

（3）元理论。它是有内容意义的，是用来研究对象理论的，它应尽可能地简单明了，使得人们至少相信它是协调的。元理论可以是第一个理论的一部分，但也可以是另外一个理论。在希尔伯特方案中，为了保证和说明元理论的协调性，至少是使人们相信元理论是协调的，对元理论作了非常严格的要求，要求它满足有穷主义性，从而可以在直觉上保证它是协调的。但是满足有穷主义性的理论，几乎全可以表示在任何一个想证明其为协调的那些内容较为丰富的理论之内。K.哥德尔在1931年证明，要想证明一个理论S的协调性，使用能够表示于S之内的理论是不行的，必须使用不能全部表示于 S之内的理论。这就是说，要证明S的协调性，元理论绝不能表示于S之内。

证明论是数理逻辑发展的产物，又是数理逻辑进一步发展的动力。如果没有数理逻辑的发展，如果未能把数学的各个部门乃至一般理论系统形式化、公理化，就得不到对象理论，也就无法从事证明论的研究。证明论建立以来，已获得一些重要的结果。1924年，德国数学家W.阿克曼证明：如对数学归纳法作一些限制，自然数论是协调的。

在哥德尔1931年的不完全性定理之后，对元理论的要求也放宽了。1936年德国数学家G.根岑证明引用超穷归纳法可以证明自然数论是协调的。这是证明论的较好结果。后来的研究又证明，加以相当限制的实数理论，即加以相当限制的数学分析是协调的。在这些证明中，只有阿克曼在1924年的证明是严格遵守有穷主义的，别的证明由于在哥德尔结果之后，已不限于有穷主义。因为根据哥德尔的结果，满足有穷主义的元理论是相当弱的。但放宽的标准颇不相同，有的尽量少放宽，力图靠近有穷主义；有的则大量放宽，得到了一些结果。

严正声明：本文由历史百科网注册或游客用户丛梦瑶自行上传发布关于» 证明论的内容，本站只提供存储，展示，不对用户发布信息内容的原创度和真实性等负责。请读者自行斟酌。同时如内容侵犯您的版权或其他权益，请留言并加以说明。站长审查之后若情况属实会及时为您删除。同时遵循 CC 4.0 BY-SA 版权协议，尊重和保护作者的劳动成果，转载请标明出处链接和本声明内容：作者：丛梦瑶；本文链接：https://www.freedefine.cn/wenzhan/137373.html