计算机科学家逻辑/谓词逻辑/Herbrand 理论

Herbrand 理论

到目前为止，我们考虑了谓词逻辑中公式的任意解释。特别是，我们有时使用数字作为解释域和函数，比如加法或后继。在下文中，我们将集中讨论一种特殊情况，Herbrand 解释，并将讨论它们与一般情况的关系。

定义 11

令 $S$ 为一组子句。S 的 Herbrand 域 $U_{H}$ 由以下给出：

• 出现在 $S$ 中的所有常量都在 $U_{H}$ 中（如果 $S$ 中没有出现常量，我们假设一个单个常量，比如 $a$ 存在于 $U_{H}$ 中）。
• 对于每个 n 元函数符号 $f$ 出现在 $S$ 中，以及每个 $t_{1},\cdots ,t_{n}\in U_{H}$，$f(t_{1},\cdots ,t_{n})\in U_{H}$。

示例：给定子句集 $S_{1}=\{P(a),\lnot P(x)\lor P(f(x))\}$，我们构建 Herbrand 域

$U_{H}=\{a,f(a),f(f(a)),f(f(f(a))),\cdots \}$

对于子句集 $S_{2}=\{P(x)\lor Q(x),R(z)\}$，我们得到Herbrand全集 $U_{H}=\{a\}$。

定义 12

设 $S$ 是一个子句集。解释 ${\mathcal {I}}=(U_{\mathcal {I}},A_{\mathcal {I}})$ 是一个Herbrand解释，当且仅当

• $U_{\mathcal {I}}=U_{H}$
• 对于每一个 $n$元函数符号（$n\geq 0$） $f$ 和 $t_{1},\cdots ,t_{n}\in U_{H}$$f^{\mathcal {I}}(t_{1},\cdots ,t_{n})=f(t_{1},\cdots ,t_{n})$
  

注意，对谓词符号的赋值关系没有限制（当然，它们必须是Herbrand全集 $U_{H}$ 上的关系）。

为了讨论谓词符号的解释，我们需要Herbrand基的概念。

定义 13

一个地原子或一个地项是一个不包含变量的原子或项。对于一组子句 $S$，它的 Herbrand 基是地原子集 $p(t_{1},\ldots ,t_{n})$，其中 $p$ 是来自 $S$ 的一个 $n$-元谓词符号，并且 $t_{1},\ldots ,t_{n}\in U_{H}$。

我们将通过简单地给出集合 $I=\{m_{1},m_{2},\cdots ,m_{n},\cdots \}$ 来表示将关系分配给谓词符号，其中每个元素都是一个文字，其原子来自 Herbrand 基。

例子

• $S=\{p(x)\lor q(x),r(f(y))\}$
• $U_{H}=\{a,f(a),f(f(a)),\ldots \}$
• $I=\{p(a),q(a),r(a),p(f(a)),q(f(a)),r(f(a)),\cdots \}$

定义 14

设 ${\mathcal {I}}=(U_{\mathcal {I}},A_{\mathcal {I}})$ 是一个子句集 $S$ 的解释; 与 ${\mathcal {I}}$ 相对应的 Herbrand 解释 ${\mathcal {I}}^{*}$ 是一个满足以下条件的 Herbrand 解释: 设 $t_{1},\ldots ,t_{n}$ 是 $S$ 的 Herbrand 域 $U_{H}$ 中的元素。通过解释 ${\mathcal {I}}$ 每个 $t_{i}$ 都映射到一个 $d_{i}\in U_{\mathcal {I}}$。如果 $p^{\mathcal {I}}(d_{1},\ldots ,d_{n})=true(false)$，那么 $p(t_{1},\ldots ,t_{n})$ 必须在 ${\mathcal {I}}^{*}$ 中被赋值为 $true(false)$。

现在让我们陈述一个简单而显而易见的引理，它将帮助我们关注后续的 Herbrand 解释。

引理 4

如果 ${\mathcal {I}}$ 是子句集的模型，那么与之相对应的每个 Herbrand 解释 ${\mathcal {I}}^{*}$ 都是 $S$ 的模型。

定理 4

一组子句 $S$ 是不可满足的，当且仅当 $S$ 没有 Herbrand 模型。

证明：如果 $S$ 是不可满足的，显然 $S$ 没有 Herbrand 模型。
假设 $S$ 没有 Herbrand 模型，并且 $S$ 是可满足的。那么，存在 ${\mathcal {I}}$ 是 $S$ 的模型，根据引理 4，相应的 Herbrand 解释 ${\mathcal {I}}^{*}$ 是 $S$ 的模型，这与假设矛盾。