2016年6月1日，《证明方法与理论》的作者张寅生回答了受众关注的关于该专著的一些问题如下。

问：《证明方法与理论》是哪一学科的著作？

答：属于数理逻辑。

问：数理逻辑是属于什么学科？

答：属于数学，是数学的分支。

问：数理逻辑和逻辑是什么关系？

数学与逻辑的交叉产生了数理逻辑。

问：中国的数理逻辑有多久的历史？

答：中国的数理逻辑应以金岳霖引进罗素的《数学原理》为开始，时间大约在20世纪二十年代至三十年代，金岳霖在清华的大学哲学系介绍了数理逻辑，并于1936年出版其著作了《逻辑》，其中介绍了罗素的《数学原理》。

问：数理逻辑对于人工智能有什么意义？

答：非常重要！人工智能理论诞生于数理逻辑。这一点可能并不完全为人所知或接受。

问：为什么说人工智能理论诞生于数理逻辑领域？

答：人工智能理论的核心是图灵机设计思想，也就是计算机的理论模型。计算机首先是一个为解答特定数学问题而设计的装置，这个数学问题就是丢翻图方程整数解求解算法是否存在，即所说的“希尔伯特第十问题”的判定问题。这一问题构成了数理逻辑中的证明论。解决的基本方法是用递归函数的求解，这些方法构成了数理逻辑中的递归论。证明论、递归论、模型论和集合论，这是构成数理逻辑的主要分支。因此，实际上对递归论和证明论直接解决了图灵可计算性的问题。

问：但是计算机系的教育似乎并没有讲解这些数理逻辑与计算机的渊源。

答：这正是计算机教育的一个失误或不当。

问：为什么？

答：如果不知道计算机的理论渊源，就远离了计算机的原理和原创思想。

问：那又怎样？

答：那你就可能只在计算机科学技术的下游活动；很多计算机原创可能与你无缘。

问：举例？

答：比如一个程序员会应用计算机编程语言，但是如果对语言的逻辑问题不清晰，或者对开发语言的上一级语言也就是被开发语言的逻辑工具不熟悉，就不能开发一种计算机语言……

问：开发一种语言和应用一种语言，有什么本质区别吗？

答：有的，形象的说是建筑设计师与建筑工人的区别。对于国家而言，计算机科学技术的发展战略包括基础理论的创新，其中首当其冲包括数理逻辑的创新；对于企业、个人的创新行为而言，数理逻辑的理论和方法是IT战略层面或IT工作指导层面的利器。

问：这么说还是太抽象。比如一个软件企业，技术研发和管理人员的数理逻辑的能力与他们创新活动的能力有什么直接关系吗？难道他们不去看市场调研报告，不去看新型的技术原理和方法，去看数理逻辑教科书吗？

答：三者都要看，“三位一体”（原理、应用、商业模式“三位一体”）才是企业好的知识结构。新兴技术是层出不穷的，发现哪些技术、自己研究开发哪些更有有价值的技术不是随便就可以做到的。数理逻辑是你的显微镜、望远镜，是你的定位坐标，帮助你发现新兴技术的价值。换言之，企业的技术CEO，特别是首席科学家应该把数理逻辑作为自己的基本功和参谋助手。

问：对于一个机器人企业，他们更关注控制技术、传感器件、数值计算，数理逻辑似乎对他们很陌生。

答：如果你不梦想更高的智能，比如机器意识，比如电路级的逻辑创新，那也许你离得开它。

问：请介绍一下《证明方法与理论》。

答：好的。《证明方法与理论》是数学/数理逻辑/证明论学科及其分支的著作，它阐述数学证明的基本原理，主要包括证明方法和证明理论，探讨证明方法和证明理论内在联系和本质特征。在“证明方法”部分，集成了常见或具有重要影响并具有逻辑独立性和形式化特征的数学证明方法。这些证明方法多数人在中学已经多少接触过，比如归纳法，反证法，等等。但是如果问数学证明方法一共有多少种呢？这个问题就很难回答了。

问：难在哪里？

答：首先，需要有一个“数学证明方法”的定义，然后才能以这个定义所确定的标准，搜集、分类、命名数学证明方法。

问：难道以前的数学都没有对数学证明下定义，进行分类、归纳吗？

答：有的，哥德尔和希尔伯特都给数学证明做了定义，他们为数学证明下的定义是，数学证明是命题的逻辑推导序列，最后指向证明结论。

问：《证明方法与理论》之前的学术界对数学证明方法的归纳整理情况怎样？

答：实际上对于数学证明方法的分类和归纳进展的很慢，工作不多。

问：为什么会是这样？

答：根据哥德尔和希尔伯特的定义，数学证明方法应该是独特的证明序列的抽象，也就是数学证明的逻辑形式化，但是这个形式化的工作几乎没有做。也许这与数学证明方法的学科分类有关，证明论研究证明的理论，即证明的内容本身，而证明的形式化是方法表示------理论与方法并不是一回事。质言之，证明方法被放置于“数学基础”分支。

问：好奇怪，为什么证明的内容属于证明论，而证明的形式就在另外一个学科分支？

答：是的，一般把证明方法列为数学的“数学基础”分支。这样有不合理之处，即理论与方法实际上是一体的，却列为不同领域研究，容易割裂其内在联系。实际上，证明论的创立者希尔伯特曾希望将证明方法列为证明论研究范畴。大家熟知希尔伯特在1900年的世界数学家大会上提出了著名的23个数学问题，实际上还有第24个数学问题，即证明论中的数学证明方法的研究。最近发现了他的手稿，不过实际上他不知什么原因在讲演时删除了这个问题。

问：《证明方法与理论》对于数学证明方法做了哪些工作？

答：根据希尔伯特和哥德尔对数学证明的定义，《证明方法与理论》集成了具有重要影响的数学证明方法。然后，把这些方法都进行了形式化，也就是把这些方法都写成了数学公式。

问：根据你的这些工作，数学证明方法被归纳成多少种？

答：11种（类）：①关系运算证明方法；②三段论证明方法；③数学归纳法；④反证法；⑤构造性证明方法；⑥同态证明方法；⑦解释性证明方法；⑧系统化证明方法；⑨截消证明方法；⑩归结证明方法；⑪自动化证明方法。

问：这些方法与以往的数学证明方法的分类有什么不同？

答：这个分类与集成在某种意义上是对数学证明方法最多的一次集成。虽然也有少量的著作所列的数学证明方法数量超过《证明方法与理论》，但是就我个人看来，《证明方法与理论》之前的著述所提及的很多证明方法是可以合并的，同时以往著述的很多证明方法不能形式化，因而不在一个分类层面。这样《证明方法与理论》在当前应该是在具有逻辑独立性和形式化特征意义上集成了最多的数学证明方法，它基本上包括了普遍接受的数学证明方法，如归纳法，也有近年出现不久的数学证明方法，如解释性证明方法，也包括机器自动证明的方法，命名为自动化证明方法------这个方法对自动证明的各种技术性证明方法做了理论抽象，涵盖了各种计算机自动证明的方法形式。就同类论著比较而言，《证明方法与理论》就作者所知晓的国际研究前沿而言，基本上包括了当前国际国内数学证明方法论述提及的各种数学证明方法。在书中，列出了《证明方法与理论》与国际上对数学证明方法研究，特别是方法归类研究的对比情况。

问：那么在“证明理论”方面，《证明方法与理论》都讲了什么？

答：“证明理论”部分阐述了自希尔伯特倡导建立证明论以来该学科的主要理论，将这些理论归纳为6个理论体系：①可判定性理论，②相容性理论，③（不）完备性理论，④可靠性理论⑤为数学证明而构建的支持性或辅助性理论和⑥证明复杂性理论。这也就是前面说到的人工智能的肇始理论。

问：这6项理论是如何确定的？是你的归纳和分类，还是已有定论？

答：如何把百年以来的证明论抽象出第一级的分类结构确实是很重要的问题，它涉及对证明论的体系结构的理解。当前的比较普遍接受的证明论结构是上面所说的①可判定性理论，②相容性理论，③完备性理论和不完备性理论，⑥证明复杂性理论；至于④可靠性理论和⑤为数学证明而构建的支持性或辅助性理论是我提出来的。

问：提出的依据是什么？

答：对于④可靠性理论，主要地由于散见于多个领域而没有独立提出，因此在逻辑上将证明的可靠性理论列为证明论的一级结构是逻辑和历史的必然结果。至于⑤为数学证明而构建的支持性或辅助性理论，如果没有这个一级结构，某些重大的证明论成果就不能列入其中，如几何定理自动证明很多人列为几何学的进展，但不视为是证明论领域的进展，如《中国大百科全书》的“证明论”词条就是这样。实际上关于几何定理自动证明的贡献不光是在几何学领域，它将几何对象转化为代数的方法使得几何的证明广义化（抽象化）为数学证明的方法，是通用的数学证明思想和方法，因此《证明方法与理论》增补了一部分结构，即描述证明的支持性理论或辅助性理论，例如将几何对象转换为代数对象使得用通用的证明方法能够证明专门的几何问题。

问：对于这6项理论，你的专著做了什么？

答：系统性地介绍、评介了前4种证明理论，介绍了理论的基本内容、历史背景、主要观点、形式化表达和应用，以及当前研究的国际前沿。

问：举例说明一下吧！前沿的东西在哪里？

答：比如对于逆推数学的介绍。逆推数学在国内还没有系统介绍。《证明方法与理论》介绍了逆推数学的最新研究成果，作为公理化思想的近年来的进展，包括1984年获 Alan T. Waterman 奖Harvey Friedman的逆推数学成果。逆推数学是希尔伯特纲要提出以来对于数学公理化运动的最新成果，它的令人吃惊之处在于，它在哥德尔第一不完备性定理之后，通常理解为不可能构建完备的数学公理系统的观点之后，依据歌德尔第二不完备性定理提出的数学公理体系结构。

问：那么你的主要工作就是对这些数学证明方法和理论的分类、抽象和集成吗？

答：我想除了这些工作还有一部分我作为数学方法的提出者所做的工作。

问：你指什么？

答：对三段论数学证明方法的协调化、经典化和自动化。

问：三段论是很悠久的证明方法，早有定论和无数的介绍，还有什么研究的前途和意义吗？

答：有的。实际上三段论作为人类的基本推理形式，其中有矛盾之处，也就是不协调性，这以前没有从根本上提出，也没有得到证明和解决。在我的三段论研究成果中提出了三段论数学证明方法协调化，也就是剔除矛盾的方法。

问：三段论的这些问题-------如果存在的化，是你发现并提出来的吗？

答：围绕三段论的一些不能解释的问题已经有人提出了一些。例如，对于三段论形式的图表示，有人认为欧拉的表示是错误的，如当代法国科学家Keith Stenning和Micheal Van Lambalge提出：为什么欧拉这样的大数学家犯此低级的错误（“How could a brilliant mathematician like Euler make such a fundamental mistake”，Keith Stenning, Micheal Van Lambalgen.Human Reasoning and Cognitive Science,The MIT Press,2008:302~303）。同时，Keith Stenning和Micheal Van Lambalge还认为，用格尔刚（Gergonne，法国数学家）图的方法解三段论因其过多的图组合方案可能无解。此外，英特尔公司的总工程师在总结三段论自动推理时也提出过类似问题，即当前对亚里士多德三段论的解释是否符合亚里士多德愿意，三段论能否经典化（用类似逻辑标准语言的一阶逻辑语言表示）都是悬而未决的（John Harrison. Handbook of Practical Logic and Automated Reasoning.Cambridge University Press.2009）。但是这些问题的提出者都没有明确提出和证明三段论形式本身有不协调性。我的研究明确提出和证明了三段论形式本身的不协调性，并对Keith Stenning和John Harrison提出的上述未解问题给与了一个解答。

问：解答的结果如何？

答：研究的结果解决了三段论的不一致性问题，也就是不协调性问题，同时实现了三段论的经典化（用一阶语言表示）和自动化（可以用通用的逻辑编程语言自动推导和证明）。这些工作不仅表述在《证明方法与理论》，还表述在作者的另一部著作《扩展的三段论及自动推理》（科学技术文献出版社，2009年）。这个工作是一个持续性的研究工作，包括在作者在清华大学博士后期间在蔡曙山教授的指导下完成的研究工作。

问：那么你的三段论研究的意义是什么?

答：三段论是人类重要的推理形式之一，自亚里士多德建立以来一致作为常识和定论被接受和传承，并且作为法律的教科书的内容加以确定。期间虽有不可理解的问题发现，但都没有提出和证明其存在不协调性。发现和证明三段论的不协调性是对基本证明方法缺陷的一个发现和修正，应该是一个重要的推理方法、逻辑和思维形式上的原始创新。

问：最后，请说一下，《证明方法与理论》的出版有什么意义？

答：我想这是对数学证明方法与理论的一个系统总结。它将从思维方式、科学史的角度审视数学证明的发展脉络和研究前沿，力图为证明论发展做了一个系统阐释，同时也有作者自己独立的证明方法和理论创新，相信这对证明论的研究是有益的。

（2016年6月）