命题逻辑的公理系统

重言式定理

同一律

排中律

矛盾律

分离律

双重否定律

幂等律

交换律

德摩根律

结合律

分配律

公理系统

命题演算三组公理：

设定一个初始推理规则：
分离规则（MP）如果有和，那么有。
以上三条公理和一条推理规则是这个演算系统的全部初始设定。从这些初始设定出发演绎出系统的内定理，需要给出「形式证明」的严格定义。
形式证明的定义

（证明）. 是一个有限公式序列，如果每个公式满足以下条件之一，则称这个公式序列为一个序列，简称证明。
（1）是公理。
（2）是由序列中较前的两个公式应用分离规则得到的（即存在使得）。
证明的直观意义就是从公理出发，通过分离规则得到一个又一个公式。
定义：（的证明）. 如果一个证明的最后一项是，则称这个证明的序列为的证明。
定义：（内定理）. 如果有一个证明，则称是一个内定理，记作。
结论：
（1）每条公理都是内定理。
（2）如果是一个证明，则任给也是一个证明，进而也是一个内定理。
演绎规则

（演绎）. 是公式集，是有穷公式序列。如果每个满足以下条件之一，则称这个公式序列是以为假设的一个演绎。
（1）是公理。
（2）是中的公式，即。
（3）是由序列中较前的两个公式应用分离规则得到的（即存在使得）。
定义：（从到的演绎）. 如果以为假设的演绎的最后一项是，则称这个演绎是从到的一个演绎。

如果，则可将简记为。
如果且，记为。
如果存在从到的演绎，则称推出，或是的推论，记为。
已知和都是公式集，如果任给，都有，则记为。

演绎规则：如果有且，则可得。所以，如果已经证明了，而再以为假设的演绎中出现了，则可以直接得出。这意味着一个已经被证明的演绎可以被看作一个演绎规则：从可得到。
应用已证明的演绎规则，可以简化证明。
设是公式。则如下演绎规则成立：
（1）双重否定引入

双重否定消去

（2）蕴含引入或后件引入

蕴含消去或分离规则

（3）合取引入

合取消去

（4）析取引入

析取消去

（5）等值引入

等值消去

（6）反证法

归谬法

（7）假言三段论

析取三段论

（8）前件强化

后件强化

（9）前件弱化

后件弱化

（10）建设性二难推理

破坏性二难推理

（11）幂等律

（12）交换律

（13）德摩根律

（14）结合律

（15）分配律

（16）吸收律

输出律

（17）假言易位

（18）等值否定交换

演绎的引入，得出了一些演绎规则，这些演绎规则能够进一步简化证明。但如果想证明内定理，则演绎规则中的假设必须是之前已经得到的，在内定理的证明过程中不能应用假设。
因此还需要考虑一些能够消去假设的原则，应用这些原则，可以从有假设的演绎得到内定理。其中最重要的就是演绎定理。
演绎定理

定义：（演绎定理）. 如果，则。
定义：（演绎规则的逆）. 如果，则。

演绎定理及其逆定理揭示了内定理和有前提（假设）的演绎之间的关系，能够帮助理解系统内定理和推理之间的关联。
当时，作为演绎定理和演绎定理你定理的特例，可以得到：当且仅当。

演绎定理还可以得到反证法和归谬法的其他形式：
引理：（反证法的第二形式）. 如果且，则。
引理：（归谬法的第二形式）. 如果且，则。
引理：（反证法的第三形式）. 如果且，则。

反证法、归谬法的几种形式也可以用于消去假设。

这个命题逻辑的公理系统是否是命题逻辑的形式化需要从两个方面考虑这一问题：一是可靠性，二是完全性。
可靠性

定理：（可靠性）. 如果，那么。即命题演算的所有内定理都是重言式。
定理：（广义可靠性）. 如果，则。
完全性

定理：（完全性）. 如果，那么。即命题逻辑语言下的所有重言式都是命题演算的内定理。
定理：（广义完全性）. 如果，则。

最早的完全性证明是由哥德尔给出的，而斤亨金的证明方法为人民所普遍采用。亨金最初用于证明一阶演算的完全性。也可以用于命题逻辑完全性证明。亨金证明是利用极大一致集及其性质证明的。

完全性定理亨金版本描述：设是任意命题逻辑公式，若不是内定理，则存在赋值，使得。
紧致性

公式集是可满足的当且仅当的每个有穷子集都是可满足的。

紧致性定理有很多重要的应用，在「一阶逻辑」中将会有充分的体现。

可判定性

如果一个算法告诉我们一个公式是否是一个逻辑的内定理，则称这个逻辑是可判定的。对于命题逻辑而言，应用真值表就可以判定是否重言式。因此，命题逻辑是可判定的。

一阶逻辑不具有可判定性，这是命题逻辑和一阶逻辑的重要区别之一。

此文是命题逻辑的一个公理系统，事实上命题逻辑还有自然演绎系统（自然推理系统）。自然演绎系统最初是由德国数学家 Gentzen 引进的。公理系统和自然演绎系统各有特点。