命题逻辑

命题逻辑是逻辑学的一个分支。 它也称为命題演算、句子演算、句子逻辑，有时也称为零阶逻辑。它涉及命题（可以是真或假）和命题之间的关系，包括基于它们的论证的构建。复合命题是通过逻辑连接词连接命题而形成的。不包含逻辑连接词的命题称为原子命题。 与一阶逻辑不同，命题逻辑不处理非逻辑对象、以及关于它们的谓词或量词。然而，命题逻辑的所有机制都包含在一阶逻辑和高阶逻辑中。从这个意义上说，命题逻辑是一阶逻辑和高阶逻辑的基础。

在邏輯和數學裡， 命题逻辑是一個形式系統, 有可以由以邏輯運算符結合原子命題來構成代表「命題」的公式，以及允許某些公式建構成「定理」的一套形式「證明規則」。

術語

一般地說，演算是一個形式系統，包括一套語法表示式（合式公式）、這些表示式的一個特定子集（公理）和一套定義了特定的二元關係的形式規則，這個二元關係可解釋為表示式空間上的邏輯等價關係。

若形式系統會作為一個邏輯系統，其表示式會被解釋成數學陳述，且其規則，被稱之為「推理規則」，則一般會是保真的。在此設定下，規則（可能也包括公理）可以被用來，從給定為真的陳述的公式中，推導出表示真的陳述的公式來。

公理的集合可能為空集、非空有限集、可數無限集或由公理模式所給定。形式文法遞迴地定義了語言的表示式和合式公式。之外，有時也可以給定一個語義，用以定義真值和賦值（或解釋）。

命題運算的語言包括：（1）一套原始符號，被稱之為「原子公式」、「占位符」、「命題字母」或「命題變量」；（2）一套運算符號，被稱之為「邏輯運算符」。一個合式公式是任一原子公式，或任一以運算符號依文法規則由原子公式建立起的公式。

在下文中我们描述一种标准命题演算。很多不同的公式系统存在，它们都或多或少等价但在下列方面不同：（1）它们的语言（就是说哪些原始符號和運算符號是语言的一部分）；（2）它们有哪些（如果有的话）公理；（3）采用了哪些推理规则。

命题演算的一般描述

命题演算是一個形式系统${\mathcal {L}}={\mathcal {L}}\ (\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I} )$，它的公式按如下方式构造：

• $\mathrm {A} \!$ 集合是由名為「命題符號」或「命題變量」之元素所組成的有限集合，一个「命題變量」可取值为集合裡的「命題符號」。語法上來說，它們是形式語言 ${\mathcal {L}}$ 最基本的元素，亦被稱之為「原子公式」或「終端元素」。在接著的例子中，$\mathrm {A} \!$ 內的元素一般寫作字母$p$, $q$, $r$ 之類的形式。

• $\Omega \!$ 是名為「算子符號」或「邏輯運算符」之元素所組成的有限集合。集合 $\Omega \!$ 被劃分成如下等不相交的子集：

$\Omega =\Omega _{0}\cup \Omega _{1}\cup \ldots \cup \Omega _{j}\cup \ldots \cup \Omega _{m}\,$。

在此一劃分中，$\Omega _{j}\!$ 是指元數為 $j\!$ 的算子符號所構成的集合。

在更熟知的命题演算中，$\Omega \!$ 一般被劃分如下：

$\Omega _{1}=\{\lnot \}\,,$

$\Omega _{2}\subseteq \{\land ,\lor ,\rightarrow ,\leftrightarrow \}\,$。

一種常用的做法是把常數邏輯值當作一種零元算子，即：

$\Omega _{0}=\{\top ,\ \bot \}\,$。

有些作者会用 ~ 來替代 $\neg$，也有的用 & 或 $\cdot$ 來取替 $\land$。逻辑值所構成的集合也有許多不同的符號表示，如 {假,真} 、{F,T} 或 {0,1} 來取替 {$\bot$,$\top$}，這些都常见于各個論著之中。

• $\mathrm {Z} \!$ 集合是「轉換規則」（當作為邏輯應用時則稱之為「推理規則」）之所構成的有限集合。$\mathrm {Z} \!$ 集合的「轉換規則」是用「原子公式」和「邏輯運算符」構成的。

• $\mathrm {I} \!$ 是「起始點」（當得到邏輯解釋時則稱之為「公理」）所構成的有限集合。

依據所使用的精确形式文法或文法形式化，可能需要以左括号"（"和右括号"）"作語法上的輔助，用來完成公式的构造。

${\mathcal {L}}$ 的語言，亦稱之為「公式」或「合式公式」的集合，可由如下規則集合被归纳或遞迴地定義：

1. 基本元素：$\mathrm {A} \!$ 內的任何元素都是 ${\mathcal {L}}$ 的公式。
2. 如果 $p_{1},p_{2},\ldots ,p_{j}$ 是公式 和 $f$ 属于 $\Omega _{j}$, 则 $\left(fp_{1}p_{2}\ldots p_{j}\right)$ 也是公式.
3. 封閉性：其他都不會是${\mathcal {L}}$的公式。

透過重复应用这三个规则，可以建構出复杂的公式來。例如：

• 依规则1，$p$是公式。
• 依规则2，$\neg p$ 是公式。
• 依规则1，$q$ 是公式。
• 依规则2，$(\neg p\lor q)$是公式。

示例 1 简单的公理系统

设 ${\mathcal {L}}_{1}={\mathcal {L}}\ (\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I} )$，这里的 $\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I}$ 定义如下：

• $\mathrm {A} \!$ 是個含有足夠多元素以應付討論所需的有限集合，如：

$\mathrm {A} =\{p,q,r,s,t,u\}\,$。

功能齐全的套装 逻辑运算符（逻辑连接词和否定）的Ω如下。

• $\Omega \!$ 邏輯運算符集合。 在合取、析取和蘊涵（∧、∨和→）這三個運算符之中，可以將其中一個拿來當做基本的，而另兩個則以其和否定（$\neg$）來定義。實際上，所有的邏輯運算符都可以用自足算子的方式來定義。而雙條件（↔）當然可由合取和薀涵來定義，亦即 $a\leftrightarrow b$可被定義為 $(a\rightarrow b)\land (b\rightarrow a)$。

採用否定和薀涵做為命題演算的兩個基本運算，相當於把omega集$\Omega =\Omega _{1}\cup \Omega _{2}$劃分如下：

$\Omega _{1}=\{\lnot \}\,$。

$\Omega _{2}=\{\rightarrow \}\,$。

• $\mathrm {I} \!$ 公理系統集合。 有一個公理系統是扬·武卡谢维奇所發現的，而這系統可以如下地公式化為此語言中的命題演算。各個公理都是由下列的公理模式作代換所得。

• $p\to (q\to p)$

• $(p\to (q\to r))\to ((p\to q)\to (p\to r))$

• $(\neg p\to \neg q)\to (q\to p)$

• $\mathrm {Z} \!$ 推理規則集合。 其推理規則為肯定前件（即可由 $p$ 和 $(p\rightarrow q)$ 導出 $q$）。而 $a\lor b$ 和 $a\land b$ 則是分別被定義為 $\neg a\rightarrow b$ 和 $\neg (a\rightarrow \neg b)$。

示例 2 自然演绎系統

设${\mathcal {L}}_{2}={\mathcal {L}}\ (\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I} )$，这里的$\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I}$定义如下：

• $\mathrm {A} \!$是個含有足夠多元素以應付討論所需的有限集合，如：

$\mathrm {A} =\{p,q,r,s,t,u\}\,$。

• $\Omega =\Omega _{1}\cup \Omega _{2}$划分为如下：

$\Omega _{1}=\{\lnot \}\,$。

$\Omega _{2}=\{\land ,\lor ,\rightarrow ,\leftrightarrow \}\,$。

在此命題演算的例子中，轉換規則被解釋為所謂的「自然演繹系統」下之推理規則。这里表述的特定系统没有起始点，这意味着它對邏輯應用的解釋是從空公理集合中推導出其定理的。

• 起始点的集合是空的，亦即 $\mathrm {I} =\varnothing \,$。

• 轉换规则的集合 $\mathrm {Z} \!$ 描述如下：

此命题演算有十个推理规则。这些规则允许我们从给定的一组假定为真的公式中推导出其他为真的公式。前九个只是簡單地指我们可以从其他合式公式推论出特定的合式公式。但是最后一个规则使用了假言（hypothetical）推理，这意味着在规则的前提中，我们可以临时的假定一个（未证明的）假设作为推导出的公式集合的一部分，来查看我们是否能推导出一个特定的其他公式。因为前九个规则不是这样而通常被描述为“非假言”规则，而最后一个則被稱為“假言”规则。

1. 否定介入：從 $\phi \rightarrow \neg \psi$ 和 $\phi \rightarrow \psi$ 中可推出 $\neg \phi$。
2. 双重否定除去：从$\neg \neg \phi$中可推出$\phi$。
3. 合取介入：从 $\phi$ 和 $\psi$ 中可推出 $(\phi \land \psi )$。
4. 合取除去：从 $(\phi \land \psi )$ 中可推出 $\phi$ 和 $\psi$。
5. 析取介入：从 $\phi$ 中可推出$(\phi \lor \psi )$。
6. 析取除去：从$(\phi \lor \psi )$、$(\phi \rightarrow \chi )$ 和 $(\psi \rightarrow \chi )$ 可推出 $\chi$。
7. 双条件介入：从 $(\phi \rightarrow \psi )$ 和$(\psi \rightarrow \phi )$中可推出$(\phi \leftrightarrow \psi )$。
8. 双条件除去：从 $(\phi \leftrightarrow \psi )$ 中可推出 $(\phi \rightarrow \psi )$ 和 $(\psi \rightarrow \phi )$。
9. 肯定前件（条件除去）：从 $\phi$ 和 $(\phi \rightarrow \psi )$ 中可推出 $\psi$。
10. 条件证明（条件介入）：若假定 $\phi$ 為真可證明出$\psi$，可推出 $(\phi \rightarrow \psi )$。

证明的例子

以下推导将用编号后的行的列表來表示，在每行之上有一个单一的公式和一个理由（justification）。論證的各個前提會在列表的首行給出。结论将在最后一行。一個推导稱為完备的，若所有行都是通过正确的应用一个规则而从前面的行得出的。

下面是（语法上的）证明的一个例子：
要证明：$A\rightarrow A$
证明：

编号	公式	理由
1	$A$	前提
2	$A\lor A$	析取介入自（1）
3	$(A\lor A)\land A$	合取介入自（1）和（2）
4	$A$	合取除去自（3）
5	$A\vdash A$	总结（1）到（4）
6	$\vdash A\rightarrow A$	条件证明自（5）

$A\vdash A$可解释为“假定$A$，推导出$A$”。$\vdash A\rightarrow A$为“不假定任何东西，推导出$A$蕴涵$A$”，或者“$A$蕴涵$A$是重言式”，或者“$A$蕴涵$A$是永真的”。

规则的可靠性和完备性

以上规则的关键特性是它们是可靠的和完备的。非形式的说，这意味着规则都是正确的并且不再需要其他规则。这些要求可以如下这样正式的提出。

我们定义真值指派为把命题变量映射到真或假的函数。非形式的，这种真值指派可以被理解为对事件的可能状态（或可能世界）的描述，在这里特定的陈述是真而其他为假。公式的语义因而可以被形式化，通过定义哪些"事件状态"是設定为真的。

我们通过如下规则定义这种真值指派 $A$ 在什么时候满足特定公式：

• $A$满足命题变量$P$ 当且仅当 $A(P)=$ 真
• $A$满足$\neg \phi$当且仅当$A$不满足 $\phi$
• $A$满足$(\phi \land \psi )$当且仅当$A$满足 $\phi$ 与 $\psi$ 二者
• $A$满足(φ ∨ ψ)当且仅当$A$满足 $\phi$ 和 $\psi$ 中至少一个
• $A$满足(φ → ψ)当且仅当並非$A$满足 $\phi$ 但不满足 $\psi$ 的情況
• $A$满足(φ ↔ ψ)当且仅当$A$满足 $\phi$ 与 $\psi$ 二者，或则不满足它们中的任何一个

通过这个定义，我们现在可以形式化公式 $\phi$ 被特定公式集合 $S$ 蕴涵的意义。非形式的，就是在使给定公式集合 $S$ 成立的所有可能情况下公式 $\phi$也成立。这引申出下面的形式化定义：我们说公式集合$S$ 语义蕴涵特定的公式 $\phi$，条件是满足在 $S$ 中的公式的所有真值指派也满足 $\phi$。

最后我们定义语法蕴涵，$\phi$ 被 $S$ 语法蕴涵，当且仅当我们可以在有限步骤内使用我们提出的上述推理规则推导出它。这允许我们精确的公式化推理规则的可靠性和完备性的意思：

可靠性：如果公式集合$S$语法蕴涵公式$\phi$，则$S$语义蕴涵$\phi$

完备性：如果公式集合$S$语义蕴涵公式$\phi$，则$S$语法蕴涵$\phi$

上述的兩個例子都滿足可靠性和完备性。

可靠性证明的梗概

（对于多数逻辑系统，这是相对“简单”的证明方向）

符号约定：设 $G$ 是命题集合。设$\phi$、$\psi$ 和 $\chi$ 是命題。我们把“$G$ 语法蕴涵 $\phi$ ”写成“$G$ 证明 $\phi$ ”，還有把“$G$ 语义蕴涵 $\phi$ ”写成“$G$ 蕴涵 $\phi$ ”。

我们要展示：$(\forall \phi )(\forall G)$（如果 $G$ 证明 $\phi$，则 $G$ 蕴涵 $\phi$）

我们注意到“$G$ 证明$\phi$”有一个归纳定义，这给予我们直接的办法来验证“如果 $G$ 证明 $\phi$，则……”形式的断言。所以我们的证明是用归纳法进行的。

• I.基础。验证：如果 $\phi$ 是 $G$ 的成员则 $G$ 蕴涵 $\phi$
• II.基础。验证：如果 $\phi$ 是公理，则 $G$ 蕴涵 $\phi$
• III.归纳步骤（對證明的長度 $n$ 作歸納）

（a）假定对于任意的 $G$ 和 $\phi$，如果 $G$ 在 $n$ 或更少的步數能证明 $\phi$，则 $G$ 蕴涵 $\phi$。

（b）对于在第 $n+1$ 步時，根据推理規則，由 $G$ 及其 $n$ 步以内证明的命题，可以推导出新的命题。验证：对于任意的这样的新命题 $\psi$，$G$ 蕴涵$\psi$ 。

需要注意的是，对于自然演绎系统，基础步骤II可以省略，因為它們根本没有公理。基本上，基础步骤II是要展示每个公理都是（语义上的）逻辑真理。

基础步骤证实了对于任何 $G$，来自 $G$ 的最简单的可证明的语句都被 $G$ 所蕴涵。（这是简单的，因为集合蕴涵它的任何一个成员，是個平凡的语义事實）。归纳步骤将有系统的覆盖所有的进一步的可证明的命题--通过考虑我们能够使用推理规则达成逻辑结论的每种情况--并展示如果一个新命题是可证明的，它也是在逻辑上被蕴涵的。（例如，可能有一个規則，使得从 $\phi$ 可以推导出“$\phi$ 或$\psi$ ”。在III.（a）中我们假定如果 $\phi$ 是可证明的则它也是被蕴涵的。我们也知道如果 $\phi$ 是可证明的，则“$\phi$ 或$\psi$ ”是可证明的。接着，我们必须验证“$\phi$ 或ψ”也是被蕴涵的。我们求助于语义的定义和我们所做的假定来完成。我们假定了 $\phi$ 是可以从 $G$ 证明出来的，所以它也被 $G$ 所蕴涵。所以任何使 $G$ 全部为真的指派，都使$\phi$ 为真。此外通过“或”的语义定义，使 $\phi$ 为真的任何指派都使“$\phi$ 或$\psi$ ”为真。所以任何使 $G$ 的全部为真的指派，都使“$\phi$ 或$\psi$ ”为真。所以“$\phi$ 或$\psi$ ”被蕴涵了。）一般的，归纳步骤的證明會較長，但不過是對所有推论规则按例分析，去展示每个規則都能“保持”语义蕴涵。

通过可证明性的定义，除了 $G$ 的成员、公理、或从规则推导出的命题之外，没有別的命题是可证明的；而这些命题都是语义上被蕴涵的，所以演绎演算是可靠的。

完备性证明的梗概

（这通常是相對地困难不少的证明方向。）

我们採用同上面一样的符号约定。

我们要展示：如果 $G$ 蕴涵 $\phi$ ，则 $G$ 证明 $\phi$ 。我们通过反证法来进行：我们转而展示如果 $G$ 不证明 $\phi$，则 $G$ 不蕴涵 $\phi$。

• I. 假设 $G$ 不证明 $\phi$。
• II.如果 $G$ 不证明 $\phi$，则我们可以构造一个（有限的）"最大化的集合" $G^{*}$，它是 $G$ 的超集并且不证明 $\phi$。
  • （a）把这个语言中的所有命题上加置一个“次序”。（比如，字母表次序），并把它们编号为 $E_{1},E_{2},\cdots$
  • （b）归纳的定义集合 $(G_{0},G_{1},\cdots )$的一个序列 $G_{n}$ 为如下。

（i）$G_{0}=G$。

（ii）如果 $G_{k}\cup \{E_{k+1}\}$ 证明 $\phi$ ，则 $G_{k+1}=G_{k}$。

（iii）如果 $G_{k}\cup \{E_{k+1}\}$ 不证明 $\phi$，则 $G_{k+1}=G_{k}\cup \{E_{k+1}\}$。

• • （c）定义 $G^{*}$ 为所有 $G_{n}$ 的并集。（就是说，$G^{*}$ 在任何 $G_{n}$ 中的所有命题的集合）
  • （d）可以容易地验证

（i）$G^{*}$ 包含（是其超集）$G$（通过(b.i)）；

（ii）$G^{*}$ 不证明 $\phi$（因为如果它证明 $\phi$，则某些命题被增加到某个 $G_{n}$ 上而导致它证明了 $\phi$；但是这被定义所排除）；

（iii）$G^{*}$ 是（关于 $\phi$）"最大化的集合"：如果任何更多的命题不管怎样的被增加到$G^{*}$，它就会证明 $\phi$。（因为如果有可能增加任何更多的命题，再次根据定义，在构造 $G_{n}$ 期间被遇到的时候它们就应当已经被增加进去了。）

• III.如果 $G^{*}$ 是（关于 $\phi$ ）的最大化集合，则它是"类真理的"。这意味着它包含命题 $\psi$，只在它不包含 $\neg \psi$ 的命题的条件下；如果它包含 $\psi$ 并且包含“如果$\psi$ 则 $\chi$”，则它也包含 $\chi$；以此类推。
• IV.如果 $G^{*}$ 是类真理的，则有“$G^{*}$-规范”的指派：它使在$G^{*}$ 中每个命题为真而在$G^{*}$ 之外的所有命题为假，而仍然遵守在这个语言的语义合成的法则。
• V. $G^{*}$-规范的命题将使我们最初的集合 $G$ 中的命题全部为真，而使 $\phi$ 为假。
• VI.如果有在 $G$ 其上是真而 $\phi$ 是假的指派，则 $G$ 不（语义上）蕴涵 $\phi$。Q.E.D.

公理化演算

下面定义的命题演算通过公理的方式定义了多数逻辑算子的语法并且它只使用一个推理规则。它也叫做标准命题演算。

公理

设 $\phi$ 、$\chi$ 和 $\psi$ 表示合式公式。（wff自身将不包含任何希腊字母，而只包含大写罗马字母、连结算子和圆括号）。公理有

• THEN-1：$\phi \rightarrow (\chi \rightarrow \phi )$
• THEN-2：$(\phi \rightarrow (\chi \rightarrow \psi ))\rightarrow ((\phi \rightarrow \chi )\rightarrow (\phi \rightarrow \psi ))$
• AND-1：$\phi \land \chi \rightarrow \phi$
• AND-2：$\phi \land \chi \rightarrow \chi$
• AND-3：$\phi \rightarrow (\chi \rightarrow (\phi \land \chi ))$
• OR-1：$\phi \rightarrow \phi \lor \chi$
• OR-2：$\chi \rightarrow \phi \lor \chi$
• OR-3：$(\phi \rightarrow \psi )\rightarrow ((\chi \rightarrow \psi )\rightarrow (\phi \lor \chi \rightarrow \psi ))$
• NOT-1：$(\phi \rightarrow \chi )\rightarrow ((\phi \rightarrow \neg \chi )\rightarrow \neg \phi )$
• NOT-2：$\phi \rightarrow (\neg \phi \rightarrow \chi )$
• NOT-3：$\phi \lor \neg \phi$

公理THEN-2可以被看作是“蕴涵关于蕴涵的分配律”。公理AND-1和AND-2对应于“合取除去”。在AND-1和AND-2之间的关系反映了合取算子的交换律。公理AND-3对应于“合取介入”。公理OR-1和OR-2对应于“析取介入”。在OR-1和OR-2之间的关系反映了析取算子的交换律。公理NOT-1对应于反证法。公理NOT-2说明了“从矛盾中可以推导出任何东西”。公理NOT-3叫做排中律（拉丁语tertium non datur：“排除第三者”）并反映了命题公式的语义求值：公式的真值要么是真要么是假。至少在经典逻辑中，没有第三个真值。直觉逻辑不接受公理NOT-3。

推理规则

推理规则是肯定前件：

• $\phi ,\ \phi \rightarrow \chi \vdash \chi$.

如果还使用双箭头的等价算子的话，则要增加如下"自然"推理规则：

• IFF-1：$\phi \leftrightarrow \chi \vdash \chi \rightarrow \phi$
• IFF-2：$\phi \rightarrow \chi ,\ \chi \rightarrow \phi \vdash \phi \leftrightarrow \chi$

元推理规则

设一個推導被表示为相继式，各個假设在十字转门（turnstile）的左侧，而结论在十字转门的右侧。则演绎定理可以被陈述如下：

如果相继式

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi$

已经被证明了，则也有可能证明相继式

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \rightarrow \psi$。

这个演绎定理（DT）自身没有公式化为命题演算：它不是命题演算的定理，而是关于命题演算的一个定理。在这个意义上，它是元定理，相当于关于命题演算可靠性和完备性的定理。

在另一方面，DT对於简化语法上的证明过程是如此的有用以至于它看作和用做推理规则，同肯定前件一起使用。在这个意义上，DT对应于自然条件证明推理规则，它是在本條目中提出的第二个例子的命题演算的一部分。

DT的逆定理也是有效的：

如果相继式

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \rightarrow \psi$

已经被证明了，则也有可能证明相继式

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi$

实际上，DT的逆定理的有效性相对于DT而言是平凡的：

如果

$\phi _{1},\ ...,\ \phi _{n}\vdash \chi \rightarrow \psi$

则

1：$\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi \rightarrow \psi$

2：$\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi$

并且可以演绎自（1）和（2）

3：$\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \psi$

通过肯定前件的方式，Q.E.D.

DT的逆命题有着强有力的蕴涵：它可以用来把公理转换成推理规则。例如，公理AND-1

$\vdash \phi \wedge \chi \rightarrow \phi$

可以通过演绎定理的逆定理的方式被转换成推理规则

$\phi \wedge \chi \vdash \phi$

这是合取除去，是前面给出的自然演绎命题演算中使用的十个推理规则中的一个。

证明的例子

下面是（语法上）证明的一个例子，只涉及到公理THEN-1和THEN-2：
要证明：$A\rightarrow A$（蕴涵的自反性）。
证明：

1.$(A\rightarrow ((B\rightarrow A)\rightarrow A))\rightarrow ((A\rightarrow (B\rightarrow A))\rightarrow (A\rightarrow A))$

公理THEN-2通过$\phi =A$, $\chi =B\rightarrow A$, $\psi =A$

2. $A\rightarrow ((B\rightarrow A)\rightarrow A)$

公理THEN-1通过$\phi =A$, $\chi =B\rightarrow A$

3.$(A\rightarrow (B\rightarrow A))\rightarrow (A\rightarrow A)$

得自（1）和（2）通过肯定前件。

4. $A\rightarrow (B\rightarrow A)$

公理THEN-1通过$\phi =A$, $\chi =B$

5. $A\rightarrow A$

得自（3）和（4）通过肯定前件。

等价于等式逻辑

前面的公理化命题演算是希尔伯特风格演绎系统的一个例子。在这种命题系统中公理是用逻辑连结词構建的项，而唯一的推理规则是肯定前件。等式逻辑在高等学校的抽象代数教学中被作为正式的标准，它是不同于希尔伯特系统的一类不同的演算。它的定理是等式而它的推理规则表达出等號的性质，也就是在容许代换的项上的相等关系。

上述的经典命题演算等价于布尔代数，而直觉命题演算等价于海廷代数。等价性是通过在两个方向上转换各自系统的定理来证明的。经典命题演算或直觉命题演算的定理Φ被分别转换为布尔代数或Heyting代数的等式 $\Phi =1$。反过来布尔代数或Heyting代数的定理 $x=y$ 被分别转换为定理经典名义演算或直觉命题演算的定理 $(x\rightarrow y)\land (y\rightarrow x)$，它的标准简写是 $x\equiv y$。在布尔代数的情况下，$x=y$ 还可以被转换为 $(x\land y)\lor (\neg x\land \neg y)$，但在直觉命题演算的情况下中不能这么转换。

在布尔代数和Heyting代数中，可以使用不等式 $x\leq y$ 代替等式。等式 $x=y$ 可以被表达为一对不等式 $x\leq y$ 和 $y\leq x$。反过来不等式 $x\leq y$ 可被表达为等式 $x\land y=x$ 或$x\lor y=y$。不等式的重要性在于它对应于希尔伯特系统的演绎或蕴涵符号$\vdash$。蕴涵

$\phi _{1},\ \phi _{2},\ldots ,\ \phi _{n}\vdash \psi$

被转换为代数框架下的不等式

$\phi _{1}\ \land \ \phi _{2}\ \land \ \ldots \ \land \ \phi _{n}\ \ \leq \ \ \psi$

反过来代数不等式 $x\leq y$ 被转换为蕴涵

$x\ \vdash \ y$

在实质条件（implication）$x\rightarrow y$ 和不等式或者蕴涵（entailment）$x\leq y$ 或 $x\ \vdash \ y$ 之间的区别在于，前者是内在于逻辑的，而后者是外在的。在两个项之间内在的实质条件是同类的另一个项。在两个项之间的外在的蕴涵表达了在逻辑语言之外的元真理，并被认为是元语言的一部分。即使所研究的逻辑是直觉的，蕴涵都通常经典的理解为二值的：要么左侧蕴涵（或小于等于）右侧，要么不蕴涵之。

同代数逻辑之间类似但更加复杂的相互转换，对于自然演绎系统和相继式演算也是可能的。后者的转换可以被释义为二值的，但是更有洞察力的释义是作为集合，它的元素可以被理解为由范畴的态射组成的抽象证明。在这种释义下相继式演算的切规则对应于范畴的复合。

其他逻辑演算

命题演算大概是在所有当前使用的逻辑演算中最简单的一种。（亚里士多德的“三段论”演算，在现代逻辑中在很大程度上被替代了，它与命题逻辑相比在某些方面更简单--但在其他方面更加复杂）。它可以按很多方式来扩展。

最直接的方式是开发一个更加复杂的逻辑演算，介入对所用于的句子的更精细的细节敏感的规则。在命题逻辑中的原子句子被分解成项、变量、谓词和量词的时候，它们就生成了一阶逻辑，或者叫做一阶谓词逻辑，它保留命题逻辑的所有规则并增加了一些新规则。（例如，从“所有的狗都是动物”我们可以推出“如果Rover是狗，则Rover是动物”）。

通过一阶逻辑的工具，有可能公式化一些理论，要么带有显式的公理要么通过推理规则，而把它们自身当作逻辑演算。算术是其中最周知的理论；其他的还包括集合论和分体论。

模态逻辑也提供了一种推理的变体，它不能在命题演算中捕获。例如，从“必然地p”我们可以推出p。从p我们可以推出“可能地p”。

多值逻辑是允许句子有除了“真”和“假”之外的值的逻辑。（例如，“都不”和“都是”是标准的“额外值”；“连续统逻辑”允许每个句子有任何的在“真”和“假”之间的表示“真实程度”的无限个值）。这些逻辑经常要求与命题逻辑非常不同的运算设备。

参见

• 逻辑
• 零阶逻辑
• 演绎推理
• 希尔伯特演绎系统
• 自然演绎
• 推理规则列表
• 相继式演算
• 布尔逻辑
• 布尔代数
• 一階邏輯

引用

• Brown, Frank Markham(2003), Boolean Reasoning: The Logic of Boolean Equations, 1st edition, Kluwer Academic Publishers, Norwell, MA. 2nd edition, Dover Publications, Mineola, NY.
• Chang, C.C., and Keisler, H.J.(1973), Model Theory, North-Holland, Amsterdam, Netherlands.
• Kohavi, Zvi(1978), Switching and Finite Automata Theory, 1st edition, McGraw–Hill, 1970. 2nd edition, McGraw–Hill, 1978.
• Korfhage, Robert R.(1974), Discrete Computational Structures, Academic Press, New York, NY.
• Lambek, J. and Scott, P.J.(1986), Introduction to Higher Order Categorical Logic, Cambridge University Press, Cambridge, UK.
• Mendelson, Elliot(1964), Introduction to Mathematical Logic, D. Van Nostrand Company.

外部链接

• Klement, Kevin C. (2006), "Propositional Logic", in James Fieser and Bradley Dowden(eds.), Internet Encyclopedia of Philosophy, Eprint（页面存档备份，存于互联网档案馆）.
• Introduction to Mathematical Logic（页面存档备份，存于互联网档案馆）
• Elements of Propositional Calculus
• forall x: an introduction to formal logic（页面存档备份，存于互联网档案馆）, by P.D. Magnus, covers formal semantics and proof theory for sentential logic.
• Propositional Logic (GFDLed)