命题逻辑

在逻辑和数学里，命题演算（或称句子演算）是一个形式系统，有着可以由以逻辑运算符结合原子命题来构成代表“命题”的公式，以及允许某些公式建构成“定理”的一套形式“证明规则”。

术语

一般来讲，运算是一个形式系统，包括一套语法表示式、这些表示式可区分的子集（公理）和一套定义了特定的二元关系，可解译为表示式空间上的逻辑等价的形式规则。 若形式系统被指为是一个逻辑系统，其表示式会被解释成数学陈述，且其规则，被称之为“推理规则”，则一般会被指是保真的。在此设定下，规则（可能也包括公理）可以被用来从给定为正确陈述的公式中推导出表示正确陈述的公式来。 公理的集合可能为空集、非空有限集、可数无限集或由公理模式所给定。形式文法递回地定义了语言的表示式和合式公式。之外，一个语义可以由定义真值和赋值（或解释）来给定。 命题运算的语言包括：(1)一套原始符号，被称之为“原子公式”、“占位符”、“命题字母”或“命题变量”；(2)一套运算符号，被称之为“逻辑运算符”。一个“合式公式”是任一原子公式，或任一以运算符号依文法规则由原子公式建立起的公式。 在下文中我们描述一种标准命题演算。很多不同的公式系统存在，它们都或多或少等价但在下列方面不同：(1)它们的语言(就是说哪些操作符和变量是语言的一部分); (2) 它们有哪些(如果有的话)公理; (3)采用了哪些推理规则。

命题演算的形式描述

命题演算是一个形式系统 ，它的公式按如下方式构造:

是有限多个被称之为“命题符号”或“命题变量”之元素所组成的集合。语法上来说，这些是形式语言  最基本的元素，亦被称之为“原子公式”或“终端元素”。在后面的例子中，  内的元素一般会被写为字母 p 、 q 、 r 之类的形式。

是有限多个被称之为“算子符号”或“逻辑运算符”之元素所组成的集合。集合 被划分成如下等不相交的子集：

在此一划分中， 是指元数为 的算子符号所构成的集合。 在更熟知的命题演算中， 一般被划分如下:

常数逻辑值则常被选择视为一种零元算子，即：

有些作者用 ~ 来替代 ¬ ，且用 & 或 来取替 。逻辑值所构成的集合也有许多不同的符号表示，如 {假,真} 、 {F,T} 、 {0,1} 和 {, } ，这些都常见于各个文献之中。 依据所使用的精确形式文法或文法形式化，语法辅助设施如左括号 "(" 和右括号 ")"，若要完成公式的构造，可能会是必须的。

的语言，亦称之为“公式”或“合式公式”的集合，可由如下规则被归纳或递回地定义：

基本元素： 内的任何元素都是 的公式。 步骤 (a)：如果 p 是公式，则 ¬p 也会是公式。 步骤 (b)：如果 p 和 q 是公式，则 ( ) 、 ( ) 、 () 和 () 也都会是公式。 封闭性：其他都不会是 的公式。 重复应用这三个规则允许建构出复杂的公式来。例如: 依规则 1，p 是公式。 依规则 2，¬p 是公式。 依规则 1，q 是公式。 依规则 3，(¬p ∨ q) 是公式。

是有限多个当取得逻辑应用时被称之为“推理规则”之“转换规则”所构成的集合。
是有限多个当得到逻辑解释时被称之为“公理”之“起始点”所构成的集合。

简单的公理系统

设 ，这里的 定义如下:

是个大到有足够多可供给定的讨论所需之符号所构成的有限集合，如：

合取、析取和蕴涵（∧、∨ 和 →）这三个运算符，可以将其中一个拿来当做基本的，而另两个则以其和否定（¬） 来定义。实际上，所有的逻辑运算符都可以用自足算子的方式来定义。而双条件（↔）当然可由合取和蕰涵来定义，亦即 a ↔ b 可被定义为 (a → b) ∧ (b → a) 。 接受否定和蕴涵作为命题演算的两个基本运算等价于把 omega 集 划分为如下: 采用否定和蕰涵做为命题演算的两个基本运算，相等于将 划分如下：

由扬·武卡谢维奇所发现的一个公理系统可以依如下公理模式公式化此语言的命题演算。

其推理规则为肯定前件（即可由 p 和 (p → q) 导出 q ）。而 a ∨ b 和 a ∧ b 则是分别被定义为 ¬a → b 和 ¬(a → ¬b) 。 设 ，这里的 定义如下:

是个大到有足够多可供给定的讨论所需之符号所构成的有限集合，如：

。

划分为如下:

。 。 在此命题演算的例子中，转换规则被解释为所谓的“自然演绎系统”下之推理规则。这里表述的特定系统没有起始点，这意味着它对逻辑应用的解译是从空公理集合中推导出其定理的。 起始点的集合是空的，亦即 。 转换规则的集合 描述如下: 此命题演算有十个推理规则。这些规则允许我们从给定的一组假定为真的公式中推导出其他为真的公式。 前九个简单的陈述我们可以从其他合式公式推论出特定的合式公式。但是最后一个规则使用了假言(hypothetical)推理，这意味着在规则的前提中我们可以临时的假定一个(未证明的)假设作为推导出的公式集合的一部分，来查看我们是否能推导出一个特定的其他公式。因为前九个规则不是这样而通常被描述为“非假言”规则，而最后一个则被称为“假言”规则。 反证证明(否定介入) 从 φ → ¬ ψ 和 φ → ψ 中可推出 ¬ φ 。 双重否定除去 从 ¬ ¬ φ 中可推出 φ。 合取介入 从 φ 和 ψ 中可推出 ( φ ∧ ψ ) 。 合取除去 从 ( φ ∧ ψ ) 中可推出 φ 和 ψ 。 析取介入 从 φ 中可推出 (φ ∨ ψ) 和 (ψ ∨ φ) 。 析取除去 从 ( φ ∨ ψ ) 、 ( φ → χ ) 和 ( ψ → χ ) 可推出 χ 。 双条件介入 从 ( φ → ψ ) 和 ( ψ → φ ) 中可推出 ( φ ↔ ψ )　。 双条件除去 从 ( φ ↔ ψ )　中可推出 ( φ → ψ ) 和 ( ψ → φ ) 。 肯定前件(条件除去) 从 φ 和 ( φ → ψ ) 中可推出 ψ。 条件证明(条件介入) 若假定 φ 为真可证明出 ψ ，可推出 ( φ → ψ ) 。