计算机科学家逻辑/谓词逻辑/等价和范式

等价和范式

公式的等价定义与命题情况相同

定义 6

公式 $F$ 和 $G$ 称为（语义）等价，如果对于 $F$ 和 $G$ 的所有解释 ${\mathcal {I}}$ ， ${\mathcal {I}}(F)={\mathcal {I}}(G)$ 。我们写 $F\equiv G$ 。

命题情况下的等价关系在定理4中成立，此外对于量词我们还有以下情况。

定理 1

以下等价关系成立

$\lnot \forall xF$ $\equiv$ $\exists x\lnot F$

$\lnot \exists xF$ $\equiv$ $\forall x\lnot F$

如果 $x$ 在 $G$ 中不作为自由变量出现

$\forall xF\land G$ $\equiv$ $\forall x(F\land G)$

$\forall xF\lor G$ $\equiv$ $\forall x(F\lor G)$

$\exists xF\land G$ $\equiv$ $\exists x(F\land G)$

$\exists xF\lor G$ $\equiv$ $\exists x(F\lor G)$

$\forall xF\land \forall xG$ $\equiv$ $\forall x(F\land G)$

$\exists xF\lor \exists xG$ $\equiv$ $\exists x(F\lor G)$

$\forall x\forall y\;F$ $\equiv$ $\forall y\forall xF$

$\exists x\exists y\;F$ $\equiv$ $\exists y\exists xF$

证明： 我们只证明等价关系

\forall xF\land G\equiv \forall x(F\land G)

其中 $x$ 在 $G$ 中没有自由出现，例如。假设一个解释 ${\mathcal {I}}=(U,{\mathcal {A}})$ 使得

{\mathcal {I}}(\forall xF\land G)=true

{\text{iff }}{\mathcal {I}}(\forall xF)=true{\text{ and }}{\mathcal {I}}(G)=true

{\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}(G)=true

{\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}_{[x/d]}(G)=true{\text{ (x = does not occur free in = G)}}

{\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}((F\land G))=true

{\text{iff }}{\mathcal {I}}(\forall x(F\land G))=true.

请注意，以下对称情况不成立

$\forall xF\lor \forall xG$ 与 $\forall x(F\lor G)$ 不等价

$\exists xF\land \exists xG$ 与 $\exists x(F\land G)$ 不等价

替代性定理与命题情况一样成立。

**示例：**让我们使用替代性和定理 1 中的等价关系来转换以下公式

(\lnot (\exists xP(x,y)\lor \forall zQ(z))\land \exists wP(f(a,w)))

\equiv ((\lnot \exists xP(x,y)\land \lnot \forall zQ(z))\land \exists wP(f(a,w)))

\equiv ((\forall x\lnot P(x,y)\land \exists z\lnot Q(z))\land \exists wP(f(a,w)))

\equiv (\exists wP(f(a,w))\land (\forall x\lnot P(x,y)\land \exists z\lnot Q(z)))

\equiv \exists w(P(f(a,w))\land \forall x(\lnot P(x,y)\land \exists z\lnot Q(z)))

\equiv \exists w(\forall x(\exists z\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))

\equiv \exists w(\forall x\exists z(\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))

\equiv \exists w\forall x\exists z((\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))

定义 7

令 $F$ 为一个公式， $x$ 为一个变量， $t$ 为一个项。 $F[x/t]$ 是从 $F$ 通过将 $x$ 的所有自由出现替换为 $t$ 而获得的。
注意，这个概念可以重复使用： $F[x/t_{1}][y/t_{2}]$ 以及 $t_{1}$ 可能包含 $y$ 的自由出现。

引理 1

令 $F$ 为一个公式， $x$ 为一个变量， $t$ 为一个项。

${\mathcal {I}}(F[x/t])={\mathcal {I}}_{[x/{\mathcal {I}}(t)]}(F)$

引理 2 (受限重命名)

令 $F=QxG$ 为一个公式，其中 $Q\in \{\forall ,\exists \}$ 且 $y$ 为一个不在 $G$ 中出现的变量，则 $F\equiv QyG[x/y]$

定义 8

如果一个公式中没有变量同时出现于约束和自由状态，并且每个量词之后都是一个不同的变量，则称该公式为 proper 公式。

引理 3 (proper 公式)

对于每个公式 $F$ ，都存在一个公式 $G$ ，该公式为 proper 公式，并且与 $F$ 等价。
证明： 由受限重命名直接得出。
例子

F=\forall x\exists y\;p(x,f(y))\land \forall x(q(x,y)\lor r(x))

有等价的 proper 公式

G=\forall x\exists y\;(p(x,f(y)))\land \forall z(q(z,u)\lor r(z)

定义 9

如果公式具有形式 $Q_{1}\cdots Q_{n}F$ ，其中 $Q_{i}\in \{\forall ,\exists \}$ ，并且在 $F$ 中没有出现量词，那么该公式称为前束范式。

定理 2

对于每一个公式，都存在一个等价的前束范式。
例子

$\forall x\exists y\;(p(x,g(y,f(x)))\lor \lnot q(z))\lor \lnot \forall x\;r(x,z)$

$\forall x\exists y\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \exists x\;\lnot r(x,z)$

$\forall x\exists y\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \exists v\lnot r(v,z)$

$\forall x\exists y\exists v\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \lnot r(v,z)$

证明：通过对公式结构进行归纳，我们可以直接得到原子公式的定理。

$F=\lnot F_{0}$ ：存在一个 $G_{0}=Q_{1}y_{1}\cdots Q_{n}y_{n}G'$ ，其中 $Q_{i}\in \{\forall ,\exists \}$ ，等价于 $F_{0}$ 。因此我们有

$F\equiv {\overline {Q_{1}}}y_{1}\cdots {\overline {Q_{n}}}y_{n}\lnot G'$

其中 ${\overline {Q_{i}}}={\begin{cases}\;\;\,\exists &ifQ_{i}=\forall \\\;\;\,\forall &ifQ_{i}=\exists \end{cases}}$

$F=F_{1}\circ F_{2}$ 其中 $\circ \in \{\land ,\lor \}$ 。存在 $G_{1},G_{2}$ 是正确的预nex 范式，并且 $G_{1}\equiv F_{1}$ 以及 $G_{2}\equiv F_{2}$ 。通过有界重命名我们可以构造

G_{1}=Q_{1}y_{1}\cdots Q_{k}y_{k}G_{1}'

G_{2}=Q_{1}'z_{1}\cdots Q_{l}'z_{l}G_{2}'

其中 $\{y_{1},\cdots ,y_{n}\}\cap \{z_{1},\cdots ,z_{l}\}=\emptyset$ ，因此

F\equiv Q_{1}y_{1}\cdots Q_{k}y_{k}Q_{1}'z_{1}\cdots Q_{l}'z_{l}(G_{1}'\circ G_{2}')

在下文中，我们将正确的预nex 范式公式称为 PP-公式或 PPF。

定义 10

令 $F$ 为一个 PPF。当 $F$ 包含一个 $\exists$ -量词时，进行以下变换

$F$ 有如下形式

\forall y_{1},\cdots \forall y_{n}\exists z\;G

其中 $G$ 是一个 PPF，而 $f$ 是一个 $n$ -元函数符号，它在 $G$ 中不出现。

令 $F$ 为

\forall y_{1},\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})]

如果不存在更多 $\exists$ -量词，那么 $F$ 处于 Skolem 标准型。

定理 3

令 $F$ 是一个 PPF。 $F$ 是可满足的当且仅当 $F$ 的 Skolem 标准型是可满足的。

证明：令 $F=\forall y_{1}\cdots \forall y_{n}\exists z\;G$ ；经过一次按照 while 循环的转换后，我们得到

F'=\forall y_{1}\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})

其中 $f$ 是一个新的函数符号。我们需要证明这种变换是可满足性保持的：假设 $F'$ 是可满足的。那么存在一个模型 ${\mathcal {I}}$ 对于 $F'$ ${\mathcal {I}}$ 是 $F$ 的一个解释。根据模型性质，我们有对于所有 $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}$

{\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}]}(G[z/f(y_{1},\cdots ,y_{n})])=true

根据引理1，我们可以得出结论

{\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true

其中 $v={\mathcal {I}}(f(u_{1},\cdots ,u_{n})$ 。因此，我们有，对于所有 $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}$ ，存在一个 $v\in U_{\mathcal {I}}$ ，其中

{\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true

因此，我们有 ${\mathcal {I}}(\forall y_{1}\cdots \forall y_{n}\exists z\;G)=true$ ，这意味着 ${\mathcal {I}}$ 是 $F$ 的一个模型。

对于定理的反方向，假设 $F$ 有一个模型 ${\mathcal {I}}$ 。那么我们有，对于所有 $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}$ ，存在一个 $v\in U_{\mathcal {I}}$ ，其中

{\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true

令 ${\mathcal {I'}}$ 是一个解释，它只在函数符号 $f$ 上与 ${\mathcal {I}}$ 不同，其中 ${\mathcal {I}}$ 没有定义。我们假设 $f^{{\mathcal {I}}'}(u_{1},\cdots ,u_{n})=v$ ，其中 $v$ 是根据上述等式选择的。

因此，我们有对于所有 $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}'$

{\mathcal {I}}'_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/f^{{\mathcal {I}}'}(u_{1},\cdots ,u_{n})]}(G)=true

根据引理 1，我们得出结论，对于所有 $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}$

{\mathcal {I}}'_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}]}(G[z/f^{(}y_{1},\cdots ,y_{n})])=true

这意味着 ${\mathcal {I}}'(\forall y_{1}\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})])=true$ ，因此 ${\mathcal {I}}'$ 是 $F'$ 的模型。

以上结果可用于将一个公式转换为一组子句，即它的子句范式。

转换为子句范式

给定一个一阶逻辑公式 $F$ 。

将 $F$ 转换为等价的适当 $F_{1}$ ，通过有界重命名。
令 $y_{1},\cdots ,y_{k}$ 是 $F_{1}$ 中的自由变量。将 $F_{1}$ 转换为 $F_{2}=\exists y_{1}\cdots \exists y_{k}\;F_{1}$
将 $F_{2}$ 转换为等价的前束范式 $F_{3}$ 。
将 $F_{3}$ 转换为它的斯科伦范式 $F_{4}=\forall x_{1}\cdots \forall x_{l}\;G$
将 $G$ 转换为其 CNF $G\prime =(\bigwedge _{i=1}^{n}~(\bigvee _{j=1}^{m}~L_{i,j}))$ ，其中 $L_{ij}$ 是一个文字。这将导致 $F_{5}=\forall x_{1}\cdots \forall x_{l}\;G\prime$
将 $F_{5}$ 写成一组子句。

F_{6}=\{C_{1},\cdots ,C_{n}\}

，其中

C_{i}=\{L_{i,1},\cdots ,L_{i,m}\}

问题

问题 6 (谓词)

令 $F$ 为一个公式， $x$ 为一个变量， $t$ 为一个项。则 $F[x/t]$ 表示用 $t$ 替换 $F$ 中每个 $x$ 的自由出现而得到的公式。根据公式 $F$ 的结构，对这个三元函数 $F[x/t]$ 给出形式定义。

$\Box$

问题 7 (谓词)

显示以下语义等价性

$\forall x(p(x)\to (q(x)\land r(x)))\equiv \forall x(p(x)\to q(x))\land \forall x(p(x)\to r(x))$
$\forall x(p(x)\to (q(x)\lor r(x)))\not \equiv \forall x(p(x)\to q(x))\lor \forall x(p(x)\to r(x))$