[敬请读者注意] 本人保留本文的全部著作权利。如果哪位读者使用本文所描述内容，请务必如实引用并明白注明本文出处。如果本人发现任何人擅自使用本文任何部分内容而不明白注明出处，恕本人在网上广泛公布侵权者姓名。敬请各位读者注意，谢谢！

准确地理解哥德尔不完全性定理“关于PM及相关系统的形式不可判定命题”(5) - 一些相关事实

程京德

本文介绍和说明与“哥德尔不完全性定理”相关的一些事实。

哥德尔证明的两个重要定理的原始陈述如下 [1-7]：

命题IX(“第一不完全性定理”)：在命题VI中言及的所有形式系统中，都存在有受限谓词演算的不可判定问题（亦即，受限谓词演算的逻辑式，其普遍有效性以及其反例的存在性都不可证）。

命题XI(“第二不完全性定理”)：如果c是一个给定的递归且一致的逻辑式类，则表达“c是一致的”之内容的命题逻辑式不是c-可证的；特别地，P的一致性在P中不可证，在假设P是一致的前提下（如果不是，那么当然，任何言明都是可证的）。

哥德尔的两个重要定理都是否定性定理。下面，笔者介绍和说明与这两个定理所否定的性质（亦即，可判定性、完全性、一致性、希尔伯特计划）相关的一些事实。

[对于数理逻辑中形式系统/理论的概念不熟悉的读者，在阅读下面内容之前，最好先阅读一下笔者的科普文章 [8]。]

皮亚诺算术一致性的可证明性及希尔伯特计划

如同笔者在本系列前面文章所述，哥德尔工作的原本目的是试图实现希尔伯特计划，证明皮亚诺算术(Peano Arithmetic)的一致性 [9,10]。

哥德尔的命题XI(“第二不完全性定理”)否定了希尔伯特计划以有穷方法论限制下的、基于经典数理逻辑的形式化方法证明皮亚诺算术的一致性的可能。

但是如同笔者在本系列前面文章中已经说明过的，“在一个形式系统/理论内部不可能找到一个表达其一致性的目标定理的形式证明，并不意味着也必定找不到一个表达其一致性的元定理的元证明（未必是形式化的，未必遵循有穷观点和方法）”。另外，还有在什么前提条件下“不可能找到”的问题，换了前提条件，就未必是“不可能找到”了。

实际上，在希尔伯特学派放宽了对有穷观点和方法的限制之后，德国数理逻辑学家根岑(Gerhard Gentzen，1909-1945)就在1935-1936年用超穷归纳法(transfinite induction)证明了一阶皮亚诺算术的一致性 [9-12]。

针对希尔伯特计划的最初贡献是希尔伯特的学生阿克曼(Wilhelm Ackermann, 1896-1962)在其博士学位论文中做出的，阿克曼于1924年（在有穷方法论限制下）“证明”(后被发现有缺陷)了不含归纳公理模式的皮亚诺算术的一致性；在哥德尔和根岑的工作之后，阿克曼于1940年给出了一阶皮亚诺算术的另外一个一致性证明，和根岑一样，也使用了超穷归纳法 [9,10,13-15]。

另外，K. Schütte 于1951年，I. N. Khlodovskii (И. H. Хлодовскпй) 在1959年，也都给出了皮亚诺算术一致性的另外的证明 [10,16-18]。

笔者在这里还必须介绍的一个重要事实是：澳大利亚相关逻辑学家迈耶(Robert K. Meyer)于2021年证明了一个重要且有趣的结果，以一阶谓词相关逻辑 RQ 作为基础逻辑形式化的一阶相关皮亚诺算术系统 R# (the system R# of first-order relevant Peano arithmetic)，表达其一致性的命题是该系统内的一个形式可证目标定理 [19-21]。

迈耶本人声称，“这篇论文废除了哥德尔著名的第二定理。(就是那个断言足够强大的系统不足以证明自己的一致性的定理。) (this paper repeals Gödel’s famous second theorem. (That’s the one that asserts that sufficiently strong systems are inadequate to demonstrate their own consistency.))” “这个定理(或者至少是它通常所宣称的意义)是一个错误 -- 也许，一个微妙的、可以理解的错误，但仍然是一个错误。(That theorem (or at least the significance usually claimed for it) was a mistake — a subtle and understandable mistake, perhaps, but a mistake nonetheless.)” [21]。但是迈耶的主张显然言过其实而并不能成立，因为算术形式化所使用的基础逻辑完全不同。

另一方面，或许是更重要的方面，我们当然也可以并且应该从迈耶的工作成果认识到：第一，算术形式化所基于的基础逻辑系统的选择是件多么重要的事情；第二，希尔伯特计划坚持有穷方法论限制仍然是可行的，但是需要更换算术形式化的基础逻辑；第三，条件句的表达和刻画是任何形式逻辑系统的核心，在条件句的表达和刻画上远比经典数理逻辑合理的相关逻辑应该在许多应用上表现出优于经典数理逻辑的特性。

形式系统/理论的完全性与可判定性 

波兰(犹太)数理逻辑学家 Mojżesz Presburger(1904-1943) 于1929年证明了，只定义了加法而没有定义乘法的一阶形式算术（通常称为“Presburger算术”）是完全的并且是可判定的 [22,23]。 

挪威数理逻辑学家斯科伦(Thoralf Albert Skolem, 1887-1963) 于1930年证明了，只定义了乘法的一阶形式算术是完全的并且是可判定的 [22,24]。 

波兰裔美国数理逻辑学家塔斯基(Alfred Tarski, 1901-1983)于1930-1931年用量词消去法证明了定义了加法和乘法的一阶形式实数理论是完全的并且是可判定的 [22,25,26]。塔斯基还证明了一阶形式欧几里得几何理论是完全的并且是可判定的 [22,25,26]。 

在本系列前面文章中介绍过，哥德尔在1929年的博士论文工作证明了经典数理逻辑一阶谓词演算的完全性（“哥德尔完全性定理”）[27]；美国数理逻辑学家丘奇(Alonzo Church, 1903-1995)于1936年证明了⼀阶谓词演算的不可判定性 [28]。 

1953年，塔斯基及其合作者证明了一些形式数学理论（比如， 群论、格论、射影⼏何等）的不可判定性 [22,29]。

参考文献

[1] K. Gödel, “über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I,” Monatshefte für Mathematik Physik, Vol. 38, pp. 173–198, 1931. (The summary of the results of this work, published in Anzeiger der Akad. D. Wiss. In Wien (math.-naturw. Kl.) 1930, No. 19.) English Translation: B. Meltzer (Translation) and R. B. Braithwaite (Introduction), K. Gödel, “On formally undecidable propositions of Principia Mathematica and related systems I,” Basic Books, 1962, Dover Publications, 1992. 

[2] K. Gödel, “Some metamathematical results on completeness and consistency, On formally undecidable propositions of Principia Mathematica and related systems I, and On completeness and consistency”(1930b, 1931, and 1931a), in J. van Heijenoort (Translation, Ed.), “From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931” pp. 592-617, Harvard University Press, 1967, “Frege and Gödel: Two Fundamental Texts in Mathematical Logic,” pp. 83-108, Harvard University Press, 1970.  

[3] K. Gödel, “Einige metamathematische Resultate über Entscheidungsdefinitheit und Widerspruchsfreiheit”(1930b) “Some metamathematical results on completeness and consistency,”(1930b), pp. 140-143, “über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I,”(1931) “On formally undecidable propositions of Principia Mathematica and related systems I,”(1931), pp. 144-195, “über Vollständigkeit und Widerspruchsfreiheit,”(1932b) “On completeness and consistency,”(1932b), pp. 234-237, Translated (by J. van Heijenoort) and Repringted in S. Feferman, et al. (Eds.), “Kurt Gödel: Collected Works, Volume I, Publications 1929-1936,” Oxford University Press, 1986.  

[4] 程京德,“准确地理解哥德尔不完全性定理‘关于PM及相关系统的形式不可判定命题’（1）- 背景及内容”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2024年6月26日。

[5] 程京德,“准确地理解哥德尔不完全性定理‘关于PM及相关系统的形式不可判定命题’（2）- 理论基础及有效范围”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2024年6月30日。

[6] 程京德,“准确地理解哥德尔不完全性定理‘关于PM及相关系统的形式不可判定命题’（3）- 意义”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2024年7月3日。

[7] 程京德,“准确地理解哥德尔不完全性定理‘关于PM及相关系统的形式不可判定命题’（4）- 误解误用的一般性原因”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2024年7月8日。

[8] 程京德，“形式理论：将形式逻辑系统应用于具体对象领域的逻辑基础”，微信公众号“数理逻辑与哲学逻辑”，2023年1月30日，科学网博客，2023年2月9日；“形式理论：将形式逻辑系统应用于具体对象领域的逻辑基础（增补版）”，微信公众号“数理逻辑与哲学逻辑”，2023年4月17日。

[9] R. Zach, “Hilbert’s Program,” The Stanford Encyclopedia of Philosophy, Center for the Study of Language and Information (CSLI), Stanford University, 2003-2023. 

[10] R. Murawski, “On Proofs of The Consistency of Arithmetic,” Studies in Logic, Grammar and Rhetoric 5 (18), pp. 41-50, 2002. 

[11] G. Gentzen, “Die Widerspruchsfreiheit der reinen Zahlentheorie,” Mathematische Zeitschrift, Vol. 112，pp. 493-565, 1936. English Translation： G. Gentzen, “The Consistency of Arithmetic,”in M. E. Szabo (ed.), “Collected Papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics,” pp. 132-213, North-Holland, 1969. 

[12] 王宪钧, “数理逻辑引论 第三篇 数理逻辑发展简述”，北京大学出版社, 1982年,1998年。

[13] W. Ackermann, “Begrϋndung des ‘tertium non datur’ mittels der Hilbertschen Theorie der Widerspruchsfreiheit,” Mathematische Annalen, 93, pp. 1-36, 1924. 

[14] W. Ackermann, “Zur Widerspruchsfreiheit der Zahlentheorie,” Mathematische Annalen, 117, pp. 162-194, 1940.

[15] H. Hermes “In memoriam WILHELM ACKERMANN 1896-1962,” Notre Dame Journal of Formal Logic, Vol. 8, No. 1-2, pp. 1-8, 1967.

[16] K. Schütte, “Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie,” Mathematische Annalen, Vol. 122, pp. 369-389, 1951. 

[17] K. Schütte, “Beweistheorie,” Springer-Verlag, 1960. English translation: “Proof Theory,” Springer-Verlag, 1977. 

[18] I. N. Khlodovskii (И. H. Хлодовскпй), “A New Proof of the Consistency of Arithmetic (НОВОЕ ДОКАЗАТЕЛЬСТВО НЕПРОТИВОРЕЧИВОСТИ АРИФМЕТИКИ),” Uspekhi Mat. Nauk, Vol. 14, Issue 6, pp. 105-140, 1959. 

[19] R. K. Mayer, “Relevant Arithmetic (Abstract),” Bulletin of the Section of Logic, Vol. 5/4, pp. 133-137, 1976; Australasian Journal of Logic, Vol.18, No. 5, pp. 150-153, 2021. 

[20] H. Friedman and R. K. Mayer, “Whither Relevant Arithmetic?” The Journal of Symbolic Logic, Vol. 57, No. 3, pp. 824-831, 1992. 

[21] R. K. Mayer, “The Consistency of Arithmetic,” Australasian Journal of Logic, Vol. 18, No. 5, pp. 289-379, 2021. 

[22] P. Raatikainen, “Gödel’s Incompleteness Theorems,” The Stanford Encyclopedia of Philosophy, Center for the Study of Language and Information (CSLI), Stanford University, 2013-2020. 

[23] M. Presburger, “über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt,” Sprawozdanie z I Kongresu Matematyków Sn Krajów Slowiańskich, (= Comptes-rendus du I Congrès Mathématiciens des Pays Slaves), Warsaw, pp. 92–101, 1929;  English translation: “On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation,” History and Philosophy of Logic, Vol. 12, No. 2, pp. 225-232, 1991.

[24] T. Skolem, “über einige Satzfunktionen in der Arithmetik,” Skrifter utgitt av Det Norske Videnskaps-Akademi i Oslo, I, No. 7, pp. 1-28, 1930. 

[25] A. Tarski, “Sur les ensembles définissables de nombres réels I,” Fundamenta Mathematica 17, pp. 210-239, 1931. 

[26] A. Tarski, “A Decision Method for Elementary Algebra and Geometry,” Santa Monica CA, 1948. 

[27] K. Gödel, “Die Vollständigkeit der Axiome des logischen Funktionenkalküls,” Monatshefte für Mathematik und Physik, Vol. 37, pp. 349-360, 1930. 

[28] A. Church, “An Unsolvable Problem of Elementary Number Theory,” American Journal of Mathematics, Vol. 58, Issue 2, pp. 345-363, 1936. 

[29] A. Tarski, A. Mostowski, and R. M. Robinson (Eds.), “Undecidable Theories,” Elsevier, 1953.  

微信公众号“数理逻辑与哲学逻辑”