命題演算 是 邏輯 的形式基礎，處理諸如“非”、“或”、“與”和“蘊含”等詞語的概念和用法。已經設計了許多命題演算系統，旨在實現 公理 的一致性、完備性和獨立性。“語句演算”一詞有時用作命題演算的同義詞。
公理（或其模式）和推理規則定義了 證明理論，並且可以設計出各種等效的命題演算證明理論。以下命題演算公理模式列表來自 Kleene (2002)。
 |
(1)
|
 |
(2)
|
 |
(3)
|
 |
(4)
|
 |
(5)
|
 |
(6)
|
 |
(7)
|
 |
(8)
|
 |
(9)
|
 |
(10)
|
在每個模式中，
、
、
可以被任何 語句公式 替換。以下稱為 肯定前件 的規則是唯一的推理規則
 |
(11)
|
此規則表明，如果 
和 
中的每一個都是公理或透過應用推理規則從公理形式推匯出的定理，則 
也是一個形式定理。
其他規則從 肯定前件 推導而來，然後在形式證明中使用，以使證明更簡短和更易於理解。這些規則用於直接引入或消除 聯結詞。肯定前件 基本上是 
-消除，而 演繹定理 是 
-引入。
示例引入規則包括
 |
(12)
|
示例消除規則包括
 |
(13)
|
基於 肯定前件 的證明理論稱為希爾伯特型，而那些基於作為假定規則的引入和消除規則的證明理論稱為根岑型。命題演算中的所有形式定理都是 永真式，並且所有 永真式 都是形式上可證明的。因此，證明可以用於發現命題演算中的 永真式，而 真值表 可以用於發現命題演算中的定理。
可以僅使用 與非 運算子來構建命題邏輯。可以在 Wolfram (2002, p. 1151) 中找到其歷史。最短的此類公理是 Wolfram 公理。
