17世纪德国数学家和哲学家莱布尼茨在创立数理逻辑时，曾经有过两个设想：第一，建立一种精确的通用语言；第二，在这种通用语言的基础上，寻求一种推理演算，以便用计算来解决论辩和争论的问题.上一节，我们完成了他的第一个设想.本节我们来实现他的第二个设想.为实现他的第二个设想，我们采用公理化的方法.正如两千多年前欧几里得几何学一样，把一些较为自明的基本性质作为公理或公设，以此为出发点，严格地论证出一系列的定理.根据我们研究和讨论的对象，我们只能取重言式（或永真式）作为公理.另外，在我们建立的推理演算（系统）中，推理的研究和证明的研究都是从形式结构方面进行的，把形式和内容分离开进行的，因而得到的结果也是形式的.但就形式结构来说，它有普遍性.关于这一点，读者可以在学完了本节的内容以后，作一些对比.例如，把传统逻辑中的排中律、同一律和不矛盾律，与命题演算系统中的排中律、同一律和不矛盾律进行对比，然后体会一下二者的处理方法.其实，后者的处理方法，是数学化的方法.

由于数学的陈述通常用半形式化语言来表述，这种半形式化语言是由某种自然语言（例如，汉语、英语等等）辅之以专门的数学符号组成.本节中，我们关于形式定理的证明都是形式的.所以，这一节的讨论都是用符号表述的，读者可能会感到抽象一些.其实，弄清它的缘由就好了.这就像小孩儿做算术题一样，也有一个抽象的过程.开始，大人们告诉他们：1个苹果加上2个苹果等于3个苹果.后来就可以把“1个苹果加上2个苹果等于3个苹果”表示成：1+2=3（苹果）.再后来，他们就会做任意两个数a和b的加法a+b了.特别地，他们还知道a+b=b+a.即两个数相加满足交换律.在这一节里，我们要寻找命题之间的一些推理规律.如两个命题关于合取运算是否满足交换律等.

本书所采用的命题演算的公理系统是D.希尔伯特（Hilbert）型的系统.这一节将介绍公理系统PC.它的特点是，每一公理采用形式语言表示，每一公理模式代表无穷多条公理.因此，推理比较简单，同时不需要作代入.(www.daowen.com)

命题演算的公理系统PC所用的语言，是本章第二节中的L0.本节要做的就是把所有的重言式汇集成一个系统，把我们心目中的重言式一并列出来，使得后面的总可以从前面的“演绎”出.最前面的就是作为演绎出发点的“公理”，通过它们可以演绎出其他的“重言式”，而它们本身是不能由别的“重言式”演绎出的.