谓词逻辑的自然推理系统Qᴺ是命题逻辑自然推理Pᴺ的扩充，所有Pᴺ的规则都是Qᴺ的规则；所有已经证明的Pᴺ定埋和导出的规则，都是Qᴺ的定理和导出规则，故在证明或推演中可以直接使用它们，无需另外证明。（ - 命题逻辑的自然推演及规则 ）

Qᴺ推演规则（相比命题逻辑不一样的地方）

1，全称量词消去规规∀-（全称例示规则）

从∀xA(x)可以推出A(x/t)，t对x代入自由。

∀xA(x)┣A(x/t)。

图示见下图

全称量词消去规则∀-：从∀xA(x)推出A(x/t)，其中代换x的t不会被A中原有的量词所约束，这包括以下情形：

（1）t是一个个体常项；

（2）A是一个原子公式，x是其中的自由变项，t是任一个体词；

（3）A含有量词，但自由变项x不在这些量词的辖域之内，t是任一个体词。

（4）A含有量词，且自由变项x在这些量词的辖域之内，则t必须是与已量化变项不同的变项。否则，称为t对于公式A中的自由变项x代入不自由。

例题：

2，全称量词引入规则∀+（全称概括规则）

从A(x)可推出∀xA(x)，只要能确保前提中的x是任意的。

A(x)┣∀xA(x)

图示如下：

若不能确保前提中的自由变项x是任意的，就要给该x加标记，其具体做法是：在一个证明或推演的某一步上，出现了含自由变项x的公式A，且不能保证其中的x是任意的，则在该公式的右边注明该公式来历的位置，写上x，表示该x可能不是任意的，不能对它使用∀+规则。

以下三种情形需要给相应的自由变项加标记：

3，存在量词消去规则∃-（存在例示规则）

从∃xA(x)可推出A(x/α)，要求：

（ⅰ）α是先前没有出现过的特指常项；

（ⅱ）如果公式A含有x之外的自由变项y，在行末标记yα。

∃xA(x)┣A(x/α)

图示如下：

4，存在量词引入规则∃+（存在概括规则）

从A(x/t)可推出∃xA(x)，只要代换x的t不会被A原有的量词所约束，或者新引入的存在量词不会将A(x)中除x之外的其他自由变项一并加以约束。

A(x/t)┣∃xA(x)。

图示如下：

这是个技术活，真的难[捂脸]