命题演算 是 逻辑 的形式基础，处理诸如“非”、“或”、“与”和“蕴含”等词语的概念和用法。已经设计了许多命题演算系统，旨在实现 公理 的一致性、完备性和独立性。“语句演算”一词有时用作命题演算的同义词。
公理（或其模式）和推理规则定义了 证明理论，并且可以设计出各种等效的命题演算证明理论。以下命题演算公理模式列表来自 Kleene (2002)。
 |
(1)
|
 |
(2)
|
 |
(3)
|
 |
(4)
|
 |
(5)
|
 |
(6)
|
 |
(7)
|
 |
(8)
|
 |
(9)
|
 |
(10)
|
在每个模式中，
、
、
可以被任何 语句公式 替换。以下称为 肯定前件 的规则是唯一的推理规则
 |
(11)
|
此规则表明，如果 
和 
中的每一个都是公理或通过应用推理规则从公理形式推导出的定理，则 
也是一个形式定理。
其他规则从 肯定前件 推导而来，然后在形式证明中使用，以使证明更简短和更易于理解。这些规则用于直接引入或消除 联结词。肯定前件 基本上是 
-消除，而 演绎定理 是 
-引入。
示例引入规则包括
 |
(12)
|
示例消除规则包括
 |
(13)
|
基于 肯定前件 的证明理论称为希尔伯特型，而那些基于作为假定规则的引入和消除规则的证明理论称为根岑型。命题演算中的所有形式定理都是 永真式，并且所有 永真式 都是形式上可证明的。因此，证明可以用于发现命题演算中的 永真式，而 真值表 可以用于发现命题演算中的定理。
可以仅使用 与非 运算符来构建命题逻辑。可以在 Wolfram (2002, p. 1151) 中找到其历史。最短的此类公理是 Wolfram 公理。
