命题演算是描述命题逻辑的形式系统。在命题演算中，我们仍然研究命题逻辑公式，同样对公式提出永真、不永真等概念，但不再采用（真值）函数论的观点，而是采用数理逻辑本身所固有的观点—形式公理、形式定理的观点，在这种观点下，一个公式称为可从另一个公式推出，即指存在某个所谓“形式推理”从后者一步步推出前者，而一个公式所谓是永真的，即它能从公理系统中的公式出发形式地推出，等等。新的观点要求我们掌握在讨论各种问题时采用新的方法—形式演绎法，这种方法比起我们前面采用的真值表方法来，要难于接受一些，但是我们必须掌握它，因为它更重要，实际上，掌握这种方法是学习数理逻辑的基本目的之一。
第一节 命题演算的公理系统
。
描述任何一个形式系统，都要包含3步工作：
1. 指出这个形式系统的所有组成符号；
2. 规定由这些符号组成的符号串（string）中哪些是该形式系统的公式；
3. 从全体公式中，再划分出哪些公式是该形式系统中的永真公式。
公理系统可有许多不同形式，下面先来介绍我们采用的公理系统，然后再介绍一些别的公理系统，并说明选择公理系统的原则。
（一）我们采用的公理系统
我们采用的公理系统，就是我们上章第二节所介绍的那些，只是把大写拉丁字母X,Y,Z等换成A,B.C等，这是为了与后面第四章谓词演算中使用的符号统一。因此不再在这里重新描述。这个公理系统的全体永真公式是用如下方式从公式中划分出来的：
我们指出某些公式是公理，公理是初始永真公式；再指出由公理产生新永真公式的那些手段；最后肯定，所有永真公式都能由这些方法产生，不能由这些方法产生的公式都不是永真公式。
【公理】我们重点研究的公理系统包含下列12条公理：
以上14条公理分成五组，在每一组符号中均出现蕴含号，而且还都是蕴含式，即公式形成时最后一次为蕴含运算。五组公理第一组中不再有其他符号，其余四组依次出现一个新符号，它们是合取&析取V否定--和等价号
注意，这14条公理显然都是第一章命题逻辑中的永真公式，如果读者怀疑其永真性，不妨用真值表方法去验证一下。但是我希望读者能直接看出每一条都是一个永真命题，即所谓的“重言式”。
推理模式：由已知永真公式推演新永真公式的任何手段，统称推理模式。推理模式有2类，一种是基本的，基本推理模式是我们无条件承认的，它们具有公理性质，允许我们无条件使用；另一类叫导出的推理模式，这种推理模式由永真公式推演新永真公式时需要证明的。我们的公理系统的基本推理模式有两条:
1. 代入模式：由真公式，可生成真公式，其中
且还都是蕴含式。
2. 蕴含模式：由真公式，可生成真公式，其中
且还都是蕴含式。
.