前两篇中，我们介绍了演算和（组合子逻辑），
我们采用了公理化的方法，先定义系统中的公理，然后定义推导规则，
最终得到了两个形式系统，系统以及系统。
值得注意的是，公理系统不仅仅包含由公理和推导构成的形式系统，
还包含给这个形式系统所选择的语义。
给形式系统选择一个可靠的语义，是复杂的，我们将在后文再详细介绍。
从这一篇开始，我们先开始介绍数理逻辑，
看看逻辑学是怎么看待形式化问题的。
1. 命题逻辑形式系统
下文中，我们采用与系统，系统相同的方式，
来介绍命题逻辑（propositional logic）。
命题逻辑，是在研究命题的证明和推理的过程中抽象出来的，
先不考虑语义，仅仅从符号的角度（形式化）来考虑它，则是更简单直接的。
1.1 公理和推导规则
首先我们给出命题逻辑形式系统中的公理，
（1）
（2）
（3）
然后，我们给出命题逻辑形式系统中的推导规则，
（1）
以上推导规则可以理解为，
如果和成立，则成立。
这里我们采用了推导规则的常用写法，，
横线上面的部分“”称为规则的前提（premise），
横线下面的部分“”，称为结论（conclusion）。
在命题逻辑中，根据公理和推导规则，得到的公式称为定理。
根据公理，定理和推导规则，得到的公式也是定理。
1.2 例子
下面我们来看一个例子，
求证：是一个定理。
证明：
首先，我们使用公理（1），我们有下式成立，
然后，我们使用公理（2），并令其中的，
最后，我们结合以上两个结论，再使用推导规则（1），就得到了，
证毕。
2. Hilbert-style和Gentzen-style
以上的证明过程中，每一行断言，是一个不包含条件的定理，
这种风格的演绎系统（deduction system）称为具有Hilbert-style。
如果是有限的公式集合，则，
，称为一个序贯（sequent）。
其中，称为序贯的前提（antecedent），称为序贯的结论（succedent）。
它表示，如果公式集都成立，那么中至少有一个成立。
如果证明过程中，每一行断言是一个序贯，
这种风格的演绎系统，称为具有Gentzen-style。
Hilbert-style演绎系统，通常具有较多的公理，但是具有较少的推导规则，
Gentzen-style演绎系统，则反之，具有较少的公理，却具有较多的推导规则。
如果中总是只包含一个公式，
则称该演绎系统为自然演绎系统（natural deduction system）。
如果有限序列，，满足，
（1）为有限公式集
（2）为公式
（3）每个，，都是它之前若干个，，应用某条推导规则得到的
我们就称这个有限序列，为的一个（形式）证明序列。
此时，也称可由（形式）证明。
3. 命题逻辑的自然演绎系统
以上定义的形式系统，称为命题逻辑形式系统，
下面我们再定义一个与之等价的，命题逻辑的自然演绎系统。
3.1 语法
（1）可数个命题符号：
（2）5个联接词符号：
（3）2个辅助符号：
3.2 合法的公式
我们使用BNF来定义，
3.3 推导规则
（1）包含律：
（2）消去律：
（3）消去律：
（4）引入律：
（5）消去律：
（6）引入律：
（7）消去律：
（8）引入律：
（9）消去律：，
（10）引入律：
3.4 例子
以上，我们定义了命题逻辑的自然演绎系统，
它比命题逻辑形式系统更复杂一些，但是这两个系统是等价的。
我们来看一个例子。
求证，是一个定理。
证明：
首先，我们根据包含律有，
然后，根据这两个结论，以及消去律，就有，
。
证毕。
4. 系统和的等价性
本文我们介绍了两个形式系统，
命题逻辑形式系统，以及命题逻辑的自然演绎系统，
可以证明，对于（或）中的公式，当且仅当。
因此，这两个系统中的定理集是一样的，
某个定理在中可证，当且仅当在中也可证。
其中，我们令，
，表示，
，表示，
，表示。
对于这两个系统而言，如上文所示，
我们只进行了符号的推导操作，即对公式进行形式证明，
至于这些符号到底代表什么意思，我们却故意没有提及。
我们并没有说表示“或”，也没有说表示“与”，
在学数理逻辑的时候，一开始就将形式系统与它的语义模型相区分，
是非常有益的，后文我们将看到这样做的好处。
5. 总结
本文介绍了命题逻辑，以及与之相关的两个形式系统和，
和，一样，我们采用了公理化的方式构建它们，
这样得到的形式系统，只是符号演算，还没有被赋予特定的语义，
下文我们开始介绍一阶谓词逻辑。