命题逻辑简化

一旦建立了从量化句子推断非量化句子的规则，就有可能将一阶推理简化为命题推理。第一个概念是，正如一个实例化可以替代一个存在量化的陈述，所有潜在实例化的集合可以替代一个全称量化的句子。考虑以下场景：我们的知识库仅包含行

$\forall x \operatorname{King}(x) \wedge \operatorname{Greed} y(x) \Rightarrow \operatorname{Evil}(x)$

$\operatorname{King}(J o h n)$

$\operatorname{Greedy}(J o h n)$

$\operatorname{Brother}(Richard, J o h n)$

然后，利用知识库词汇中所有可行的基本术语替换——在这种情况下， $\{x / J o h n\}$和$\{x / \text { Richard }\}$ — 我们将 UI 应用于第一个短语。我们得到$\begin{aligned} &\operatorname{King}(J o h n) \wedge \operatorname{Greedy}(J o h n) \Rightarrow \operatorname{Evil}(J o h n) \\ &\operatorname{King}(\text { Richard }) \wedge \text { Greedy }(\text { Richard }) \Rightarrow \text { Evil }(\text { Richard }) \end{aligned}$

我们不使用普遍量化的句子。如果地面原子句子—— $\operatorname{King}(J o h n), \text { Greedy }(J o h n)$ ，等等——被视为命题符号，知识库现在基本上是命题的。因此，任何综合命题程序都可以用来得出如下结论： $\operatorname{Evil}(J o h n)$ .

命题化技术可以应用于任何一阶知识库或查询，保留蕴涵。因此，我们有一个全面的蕴涵决策方法……或者我们有吗？有一个问题：当知识库中包含函数符号时，可能的基本术语替换的数量是无限的！如果$Father$知识库中提到了符号，例如，可以创建无限数量的嵌套术语，例如$\text { Father (Father (Father (John))) }$对于无限数量的句子，我们的命题算法会出现问题。

幸运的是，Jacques Herbrand (1930) 证明，如果一个陈述被原始的一阶知识库所暗示，那么它可以仅使用命题知识库的有限部分来证明。我们可以通过使用常量符号生成所有实例来发现子集（ $\text{Richard and John}$ )，那么所有深度为 1 的项$\text{(Father (Richard ) and Father (John ))}$ ，然后是深度为 2 的所有项，依此类推，直到我们可以产生蕴涵句子的命题证明。

我们已经勾勒出一个通过命题化进行一阶推理的完整方法，它可以证明任何蕴涵短语。考虑到大量可想象的模型，这是一项重大成就。但是，在证明完成之前，我们不会知道这句话是否蕴含！如果句子后面没有从句会怎样？有可能确定这一点吗？事实证明，我们不能进行一阶逻辑。我们的证明过程可以无限地继续下去，生成越来越深的嵌套词，但我们不知道它是否被锁定在一个无限循环中，或者证明是否即将出现。图灵机的停机问题与此非常相似。 Alonzo Church (1936) 和 Alan Turing (1936) 都以不同的方式证明了这种情况的必然性。对于一阶逻辑，蕴涵问题是半可判定的，这意味着有算法对每个蕴涵语句都回答是，但没有算法对每个非蕴涵语句说不。