从形式系统的角度来看，
一阶谓词逻辑，只是比命题逻辑多添加了一些公理，
或者多添加了一些推导规则，
然而，这样的举动，却会让形式系统截然不同。
欧几里得第五公设，是一个公理，无法由前四个公设推导证明，
在原来的欧氏几何中去掉它，然后添加上不同的第五公设，就变成了不同的几何，
黎曼几何与闵可夫斯基几何。
因此，不同的公理和推导规则，构成了不同的形式系统，
哪怕是有很小的变化。
本文我们来扩充前一篇中提到的，命题逻辑形式系统，
以及，命题逻辑的自然演绎系统。
1. 一阶谓词逻辑形式系统
1.1 公理和推导规则
命题逻辑形式系统，只有三条公理，一条推导规则，
以下我们保持推导规则不变，为它添加四条公理，
这样得到的系统，我们记为。
公理：
（1）~（3）与命题逻辑形式系统相同
（4），若对在中自由出现
（5），若不在中自由出现
（6）
（7）若是的一个公理，则也为的一个公理
推导规则：
（1）与命题逻辑形式系统相同
1.2 辖域和自由出现
其中（5）和（6）中提到了“自由出现”的概念，
现在解释如下，
我们称公式中的，为量词的辖域。
变元符号在公式中的某处出现，如果是在量词的辖域内，
则称为约束出现，否则称为自由出现。
例如，，
由于的优先级比较低，上式相当于，
所以，第一个是约束出现，第二个是自由出现。
1.3 例式
上述公理（4）中，出现了，它称为公式的例式。
它表示，将中每一个自由出现的，都替换为项之后，得到的公式。
1.4 简写
我们记，
，为的简写，
，为的简写，
，为的简写，
，为的简写。
1.5 举个例子
求证：设项对变元符号在中自由，则是是一条定理。
证明：
因为，
又根据公理（4），，
所以，。
又根据公理（3），，
再根据推导规则（1），，
，
即，。
证毕。
2. 一阶谓词逻辑的自然演绎系统
上一篇中我们介绍了命题逻辑的自然演绎系统，
而且，我们知道了是与命题逻辑形式系统是等价的。
现在我们扩充，得到一阶谓词逻辑的自然演绎系统，
它与一阶谓词逻辑形式系统也是等价的。
和一样，是Hilbert-style演绎系统，
它们具有更多的公理，更少的推导规则，
而和，是Gentzen-style自然演绎（natural dedution）系统，
它们具有更少的公理，更多的推导规则。
由于是对的扩充，
下文中，我们只列出新增的公理和推导规则。
2.1 公理和推导规则
公理：
公理集仍为空集。
推导规则：
（1）~（10）与命题逻辑的自然演绎系统相同
（11）增加前提律：
（12）消去律：，对在中自由出现
（13）引入律：
（14）消去律：，不在中自由出现
（15）引入律：，对在中自由出现
2.2 举个例子
求证：
证明：
根据规则（1）包含律，
（1），
（2），
根据规则（12）消去律，
（3），
（4），
式（3）（4），根据规则（9）消去律，
（5），
式（4）（5），根据规则（13）引入律，
（6），
（7），
式（6）（7），根据规则（10）引入律，
（8）。
证毕。
3. 总结
本文介绍了两种风格的一阶谓词逻辑演算系统，
其中是Hilbert-style演绎系统，
是Gentzen-style自然演绎系统，
可以证明它们是等价的。
结合上一篇，我们已经从形式系统的角度介绍了命题逻辑和一阶谓词逻辑，
我们有了足够的基础之后，就可以给系统加上类型，
开始介绍简单类型演算了。