量词相关的推理规则

定义 1　量词相关的推理规则

　　 量词相关的推理规则有以下四条，用 $x$，$y$ 表示变元，而 $c$ 表示常元，则可以分别表示为：

1. $\forall -$ 规则（US 规则，又称 UI 规则）：
   \begin{equation} \forall x A(x) \Rightarrow A(y) ~, \end{equation}
   \begin{equation} \forall x A(x) \Rightarrow A(c) ~. \end{equation}
2. $\exists -$ 规则（ES 规则，又称 EI 规则）：
   \begin{equation} \exists x A(x) \Rightarrow A(c) ~. \end{equation}
   注意此处只能使用常元，此处 $c$ 是使 $A(x)$ 成立的那常元。
3. $\forall +$ 规则（UG 规则）：
   \begin{equation} A(y) \Rightarrow \forall x A(x) ~. \end{equation}
4. $\exists +$ 规则（EG 规则）：
   \begin{equation} A(c) \Rightarrow \exists x A(x) ~. \end{equation}