谓词演算的推理理论

1. UI(全称量词消去规则)：\forall xA(x)\Rightarrow A(x)
2. EI(存在量词消去规则)：\exists xA(x)\Rightarrow A(c)
3. UG(全称量词引入规则)：A(y)\Rightarrow \forall x A(x), y 为任意值，A(y) 为真
4. EG(存在量词引入规则)：A(c)\Rightarrow \exists xA(x)

例 1： 构造下列推理的证明

<1> 前提：\forall xG(x)

步骤 | 公式 | 理由 :-|:-:|:- 1 | \forall x(F(x)\rightarrow G(x)) | 前提引入 2 | F(c)\rightarrow G(c) | 1，UI 3 | \forall xF(x) | 前提引入 4 | F(c) | 3，UI 5 | G(c) | 2，4，假言推理 6 | \forall xG(x) | 5，UG

<2> 用归谬法 (反证法) 证明下列推理 前提：\exists xF(x)

步骤 | 公式 | 理由 -|-|- 1 | \neg \exists xF(x) | 附加前提引入，假设结论不成立 2 | \forall x\neg F(x) | 1，量词否定转换 3 | \neg F(c) | 2，UI 4 | \neg \exists xG(x) | 前提引入 5 | \forall x\neg G(x) | 4，量词否定转换 6 | \neg G(c) | 5，UI 7 | \forall x(F(x)\vee G(x)) | 前提引入 8 | F(c)\vee G(c) | 7，UI 9 | F(c) | 6，8，析取三段论 10 | \neg F(c)\wedge F(c) | 3，9，合取(出现矛盾，假设不成立❌)

** 例 2：** ⭐️证明下述论断的正确性

* 所有哺乳动物都是脊椎动物 * 并非所有哺乳动物都是胎生动物 * 故有些脊椎动物不是胎生动物

proof: 命题符号化：

* p(x): x 是哺乳动物 * q(x): x 是脊椎动物 * r(x): x 是胎生动物

前提：\forall x(p(x)\rightarrow q(x)),\neg \forall x(p(x)\rightarrow r(x)) 结论：\exists x(q(x)\wedge \neg r(x))

步骤 | 公式 | 理由 -|-|- 1 | \neg \forall x(p(x)\rightarrow r(x)) | 前提引入 2 | \exists x\neg (p(x)\rightarrow r(x)) | 1，量词否定转换 3 | \neg (p(c)\rightarrow r(c)) | 2，EI 存在量词消去 4 | \neg(\neg p(c)\vee r(c)) | 3，置换规则（等值演算） 5 | p(c)\wedge \neg r(c) | 4，置换规则 6 | \neg r(c) | 5，化简律 7 | \forall x(p(x)\rightarrow q(x)) | 前提引入 8 | p(c)\rightarrow q(c) | 7，UI 9 | p(c) | 5，化简律 10 | q(c) | 8，9，假言推理 11 | q(c)\wedge \neg r(c) | 6，10，合取 12 | \exists x(q(x)\wedge \neg r(x))✔️ | 11，EG 存在量词引入