SEP：可计算性与复杂性（一） (5-2)

在1930年代，也就是远在计算机被发明出来之前,世界各地的数学家发现了关于，“什么是可计算的”这个东西的，精确与独立的定义。丘奇定义了lambda演算(lambda calculus)。哥德尔定义了递归函数(recursive functions)。斯蒂芬克莱尼定义了形式系统(formal systems)。马尔可夫定义了被人们熟知的马尔可夫算法(Markov algorithms)，波斯特与图灵定义了现在被人们熟知的波斯特-图灵机(Post machines and Turing machines)的抽象的机器。

令人惊奇的是，所有这些模型都是精确相等的：所有在lambda演算中是可计算的，在图灵机中也是，并且对于上述所有系统的其他对子来说也都是如此。在此被证明之后，丘奇表示，“原则上可计算”这个直观概念，可以被定义为上述的精确概念。这个信念，现在被称作丘奇-图灵论题(Church-Turing Thesis)，并被数学家们统一接受。

编纂什么是可计算的，的部动力来自于数学家大卫希尔伯特。希尔伯特相信，所有数学都能被精确地公理化(axiomatized)。他认为，一旦做到这一点，我们就将有一个“能行的程序(effective procedure)”，即，一种算法，它将任何一个精确的数学陈述作为输入，经过有限步之后，决定这个数学陈述是正确的还是错误的。希尔伯特现在要的就是，对所有的数学去进行判定的这样一个判定程序(decision procedure)。

作为判定问题的一个特殊的例子，希尔伯特考虑了一阶逻辑的有效性问题(validity problem)，一阶逻辑是一个可以形式化大多数数学陈述的数学语言。任何一个一阶逻辑中的陈述，在任意适合的逻辑结构中，都有一个精确的意义，即，其在任何一个这样的结构中，要么为真要么为假。那些在所有适合的结构中都为真的陈述被称为有效的。那些在某个结构中为真的陈述被称为可满足的(satisfiable)。注意，一个公式φ是有效的，当且仅当，其否定¬φ是不可满足的。

希尔伯特将一阶逻辑的有效性问题称为判定问题(entscheidungsproblem)。在一本希尔伯特与阿克曼所著的教科书上(Principles of Mathematical Logic)有这样写道，“当我们掌握了一个程序，其允许，在有限步的运算中能够判定，任何被给定的逻辑表达式是有效的或者可满足的时，我们就解决了判定问题……而判定问题必须被考虑作数理逻辑的主要问题” (Böerger, Grädel, & Gurevich 1997)。

哥德尔在他1930年的博士论文中，基于罗素与怀特海的《数学原理》(Principia Mathematica)，提出了一阶逻辑的完全公理化。哥德尔证明了他的完全性定理(Completeness Theorem)，即， 一个式子是可由公理证明的，当且仅当其是有效的。哥德尔的完全性定理跨出了朝向解决希尔伯特判定问题的一步。

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。