柳渝
“真理”与“可证明性” - Jean-Yves Girard
2022-8-17 15:37
阅读:485

对于解读哥德尔不完全性定理,理解真理可证明性以及它们之间的关系是关键。

法国逻辑学家Jean-Yves Girard主持法语翻译哥德尔1931年的原文(Le théorème de Godel,Ernest Nagel, James R. Newman, Kurt Godel, Jean-Yves Girard),在符号领域或还原论的失败一文中,Jean-Yves Girard谈到真理可证明性

一,译文

符号领域或还原论的失败 

- Jean-Yves Girard


1. 真理和可证明性


在下文中,T表示一个未指定的数学理论;哥德尔曾使用Principia System,但现在人们宁愿采取所谓的Peano算术,甚至是集合论。事实上,T的选择对建立程序至关重要;另一方面,对于反驳来说,T允许的抽象方法越多,结果就越有说服力。


如果P是一个可判定的语句,那么 

iP真意味着在T中的形式可证明性。

iiP假意味着在T中的形式可反驳性。


为了验证这一断言,让我们注意到,我们有一个判定P的机械程序。一切机械的东西都是可以形式化的:在T的公理中,只要有一些反映导致判定P的计算的东西就足够了。如果这一论证被认为不具有说服力,我们可以写一个程序,这是用一种具有严格语法的语言来完成的,它在某种程度上是一个形式系统。


现在让Q = x y P(x,y)是一个存在陈述;那么

iii) 如果Q是真的,那么它在T中是可以形式证明的。


事实上,说Q是真的,意味着P(x,y)对于某个选择x=ny=m来说是真的,所以P(n,m)是可以证明的;然后,逻辑规则允许我们在T中形式连接x y P(x,y)


R=xy S(x,y)是一个全称陈述;那么 

iv) 如果T是一致的,并且RT中是可以形式证明的,那么R就是真的。


事实上,R的否定Q是存在的;如果R是假的,那么根据iiiQT中是可以被证明的,而T证明R和它的否定将是矛盾的。


如果没有额外的假设,就不可能说明真和可证明之间的其他一般关系。例如,如果TPeano的算术,T的公理是真的,逻辑规则保留了真,所以T的所有定理都是真的。这种说法的认识论价值是有限的,因为Peano公理的选择正是因为我们相信它们的真理。


也不排除(这也是哥德尔定理所要确定的),一个为真的全称陈述是无法证明的:事实上,这样一个陈述的无限验证过程无法通过形式上的证明来反映,本质上是有限的。


二,原文


Le théorème de Godel 

Ernest Nagel, James R. Newman, Kurt Godel, Jean-Yves Girard


p156


  1. Vérité et prouvabilité


Dans ce qui suit, T désigne une théorie mathématique non spécifiée ; Godel avait utilisé le système des Principia, mais, de nos jours, on prendrait plutôt l’arithmétique dite Peano, voire la théorie formelle des ensembles. En fait, le choix de T aurait été crucial pour établir le programme ; par contre, pour une réfutation, plus T permet de méthodes abstraites, plus le résultat est convaincant.


Si P est un énoncé décidable, alors 


i) la vérité de P implique sa démontrabilité formelle dans T,

ii) la fausseté de P implique sa réfutabilité formelle dans T.


Pour vérifier cette assertion, remarquons que nous disposons d’un procédé mécanique pour décider P. Tout ce qui est mécanique est formalisable : il suffit d’avoir parmi les axiomes de T de quoi refléter les calculs qui mènent à la décision de P. Si cet argument n’est pas jugé convaincant, pension à l’écriture d’un programme, qui se fait au moyen d’un langage à la syntaxe rigide, et qui est bien à sa faon un système formel.


Soit maintenant Q = x y P(x,y) un énoncé existentiel ; alors

iii) si Q est vrai, alors il est formellement démontrable dans T.


En effet, dire que Q est vrai veut dire que P(x,y) est vrai pour un certain choix x=n, y=m, et donc P(n,m) est démontrable ; les règles logiques permettent alors d’enchainer formellement x y y P(x,y) dans T.


Soit enfin R = x y S(x,y) un énoncé universel ; alors 

iv) si T est consistante et si R est formellement démontrable dans T, alors R est vraie.


En effet, la négation Q de R est existentielle; si R était fausse, alors d’après iii) Q serait démontable dans T, et T prouvant R et sa négation serait contradictoire.


Il n’est pas possible - sans hypothèse supplémentaire - d’énoncer d’autres relations générales entre vrai et prouvable. Par exemple, si T est l’arithmétique de Peano, les axiomes de T sont vrais, les règles logiques préservent la vérité, donc tous les théorèmes de T sont vrais. La valeur épistémologique d’une telle remarque est limitée, vu que les axiomes de Peano ont été précisément choisis parce que nous croyons à leur vérité.


Il n’est pas non plus exclu (et c’est ce que va établir le théorème d Godel) qu’un énoncé universel vrai ne sont pas prouvable : en effet, le processus infini de vérification d’un tel énoncé ne peut pas être reflété par une démonstration formelle, finie par essence.


转载本文请联系原作者获取授权,同时请注明本文来自柳渝科学网博客。

链接地址:https://wap.sciencenet.cn/blog-2322490-1351535.html?mobile=1

收藏

分享到:

当前推荐数:1
推荐人:
推荐到博客首页
网友评论0 条评论
确定删除指定的回复吗?
确定删除本博文吗?