命题逻辑是逻辑学的一个分支，研究命题及其组合之间的逻辑关系。它用符号表示命题，并用对应于“非”“且”“或”等表达的算子将命题连接起来。与一阶逻辑不同，命题逻辑不将命题进一步分析为对象、谓词和量词。在标准的经典解释中，每个命题都被赋予且仅被赋予两个真值之一：真或假。命题逻辑系统也包括采用不同解释或推理规则的非经典系统。(plato.stanford.edu)
语言与联结词
命题语言的句法规定了哪些表达式是合式公式。命题变元通常写作 (p,q,r)，它们本身就是原子公式。如果 (A) 和 (B) 是公式，那么 (\neg A)、((A\land B)) 和 ((A\to B)) 等表达式也是公式。反复应用这些构造规则，可以生成任意复杂的表达式。括号用于区分可能产生歧义的结构。有些语言还包含常量 (\top) 和 (\bot)，分别表示真和假。(cs.cmu.edu)
主要的逻辑联结词具有以下经典含义：
| 联结词 | 记号 | 真值条件 |
|---|---|---|
| 否定 | (\neg A) | 当且仅当 (A) 为假时为真 |
| 合取 | (A\land B) | 当且仅当两个组成部分都为真时为真 |
| 析取 | (A\lor B) | 至少一个组成部分为真时为真 |
| 实质蕴涵 | (A\to B) | 当且仅当 (A) 为真且 (B) 为假时为假 |
| 双条件 | (A\leftrightarrow B) | 当且仅当两个组成部分的真值相同时为真 |
这里的析取是相容析取；异或则要求恰好有一个组成部分为真。(plato.stanford.edu)
尤其需要将实质蕴涵与日常语言中的条件句区分开来。实质蕴涵等价于 (\neg A\lor B)，因此，只要前件为假，它就为真。它本身并不表示因果关系、时间先后关系，也不表示前件与后件之间存在任何实质联系。因此，将日常语言转化为形式表达时，必须注意这种形式化保留了原意的哪些方面。(plato.stanford.edu)
语义与真值表
经典语义学从赋值出发，为每个命题变元指定真或假。联结词的真值条件将这种赋值扩展到复合公式。真值表列出与某个公式相关的所有赋值；若有 (n) 个不同的变元，真值表就有 (2^n) 行。例如：(plato.stanford.edu)
| (p) | (q) | (p\land q) | (p\to q) |
|---|---|---|---|
| 真 | 真 | 真 | 真 |
| 真 | 假 | 假 | 假 |
| 假 | 真 | 假 | 真 |
| 假 | 假 | 假 | 真 |
重言式在每一种赋值下都为真，例如 (p\lor\neg p)。矛盾式在每一种赋值下都为假，例如 (p\land\neg p)。偶然式在某些赋值下为真，在另一些赋值下为假。如果至少存在一种赋值使某个公式为真，该公式就是可满足的；如果存在同一种赋值使若干公式全部为真，这些公式就是共同可满足的。(forallx.openlogicproject.org)
逻辑后承与等价
逻辑有效性关注的是真值的保持，而不是特定前提事实上是否为真。记号 (\Gamma\models A) 表示：凡是满足 (\Gamma) 中全部前提的赋值，也都满足 (A)。无效论证存在反例赋值，即使所有前提为真而结论为假的赋值。因此，仅凭有效性并不能确定一个论证的前提是否正确描述了现实世界。(plato.stanford.edu)
例如，由 (p) 和 (p\to q) 可以推出 (q)，这体现了肯定前件式。但由 (q) 和 (p\to q) 不能推出 (p)：当 (q) 为真而 (p) 为假时，两个前提仍然都为真。这种无效的推理模式就是肯定后件的谬误。(cs.cmu.edu)
如果两个公式在每一种赋值下都具有相同的真值，它们就是逻辑等价的。例如，德摩根定律表明，(\neg(A\land B)) 与 (\neg A\lor\neg B) 等价。这类等价关系将命题推理与布尔代数联系起来，并使保持真值条件不变的变换成为可能。(plato.stanford.edu)
证明系统
语义后承不同于可推导性，后者记作 (\Gamma\vdash A)。形式证明通过明确允许的规则推导出结论。证明论研究的系统包括公理演算、自然演绎、相继式演算和语义树。这些系统为演绎推理提供了不同的呈现方式，而不是不同的真值表。(openlogicproject.org)
如果可推导性蕴含语义后承，证明系统就是可靠的；如果语义后承蕴含可推导性，证明系统就是完备的。标准的经典命题演算同时满足这两项性质。因此，真值表所判定的有效性与形式上的可证明性是一致的，不过，构造证明与枚举赋值所需的工作量可能相差很大。(forallx.openlogicproject.org)
范式与计算
每个经典命题公式都有一个与之等价的合取范式：它是若干子句的合取，而每个子句又是若干文字的析取。文字是变元或变元的否定。每个公式也都有一个等价的析取范式，即由若干合取式构成的析取式。否定、合取和析取共同构成函数完备的联结词集：这些联结词可以表达任何有限元布尔真值函数。(plato.stanford.edu)
布尔可满足性问题，简称 SAT，询问一个公式是否存在使其为真的赋值。穷举真值表提供了一种必定终止的算法，从而确立了这一问题的可判定性。不过，SAT 是 NP 完全问题，因此在计算复杂性研究中占有核心地位。DPLL 等搜索过程将分支搜索与强制赋值的传播相结合。推理也可以通过可满足性来检验：有限个前提能够推出 (A)，当且仅当这些前提与 (\neg A) 的合取不可满足。(cs.cmu.edu)
应用与范围
在计算机科学中，命题公式用于描述逻辑门和开关电路，并支持自动推理。在人工智能中，命题公式可以将事实、规则和规划约束编码到知识库中。命题逻辑的局限在于，它将原子命题视为不再分析的整体：要表达关于所有对象的一般性断言，就需要更丰富的语言。模态逻辑增加了表示必然性和可能性的算子，而直觉主义逻辑提供了一种非经典的命题逻辑系统，在其中，无限制的排中律等经典原则一般不能被推导出来。(plato.stanford.edu)