丘奇—图灵论题与形式化证明

图灵关于可计算理论的工作和希尔伯特关于证明论的工作有某种共同之处：将某种模糊直观的概念赋予一个精确严密的定义。在这一意义上，香农之于信息，冯诺依曼之于博弈，柯尔莫哥洛夫之于概率都有类似的意义。然而，所有类似的工作都面临这样的问题：这些严密的数学定义是否完全把握住了一个直观概念的核心？ 为回应这一问题，丘奇和图灵提出了著名的丘奇—图灵论题：所有能行可计算的函数都是递归（图灵机）可计算的。之所以称为论题，因为这不是一个数学定理——“能行可计算”是一个非数学的直观概念。如果丘奇—图灵论题是正确的，那么“计算”这一直观概念就得到了精确的刻画。 既然仅仅只是一个论题，那么就存在反驳的可能，尤其是对于认为心灵的计算能力胜于计算机的人而言，丘奇—图灵论题并不是显然的。不过，至少有以下三条有力证据使人相信丘奇—图灵论题是正确的： 1.递归（图灵机）可计算的函数确实是直观上能行可计算的。（可靠性） 2.许多有用的，直观上能行可计算的函数，如加法，乘法，幂运算以及超幂运算，还有许多数论函数，都是递归可计算的。（成果丰富） 3.许多从不同动机和角度提出的计算模型，图灵机，λ演算，哥德尔递归函数，波斯特系统，马尔可夫机等，都是等价的。（对象稳定） 与图灵的工作类似，希尔伯特在元数学计划中，也提出了关于“证明”概念的，类似于图灵在计算理论上的论题（不妨称为希尔伯特论题）：一个语句是可证明的，当且仅当，存在一个可公理化的形式演绎系统中该语句的有穷证明序列。这一论题其实带有相当深的形式主义意味，将“证明”看做是符号串的序列变换，这样的想法无法令直觉主义者或有实在论倾向的逻辑主义者（如弗雷格）接受的，但是与丘奇—图灵论题类似，希尔伯特论题也有三个有利证据： 1.一个正确的形式化证明确实可以翻译成直观上合理的数学证明，并且（一阶）逻辑推演可以保证前提逻辑蕴含结论。（可靠性） 2.许多经典数学证明可以被形式化。（成果丰富） 3.许多不同的形式演绎系统，如弗雷格《概念文字》系统，罗素—怀特海《数学原理》系统，希尔伯特系统，费奇式演算，根岑矢列演算等，推演能力上是等价的。（对象稳定） 如果仅有以上三条，那么希尔伯特论题仅仅只是一个直观上合理的论题而已，但是我们现在已经非常习惯将证明看做公式序列，也不再使用希尔伯特“论题”这种说法，正是因为完备性定理的发现： 4.任何被前提Γ逻辑蕴含的结论φ都存在从Γ到φ的有穷演绎序列。（完备性） 因为完备性定理，我们不再问，是否存在形式化证明无法表示的证明过程，因而将证明看做公式序列的做法已经成为了一种惯例。布劳威尔这样的直觉主义者自然可以从哲学角度反驳说，公式序列不“是”数学证明，但对于数学实践而言，“证明”这一概念已经获得了一个清晰的定义，数学家争论的是哪些具体的公理是有问题的（如选择公理），但不会再质疑这套形式化框架本身。 （这里有一种可能的反驳，有些数学家考虑到二阶逻辑具有良好的范畴性质，因而提出不应以一阶逻辑作为推理和证明的基础，而二阶逻辑是不具备完备性的。不过正如蒯因指出的，二阶逻辑其实是隐藏的关于集合的理论，因而不是纯粹逻辑的。） 对比丘奇—图灵论题和希尔伯特对证明的处理，或许可以期待，计算理论中某种类似于完备性定理的命题或许可以使得丘奇—图灵论题成为一个真正意义上的对“计算”的定义。完备性定理的证明之所以是可能的，是因为逻辑推理的直观意义——保持真值——可以在数学中定义，那么对于计算理论而言，它的数学化的直观意义，又会是什么呢？