判定问题

概述

判定问题（德语：Entscheidungsproblem）是希尔伯特纲领中的核心问题，询问是否存在一种算法能判定一阶谓词逻辑中任意命题的真假。

关键内容

1. 问题定义：
2. 是否存在一种算法（机械方法），以一阶谓词逻辑的一个命题作为输入，能在有限步骤内给出"该命题是普遍有效的"还是"不是"的回答

3. 该问题最初由大卫·希尔伯特在1928年明确提出，是他形式化纲领的一部分

4. 希尔伯特纲领：

5. 目标是将全部数学形式化为一个公理系统，并证明该系统具备三个关键性质：
6. 一致性（Consistency）：系统内部不会推导出矛盾
7. 完备性（Completeness）：系统中的每一个真命题都能被证明

8. 可判定性（Decidability）：存在机械化方法判定任意命题的真假

9. 解决历程：

10. 1931年，哥德尔不完备定理已对希尔伯特纲领造成打击，但未直接解决判定问题
11. 1936年，丘奇使用λ演算首先给出否定回答
12. 几乎同时，图灵在《论可计算数》论文中用图灵机模型独立给出否定回答

13. 图灵的方法更具直观性，因为图灵机直接建模了人类计算行为

14. 理论意义：

15. 否定回答证明了数学推理无法完全机械化
16. 结合哥德尔的不完备定理，彻底终结了希尔伯特纲领
17. 表明存在数学真理，既不能被证明，也无法被机械判定

来源

• 01-turing-on-computable-numbers — 图灵的解决方案
• 论可计算数及其在判定问题上的应用 — 原始论文

相关

• 大卫·希尔伯特 — 提出者
• 阿兰·麦席森·图灵 — 解决者之一
• 停机问题 — 图灵的证明手段
• 图灵机 — 解决工具
• 丘奇 — 独立解决者
• λ演算 — 丘奇的解决工具