一阶逻辑等值演算和推理

一阶逻辑等值式

定义 设 $A,B$ 是两个谓词公式, 如果 $A\leftrightarrow B$ 是永真式, 则称 $A,B$ 等值, 记作 $A\iff B$.

• $\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$

• $\forall 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)$

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

$\forall$ 对 $\vee$, $\exists$ 对 $\wedge$ 无分配律.

指向原始笔记的链接

置换规则

设 $\Phi (A)$ 是含有 $A$ 的公式, 若 $A\iff B$, 则 $\Phi (A)\iff \Phi (B)$.

指向原始笔记的链接

换名规则

设 $A$ 为一公式, 将 $A$ 中某量词辖域中个体变项的所有约束出现以及相应的指导变元换成下雨中未出现的个体变项, 所得公式为 $A^{\prime }$, 则 $A^{\prime }\iff A$.

指向原始笔记的链接

代替规则

设 $A$ 为一公式, 将 $A$ 中某个个体变项的所有自由出现用 $A$ 中未曾出现过的个体变项符号替代, 其他部分不变, 则 $A^{\prime }\iff A$.

指向原始笔记的链接

一阶逻辑前束范式

定义 设 $A$ 为一个一阶逻辑公式, 若 $A$ 为 $Q_1{x}_1...Q_k{x}_{k}B$ 的形式, 其中 $Q_i$ 为 $\forall$ 或 $\exists$, $B$ 为不含两次的公式, 则称 $A$ 为前束范式.

定理 一阶逻辑中的任何公式都存在与之等值的前束范式.

指向原始笔记的链接

一阶逻辑推理

代换实例, 如

• $\forall xF(x)\wedge \exists yG(y)\Rightarrow \forall xF(x)$

基本等值式, 如

• $\forall xF(x)\Rightarrow \neg \neg \forall xF(x)$

其他推理定理

• $\forall xA(x)\vee \forall xB(x)\Rightarrow \forall x(A(x)\vee B(x))$

• $\exists x(A(x)\wedge B(x))\Rightarrow \exists xA(x)\wedge \exists xB(x)$

• $\forall x(A(x)\to B(x))\Rightarrow \forall xA(x)\to \forall xB(x)$

• $\forall x(A(x)\to B(x))\Rightarrow \exists xA(x)\to \exists xB(x)$

• $\exists xA(x)\to \forall xB(x)\Rightarrow \forall x(A(x)\to B(x))$

• 全称指定 US

  • $\forall xA(x)\Rightarrow A(c)$

• 全称推广 UG

  • $A(c)\Rightarrow \forall xA(x)$

• 存在指定 ES

  • $\exists xA(x)\Rightarrow A(c)$
  • $c$ 为使 $A(c)$ 为真的客体.

• 存在推广 EG

  • $A(c)\Rightarrow \exists xA(x)$
  • $c$ 为使 $A(c)$ 为真的客体.

指向原始笔记的链接