1.QC的公理（模式）

A1：α∨α→α；

A2：α→α∨β；

A3：α∨β→β∨α；

A4：（β→γ）→（（α∨β）→（α∨γ））；

A5：∀xα（x）→α（y）；

A6：α（y）→∃xα（x）.

前四条公理从形式上讲同命题演算PC系统中的公理（模式）一样，后两条是新增加的关于量词的公理（模式）.其中A5是关于全称量词的，它说明：“如果一切个体都具有性质α，则某一特定的个体y也具有性质α.”A6是关于存在量词的，它说明：“如果某个特定的个体y具有性质α，则存在一个个体x具有性质α.”

2.QC的推理规则

R1：由α（y/x）→β可得∃xα（x）→β，这里的y不在∃xα（x）和β中自由出现.

R2：由α→β（y/x）可得α→∀xβ（x），这里的y不在∀xβ（x）和α中自由出现.(www.daowen.com)

R3：由α和α→β可得β.

注：这里α（y/x）是将α中所含x都换为y的结果，β（y/x）同样.

前两条推理规则是新增加的.R1叫做关于前件的存在规则，R2叫做关于后件的概括规则.这里需要注意的是：在这个演绎系统中，有些推理规则看起来是显然的，但我们绝不可因此而掉以轻心，认为似乎规则多一个少一个没有关系.须知逻辑推理是一件极其严格的事情，不能只依靠直觉，直觉往往会欺骗我们.我们已经看到，这个系统中的规则R1和R2是加了限制的.如果不加说明，很难看出某些规则需要加这样或那样的限制，这就是直觉的欺骗性.在和涉及量词的运算打交道时，特别要注意这个问题.演绎系统必须十分严格的第二个原因，是因为我们希望把相当一部分逻辑推理的工作交给计算机去做（这个希望现在已经实现）.然而，计算机是没有直觉的，它只能一步一步死板地去做，即所谓机械化运算.因此，除了规定的变换规则以外，不允许它做任何其他的变换.所以严格的逻辑系统必须设计得使计算机能照办才行.（见文献[20]）

现在，从总体上来说，一个狭谓词逻辑的公理系统QC已经建立起来了.下面，我们将第三章3.3.2节中Φ0α和0α的定义推广到QC系统中.

定义2.1 满足下面两个条件之一的公式所组成的有穷公式序列φ1，φ2，…，φn称为本系统的一个证明：

（1）φi（i=1，2，…，n）是公理之一；或

（2）是由序列中排在前面的一个或两个公式运用推理规则得到的.

证明的有穷公式序列的最后一个公式φn，如果是α，称该证明是公式α的一个证明，或说α在QC系统中是可证的，记作α，并称α是QC系统的一个定理.

一般情况下，我们有如下的定义：

定义2.2 设α是任一公式，Φ是任一公式集.如果存在一个有穷的公式序列，其末项是公式α，而且该序列中的每个公式或是一个公理，或是属于Φ，或是由排在前面的一个或两个公式应用推理规则得到的，那么称公式α是从公式集Φ可演绎的，记作Φα，当Φ=∅时，即α.