一阶逻辑等值演算和推理

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

$\neg\forall x A (x) \Leftrightarrow \exists x \neg A (x)$

$\neg\exists x A (x) \Leftrightarrow \forall x \neg A (x)$

若 $A (x)$ 是含 $x$ 自由出现的公式, $B$ 中不含 $x$ 的自由出现,

$\forall x (A (x) \lor B) \Leftrightarrow \forall x A (x) \lor B$

$\forall x (A (x) \land B) \Leftrightarrow \forall x A (x) \land B$

$\forall x (A (x) \to B) \Leftrightarrow \exists x A (x) \to B$

$\forall x (B \to A (x)) \Leftrightarrow B \to \forall x A (x)$

$\exists x (A (x) \lor B) \Leftrightarrow \exists x A (x) \lor B$

$\exists x (A (x) \land B) \Leftrightarrow \exists x A (x) \land B$

$\exists x (A (x) \to B) \Leftrightarrow \forall x A (x) \to B$

$\forall x (B \to A (x)) \Leftrightarrow B \to \exists x A (x)$

$\forall x (A (x) \land B (x)) \Leftrightarrow \forall x A (x) \land \forall x B (x)$

$\exists x (A (x) \lor B (x)) \Leftrightarrow \exists x A (x) \lor \exists x B (x)$

$\exists x (A (x) \to B (x)) \Leftrightarrow \forall x A (x) \to \exists x B (x)$

$\forall$ 对 $\lor$ , $\exists$ 对 $\land$ 无分配律.

指向原始笔记的链接

置换规则
设 $Φ (A)$ 是含有 $A$ 的公式, 若 $A \Leftrightarrow B$ , 则 $Φ (A) \Leftrightarrow Φ (B)$ .
指向原始笔记的链接

换名规则
设 $A$ 为一公式, 将 $A$ 中某量词辖域中个体变项的所有约束出现以及相应的指导变元换成下雨中未出现的个体变项, 所得公式为 $A^{'}$ , 则 $A^{'} \Leftrightarrow A$ .
指向原始笔记的链接

代替规则
设 $A$ 为一公式, 将 $A$ 中某个个体变项的所有自由出现用 $A$ 中未曾出现过的个体变项符号替代, 其他部分不变, 则 $A^{'} \Leftrightarrow A$ .
指向原始笔记的链接

一阶逻辑前束范式
定义设 $A$ 为一个一阶逻辑公式, 若 $A$ 为 $Q_{1} x_{1} ... Q_{k} x_{k} B$ 的形式, 其中 $Q_{i}$ 为 $\forall$ 或 $\exists$ , $B$ 为不含两次的公式, 则称 $A$ 为前束范式.

定理一阶逻辑中的任何公式都存在与之等值的前束范式.
指向原始笔记的链接

一阶逻辑推理
代换实例, 如

$\forall x F (x) \land \exists y G (y) \Rightarrow \forall x F (x)$

基本等值式, 如

$\forall x F (x) \Rightarrow \neg\neg\forall x F (x)$

其他推理定理

$\forall x A (x) \lor \forall x B (x) \Rightarrow \forall x (A (x) \lor B (x))$

$\exists x (A (x) \land B (x)) \Rightarrow \exists x A (x) \land \exists x B (x)$

$\forall x (A (x) \to B (x)) \Rightarrow \forall x A (x) \to \forall x B (x)$

$\forall x (A (x) \to B (x)) \Rightarrow \exists x A (x) \to \exists x B (x)$

$\exists x A (x) \to \forall x B (x) \Rightarrow \forall x (A (x) \to B (x))$

全称指定 US

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

全称推广 UG

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

存在指定 ES

$\exists x A (x) \Rightarrow A (c)$

$c$ 为使 $A (c)$ 为真的客体.

存在推广 EG

$A (c) \Rightarrow \exists x A (x)$

$c$ 为使 $A (c)$ 为真的客体.

指向原始笔记的链接

Notes@Tsukino

探索

一阶逻辑等值演算和推理

一阶逻辑等值式

置换规则

换名规则

代替规则

一阶逻辑前束范式

一阶逻辑推理

关系图谱

反向链接