可判定性

在数学和计算机科学中，可判定性（发音为 [ɛntˈʃaɪ̯dʊŋspʁoˌbleːm]，德语为“决策问题”）是 David Hilbert 和 Wilhelm Ackermann 在 1928 年提出的一个挑战。该问题要求一种算法，考虑作为输入， 陈述和回答是或否根据陈述是否普遍有效，即在满足公理的每个结构中都有效。

根据一阶逻辑完备性定理，一个命题普遍有效当且仅当它可以从公理中推导出来，所以可判断性也可以看作是要求一个算法来决定给定命题是否可证明 使用逻辑规则的公理。

1936 年，Alonzo Church 和 Alan Turing 发表了独立的论文，表明不可能通过图灵机可计算的函数（或等价地，可表示为 lambda 演算）。 这个假设现在被称为丘奇-图灵论题。

可判定性的起源可以追溯到 17 世纪的戈特弗里德·莱布尼茨 (Gottfried Leibniz)，他在建造了一台成功的机械计算器之后，梦想建造一台可以操纵符号以确定数学陈述的真值的机器。 他意识到xxx步必须是一种干净的形式化语言，他随后的大部分工作都朝着这个目标迈进。 1928 年，大卫希尔伯特和威廉阿克曼以上述形式提出了这个问题。

在他的计划的延续中，希尔伯特在 1928 年的一次国际会议上提出了三个问题，其中第三个问题被称为希尔伯特的判定性。 1929 年，Moses Schönfinkel 发表了一篇关于决策问题特例的论文，该论文由 Paul Bernays 撰写。

直到 1930 年，希尔伯特还相信不存在无法解决的问题。

在回答这个问题之前，必须正式定义算法的概念。 这是由 Alonzo Church 在 1935 年基于他的 λ 演算提出的有效可计算性概念完成的，第二年由 Alan Turing 提出了他的图灵机概念。 图灵立即意识到这些是等效的计算模型。

1935-36 年，Alonzo Church 给出了“不确定性”的否定答案（Church 定理），此后不久，Alan Turing 于 1936 年独立给出了答案（图灵证明）。 Church 证明了对于两个给定的 λ-演算表达式，不存在决定它们是否等价的可计算函数。 他严重依赖 Stephen Kleene 的早期工作。 图灵将能够解决不确定性的“算法”或“通用方法”的存在问题简化为确定任何给定图灵机是否停止的“通用方法”的存在问题 或不（停止问题）。 如果“算法”被理解为表示可以表示为图灵机的方法，并且对后一个问题的回答是否定的（通常），那么关于可判定性的算法是否存在的问题也必须 是负面的（一般来说）。 图灵在他 1936 年的论文中说：对应于每个计算机器 'it'，我们构造了一个公式 'Un(it)' 并且我们表明，如果有一种通用方法可以确定 'Un(it) ' 是可证明的，那么有一种通用方法可以确定 'it' 是否曾打印过 0。

Church 和 Turing 的工作都深受 Kurt Gödel 早期关于他的不完备性定理的工作的影响，特别是通过将数字（Gödel 编号）分配给逻辑公式以将逻辑简化为算术的方法。

不确定性与希尔伯特的第十个问题有关，该问题要求一种算法来确定丢番图方程是否有解。 由 Yuri Matiyasevich、Julia Robinson、Martin Davis 和 Hilary Putnam 的工作建立的这种算法的不存在，以及 1970 年的最终证明，也暗示了对可判定性的否定回答。

一些一阶理论是算法可判定的； 这方面的例子包括 Presburger 算术、实封闭域和许多编程语言的静态类型系统。 然而，用皮亚诺公理表达的自然数的一般一阶理论不能用算法来决定。

对逻辑公式的类别进行实用的决策程序对于程序验证和电路验证具有相当大的意义。 纯布尔逻辑公式通常使用基于 DPLL 算法的 SAT 求解技术来确定。 线性实数或有理算术上的合取公式可以使用单纯形算法确定，线性整数算术（Presburger 算术）中的公式可以使用 Cooper 算法或 William Pugh 的 Omega 检验确定。