1.3 范式

一阶逻辑等值演算

量词否定等值式

设 A(x) 是含 x 自由出现的公式：

• $\neg \forall xA(x)\iff \exists x\neg A(x)$
• $\neg \exists xA(x)\iff \forall x\neg A(x)$

量词辖域收缩与扩张等值式

设 A(x) 是含 x 自由出现的公式，B 中不含 x 的自由出现：

全称量词

• $\forall x(A(x)\vee B)\iff \forall xA(x)\vee B$
• $\forall x(A(x)\wedge B)\iff \forall xA(x)\wedge B$
• $\forall x(A(x)\to B)\iff \exists xA(x)\to B$
• $\forall x(B\to A(x))\iff B\to \forall xA(x)$

存在量词

• $\exists x(A(x)\vee B)\iff \exists xA(x)\vee B$
• $\exists x(A(x)\wedge B)\iff \exists xA(x)\wedge B$
• $\exists x(A(x)\to B)\iff \forall xA(x)\to B$
• $\exists x(B\to A(x))\iff B\to \exists xA(x)$

量词分配等值式

全称量词对合取的分配

$\forall x(A(x)\wedge B(x))\iff \forall xA(x)\wedge \forall xB(x)$

存在量词对析取的分配

$\exists x(A(x)\vee B(x))\iff \exists xA(x)\vee \exists xB(x)$

前束范式

定义：设 A 为一个一阶逻辑公式，若 A 中的量词均出现在公式的最前面，且它们的辖域一直延伸到公式的末端，则称 A 为前束范式。

前束范式不唯一。

链接到

• 上一个知识点：1.2 等值演算
• 下一个知识点：1.4 推理理论