令人不安的哥德尔证明 - 倡议重读哥德尔1931年论文

美国最大出版社诺顿公司在介绍2021年出版的哥德尔传记“理性的边缘之旅 - 库尔特-哥德尔的一生”（Stephen Budiansky）时说 [1] ：

  • 这是第一本为普通读者撰写的关于这位逻辑学家和数学家的重要传记，他的不完备性定理帮助发起了一场现代科学革命。库尔特-哥德尔（Kurt Gödel）的著名证明，即每个数学系统都必须包含“为真但不可证明的命题”——在发表后的近一百年里，继续令数学、哲学和计算机科学感到不安。

此说并不夸张，那么哥德尔不完备性定理中到底有什么令人至今不安？如果我们仔细观察，就会发现这种不安并不是因为哥德尔给出的形式系统不完备性的结论，也不是因为哥德尔在证明中运用了“说谎者悖论”，而是哥德尔将”自己说自己是不可证明的“说谎者悖论命题当作形式系统中正常的“不可判定命题”了，由此得出形式系统中存在如说谎者悖论的命题是常态！[2] 


哥德尔的证明自发表以来一直受到挑战，道森（John W. Dawson Jr. ）在文章“哥德尔不完备性定理的接受情况（The reception of Gödel's Incompleteness Theorems）”中对此进行了梳理 [3] （p.74-95）：

  • 策梅洛（Ernst Zermelo）在1931年写给哥德尔的信中说，哥德尔对不可判定命题存在性的证明存在一个“essential gap”；
  • 逻辑学家佩雷曼（Chaïm Perelman）断言，哥德尔发现的实际上是一个二律背反（Antinomy）；
  • 维特根斯坦（Ludwig Wittgenstein）对哥德尔的证明发表了备受争议的评论（Remarks on the Foundations of Mathematics，1938)；
  • 罗素（Bertrand Russell）在给亨金（Leon Henkin）的信中表达了他的深刻困惑：我当然意识到哥德尔的工作具有根本的重要性，但我对它感到困惑。[……] 如果一个给定的公理集导致矛盾，很明显，至少有一个公理必须是错误的。

。。。


还有埃尔布朗（Jacques Herbrand）在1931年写给哥德尔的信中指出 [4]  (p.3-14)，哥德尔证明中的形式系统不能表达如Ackermann那样的非原始递归函数。


更有待人们重新认识的图灵（Alan Turing）关于Entscheidungsproblem的证明（1936）[5] ，其中图灵提到康托尔对角线法隐藏着“不恰当预设”，并大胆地对其进行了修正。


哥德尔的证明所造成的不安在人文学科中 [1] [6-8] ，甚至在人文学科与自然科学的碰撞中，不断被探讨，如物理学家索卡尔制造的“索卡尔的骗局” [9] ；人类学家保罗-乔里昂（Paul Jorion）从知识人类学的角度对哥德尔证明的质疑 [10] ，。。。


但是在数学逻辑领域，对哥德尔的证明所造成的不安，如今人们采取几近回避的态度。比如，法国逻辑学家吉拉尔（Jean-Yves Girard）在其书“盲点，逻辑课程 — 迈向完美”中（第二章 不完全性定理）中说 [11] ：

  • 探讨哥德尔定理的技术奥秘是不可能的，原因有几个：此结果，基本上很简单，但只能像看莫奈的老画一样，保持一定距离观看；靠近看，只是繁琐的细节，人们不一定想知道，。。。我们也不需要，因为这个定理是一个科学的死胡同：它指向一个死胡同。既然那里没有什么可找的，那么成为哥德尔定理的专家就没有意义了。

我们倡议重读哥德尔1931年的论文，深入哥德尔的原始证明，超越思想的局限去观察，共同面对令人不安的哥德尔证明。我们认为，在当今充满危机的时代，渴望真相，探寻真相，是化解不安的最根本的途径。在此意义上，解读哥德尔，也是在解读我们自己，。。。

参考文献：

[1] Stephen Budiansky, Journey to the Edge of Reason - The Life of Kurt Gödel (2021). https://wwnorton.com/books/9781324005445/overview

[2] Godel, On Formally Undecidable Propositions of Principia Mathematica and Related Systems, translated by Bernard Meltzer :  

https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Undecidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf

[3] S.G. Shanker (ed.), Gödel’s Theorem in Focus, Croom Helm 1988, https://pdfslide.net/documents/godels-theorem-in-focus-philosophers-in-focus.html

[4] Kurt Gödel: Collected Works: Volume V, Volume 5

https://books.google.fr/books?id=4rTYxQEACAAJ&printsec=copyright&redir_esc=y#v=onepage&q&f=false

[5] Alan Turing, « On Computable Numbers, with an Application to the Entscheidungsproblem », https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf

[6] Rebecca Goldstein, Incompleteness: The Proof and Paradox of Kurt Gödel）: https://www.essra.org.cn/upload/202102/Incompleteness%20-%20The%20Proof%20and%20Paradox%20of%20Kurt%20Godel%20by%20Rebecca%20Goldstein%EF%BC%882005%EF%BC%89.pdf

[7] Pierre Cassou-Noguès, Les Démons de Gödel - Logique et folie (2007). https://www.amazon.fr/D%C3%A9mons-G%C3%B6del-Logique-folie/dp/2020923394

[8] James R Meyer, The shackles of conviction. Paperback (2022). https://www.amazon.com/Shackles-Conviction-James-R-Meyer/dp/1906706093

[9] https://fr.wikipedia.org/wiki/Affaire_Sokal

[10] Paul Jorion, Comment la vérité et la réalité furent inventées (Gallimard 2009). https://www.gallimard.fr/Catalogue/GALLIMARD/Bibliotheque-des-Sciences-humaines/Comment-la-verite-et-la-realite-furent-inventees

[11] Jean-Yves Girard , Le Point Aveugle, Cours de Logique - Vers la perfection. http://recherche.ircam.fr/equipes/repmus/mamux/hermann.pdf



Commentaires

Enregistrer un commentaire

Posts les plus consultés de ce blog

图灵谁如何定义“可计算性”的？

  I. How did Turing define the computability? Turing's 1936 paper, as its title suggests:  On Computable Numbers, with an Application to the Entscheidungsproblem , aimed to solve the  Entscheidungsproblem  proposed by Hilbert based on c omputable numbers .   Turing answered the Entscheidungsproblem negatively, Turing said: I propose, therefore, to show that there can be no general process for determining whether a given formula A of the functional calculus K is provable (Note: K refers to the first-order predicate), i.e. that there can be no machine which, supplied with any one A of these formulae, will eventually say whether A is provable. Therefore, Turing gave a definition of  decision problem  such that «  there is a general process for determining . . . ».   1. Decision problem     Turing said ([ 1], Section 8) : The expression ''there is a general process for determining . . .'' has been used throughout this section ...
Lire la suite

停机问题（3）- 证明溯源

  There are two versions of the popular proof of the "haling problem": one based on the liar's paradox and the other based on the Cantor’s diagonisation. The academic claims that the halting problem and its proofs are originated from Turing's 1936 paper, which is highly questionable, … Roger Penrose gave an accessible presentation of the proof of the halting problem based on the Cantor’s diagonisation in  The Emperor's New Mind , and I excerpt the relevant content as follows (p.59-64) : A natural question arises: how are we to decide whether or not any particular Turing machine (when fed with some specific input) will ever stop?  … So, is there some algorithmic procedure for answering the general question - the halting problem - completely automatically?  Turing showed that indeed there is not. His argument was essentially the following.  We first suppose that, on the contrary, there is such an algorithm. Then there must be some Turing machine H which 'decides...
Lire la suite