一阶逻辑推理

代换实例, 如

• $\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)$ 为真的客体.