一阶逻辑的有效性不可判定（判定问题）

父级：first-order-logic

希尔伯特曾要求给出一个算法，能判定任意一个一阶句子是否有效。丘奇和图灵在 1936 年证明了这样的算法不存在。

丘奇–图灵定理（1936）

不存在任何算法，能对任意一个一阶句子判定它是否有效（等价地，判定它是否可满足）。

Proof

将停机问题归约到此。给定一台图灵机 M 和输入 w，可行地构造出一个一阶句子 φ，使其公理化 M 在 w 上的一次运行。用谓词描述这次计算："在时刻 t，纸带第 i 格上写着符号 a"，以及"在时刻 t，读写头处于第 i 格、状态为 q"。将以下几部分合取起来：

初始配置（w 写在纸带上，读写头在起始位置，处于初始状态）；

δ 的每一条转移对应一条蕴含式——"如果时刻 t 的配置是如此这般，那么时刻 t+1 的配置就是这般如此"（读写头之外的格子保持不变）；

"某个时刻到达一个停机状态"。

于是 φ 的一个模型恰好对应一次停机计算，因此 M 在 w 上停机 ⟺ φ 可满足（⟺ 某个对偶句子有效）。若存在判定一阶逻辑有效性的算法，就能用它判定停机——这是不可能的。∎

不可判定，但半可判定

由哥德尔完备性定理可知，有效性是递归可枚举（r.e.）的：枚举所有证明，当且仅当该句子有效时，某个证明会出现。所以你只能确证有效性，永远无法证伪它——这正是 r.e. 世界里单向的半可判定性。

分界线落在哪里

命题逻辑是可判定的（真值表即可；SAT 是 NP 完全的，但仍然可判定）。
完整的一阶逻辑不是——对无穷论域做量化意味着一个无界的搜索，这就是分界点。
有一些片段仍然可判定：一元一阶逻辑、双变量片段、Presburger 算术（只有加法）。要得到不可判定性，需要完整的一阶机器（本质上足以编码一台机器）。

这正是希尔伯特纲领真正在检验的结果，也是图灵造出他那台机器的原因：把"算法"这个概念定义得足够精确，才能证明它不存在。