查看“︁命题逻辑”︁的源代码

{{NoteTA
|G1 = IT
|G2 = Math
}}
'''命题逻辑'''是[[逻辑学]]的一个分支。<ref>{{cite book|url=http://plato.stanford.edu/archives/spr2016/entries/logic-ancient/|title=The Stanford Encyclopedia of Philosophy|first=Susanne|last=Bobzien|editor-first=Edward N.|editor-last=Zalta|date=1 January 2016|via=Stanford Encyclopedia of Philosophy|access-date=2023-07-08|archive-date=2019-03-18|archive-url=https://web.archive.org/web/20190318132519/https://plato.stanford.edu/archives/spr2016/entries/logic-ancient/|dead-url=no}}</ref> 它也称为'''命題演算'''、'''句子演算'''、'''句子逻辑'''，有时也称为'''[[零阶逻辑]]'''。它涉及[[命题]]（可以是真或假）和[[命题]]之间的关系，包括基于它们的论证的构建。复合命题是通过逻辑连接词连接[[命题]]而形成的。不包含逻辑连接词的命题称为'''原子命题'''。  与[[一阶逻辑]]不同，命题逻辑不处理非逻辑对象、以及关于它们的[[谓词]]或[[量词]]。然而，命题逻辑的所有机制都包含在[[一阶逻辑]]和[[高阶逻辑]]中。从这个意义上说，命题逻辑是[[一阶逻辑]]和[[高阶逻辑]]的基础。

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

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

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

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

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

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

==命题演算的一般描述==

'''命题演算'''是一個[[形式系统]]<math>\mathcal{L} = \mathcal{L}\ (\Alpha,\ \Omega,\ \Zeta,\ \Iota)</math>，它的公式按如下方式构造：

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

* <math>\Omega\!</math>是名為「[[算子|算子符號]]」或「[[邏輯運算符]]」之元素所組成的有限集合。集合<math>\Omega\!</math>被[[集合劃分|劃分]]成如下等不相交的子集：

::: <math>\Omega = \Omega_0 \cup \Omega_1 \cup \ldots \cup \Omega_j \cup \ldots \cup \Omega_m \,</math>。

:在此一劃分中，<math>\Omega_j\!</math>是指[[元數]]為<math>j\!</math>的算子符號所構成的集合。

:在更熟知的命题演算中，<math>\Omega\!</math>一般被劃分如下：

::: <math>\Omega_1 = \{ \lnot \} \,,</math>

::: <math>\Omega_2 \subseteq \{ \land, \lor, \rightarrow, \leftrightarrow \} \,</math>。

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

:::<math>\Omega_0 = \{\top,\ \bot \} \,</math>。

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

* <math>\Zeta\!</math> 集合是「轉換規則」（當作為邏輯應用時則稱之為「[[推理規則]]」）之所構成的有限集合。<math>\Zeta\!</math>集合的「轉換規則」是用「[[原子公式]]」和「[[邏輯運算符]]」構成的。

* <math>\Iota\!</math> 是「起始點」（當得到邏輯解釋時則稱之為「[[公理]]」）所構成的有限集合。


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

<math>\mathcal{L}</math>的語言，亦稱之為「公式」或「[[合式公式]]」的集合，可由如下規則集合被[[数学归纳法|归纳]]或[[遞迴]]地定義：

# 基本元素：<math>\Alpha\!</math>內的任何元素都是<math>\mathcal{L}</math>的公式。
# 如果 <math>p_1, p_2, \ldots, p_j</math> 是公式 和 <math>f</math> 属于 <math>\Omega_j</math>, 则 <math>\left( f p_1 p_2 \ldots p_j \right)</math> 也是公式.
# 封閉性：其他都不會是<math>\mathcal{L}</math>的公式。

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

* 依规则1，p是公式。
* 依规则2，¬p是公式。
* 依规则1，q是公式。
* 依规则2，(¬p ∨ q)是公式。

== 示例 1  简单的公理系统==
设<math>\mathcal{L}_1 = \mathcal{L}\ (\Alpha,\ \Omega,\ \Zeta,\ \Iota)</math>，这里的<math>\Alpha,\ \Omega,\ \Zeta,\ \Iota</math>定义如下：

* <math>\Alpha \!</math>是個含有足夠多元素以應付討論所需的有限集合，如：

::: <math>\Alpha = \{p, q, r, s, t, u \} \,</math>。
功能齐全的套装 逻辑运算符（逻辑连接词和否定）的Ω如下。

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

採用否定和薀涵做為命題演算的兩個基本運算，相當於把omega集<math>\Omega = \Omega_1 \cup \Omega_2</math>劃分如下：

::: <math>\Omega_1 = \{ \lnot \} \,</math>。

::: <math>\Omega_2 = \{ \rightarrow \} \,</math>。

*  <math>\Iota\!</math> 公理系統集合。 有一個公理系統是[[扬·武卡谢维奇]]所發現的，而這系統可以如下地公式化為此語言中的命題演算。各個公理都是由下列的公理模式作代換所得。
::* <math>p \to(q \to p)</math>

::* <math>(p \to (q \to r)) \to((p \to q) \to(p \to r))</math>

::* <math>(\neg p \to \neg q) \to(q \to p)</math>

* <math>\Zeta\!</math> 推理規則集合。 其推理規則為[[肯定前件]]（即可由p和(p → q)導出q）。而a ∨ b和a ∧ b則是分別被定義為¬a → b和¬(a → ¬b)。

== 示例 2  自然演绎系統 ==

设<math>\mathcal{L}_2 = \mathcal{L}\ (\Alpha,\ \Omega,\ \Zeta,\ \Iota)</math>，这里的<math>\Alpha,\ \Omega,\ \Zeta,\ \Iota</math>定义如下：

* <math>\Alpha \!</math>是個含有足夠多元素以應付討論所需的有限集合，如：

::: <math>\Alpha = \{p, q, r, s, t, u \} \,</math>。

* <math>\Omega = \Omega_1 \cup \Omega_2</math>划分为如下：

::: <math>\Omega_1 = \{ \lnot \} \,</math>。

::: <math>\Omega_2 = \{ \land, \lor, \rightarrow, \leftrightarrow \} \,</math>。

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

* 起始点的集合是空的，亦即<math>\Iota = \varnothing \,</math>。

* 轉换规则的集合<math>\Zeta\!</math>描述如下：

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

# {{le|否定介入|Negation introduction}}：從φ → ¬ ψ和φ → ψ中可推出¬ φ。
# [[双重否定除去]]：从¬ ¬ φ中可推出φ。
# {{le|合取介入|Conjunction introduction}}：从φ和ψ中可推出(φ ∧ ψ)。
# {{le|合取除去|Conjunction elimination}}：从(φ ∧ ψ)中可推出φ和ψ。
# {{le|析取介入|Disjunction introduction}}：从φ中可推出(φ ∨ ψ)。
# {{le|析取除去|Disjunction elimination}}：从(φ ∨ ψ)、(φ → χ)和(ψ → χ)可推出χ。
# {{le|双条件介入|Biconditional introduction}}：从(φ → ψ)和(ψ → φ)中可推出(φ ↔ ψ)。
# {{le|双条件除去|Biconditional elimination}}：从(φ ↔ ψ)中可推出(φ → ψ)和(ψ → φ)。
# [[肯定前件]]（条件除去）：从φ和(φ → ψ)中可推出ψ。
# [[条件证明]]（条件介入）：若假定φ為真可證明出ψ，可推出(φ → ψ)。

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

下面是（语法上的）证明的一个例子：<br>
'''要证明：'''<math>A \rightarrow A</math> <br>
'''证明：'''<br>
:{| class="wikitable"
! style="background:#93D7AE;"| 编号
! style="background:#93D7AE;"| 公式
! style="background:#93D7AE;"| 理由
|-
| 1 || A || 前提
|-
| 2 || A∨A || 析取介入自（1）
|-
| 3 || (A∨A)∧A || 合取介入自（1）和（2）
|-
| 4 || A || 合取除去自（3）
|-
| 5 || A <math>\vdash \,</math> A || 总结（1）到（4）
|-
| 6 || <math> \vdash \,</math> A→A || 条件证明自（5）
|}

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

== 规则的可靠性和完备性 ==

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

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

我们通过如下规则定义这种真值指派A在什么时候满足特定公式：
* A满足命题变量P [[当且仅当]]A(P) = '''真'''
* A满足¬ φ当且仅当A不满足φ
* A满足(φ ∧ ψ)当且仅当A满足φ与ψ二者
* A满足(φ ∨ ψ)当且仅当A满足φ和ψ中至少一个
* A满足(φ → ψ)当且仅当並非A满足φ但不满足ψ的情況
* A满足(φ ↔ ψ)当且仅当A满足φ与ψ二者，或则不满足它们中的任何一个

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

最后我们定义'''语法蕴涵'''，φ被S语法蕴涵，当且仅当我们可以在有限步骤内使用我们提出的上述推理规则推导出它。这允许我们精确的公式化推理规则的可靠性和完备性的意思：
; '''可靠性'''：如果公式集合S语法蕴涵公式φ，则S语义蕴涵φ
; '''完备性'''：如果公式集合S语义蕴涵公式φ，则S语法蕴涵φ
上述的兩個例子都滿足可靠性和完备性。

=== 可靠性证明的梗概 ===

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

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

我们要展示：(∀φ)(∀G)(如果G证明φ，则G蕴涵φ)

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

*I.基础。验证：如果φ是G的成员则G蕴涵φ
*II.基础。验证：如果φ是公理，则G蕴涵φ
*III.归纳步骤（對證明的長度n作歸納）
::（a）假定对于任意的G和φ，如果G在n或更少的步數能证明φ，则G蕴涵φ。
::（b）对于在第n+1步時，根据推理規則，由G及其n步以内证明的命题，可以推导出新的命题。验证：对于任意的这样的新命题ψ，G蕴涵ψ。

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

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

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

=== 完备性证明的梗概 ===

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

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

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

*I. 假设G不证明φ。
*II.如果G不证明φ，则我们可以构造一个（有限的）"最大化的集合" G*，它是G的超集并且不证明φ。
**（a）把这个语言中的所有命题上加置一个“次序”。（比如，字母表次序），并把它们编号为E<sub>1</sub>, E<sub>2</sub>, ...
**（b）归纳的定义集合(G<sub>0</sub>, G<sub>1</sub>, ...)的一个序列G<sub>n</sub>为如下。
:::（i）G<sub>0</sub>=G。 
:::（ii）如果G<sub>k</sub> ∪ {E<sub>k+1</sub>}证明φ，则G<sub>k+1</sub>=G<sub>k</sub>。
:::（iii）如果G<sub>k</sub> ∪ {E<sub>k+1</sub>}不证明φ，则G<sub>k+1</sub>=G<sub>k</sub> ∪ {E<sub>k+1</sub>}。
**（c）定义G* 为所有G<sub>n</sub>的并集。（就是说，G* 在任何G<sub>n</sub>中的所有命题的集合）
**（d）可以容易地验证
:::（i）G* 包含（是其超集）G（通过(b.i)）；
:::（ii）G* 不证明φ（因为如果它证明φ，则某些命题被增加到某个G<sub>n</sub>上而导致它证明了φ；但是这被定义所排除）；
:::（iii）G* 是（关于φ）"最大化的集合"：如果任何更多的命题不管怎样的被增加到G*，它就会证明φ。（因为如果有可能增加任何更多的命题，再次根据定义，在构造G<sub>n</sub>期间被遇到的时候它们就应当已经被增加进去了。）
*III.如果G* 是（关于φ）的最大化集合，则它是"类真理的"。这意味着它包含命题ψ，只在它不包含¬ψ的命题的条件下；如果它包含ψ并且包含“如果ψ则χ”，则它也包含χ；以此类推。
*IV.如果G* 是类真理的，则有“G*-规范”的指派：它使在G* 中每个命题为真而在G* 之外的所有命题为假，而仍然遵守在这个语言的语义合成的法则。
*V. G*-规范的命题将使我们最初的集合G中的命题全部为真，而使φ为假。
*VI.如果有在G其上是真而φ是假的指派，则G不（语义上）蕴涵φ。[[Q.E.D.]]

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

=== 公理 ===
设φ、χ和ψ表示合式公式。（wff自身将不包含任何希腊字母，而只包含大写罗马字母、连结算子和圆括号）。公理有
* THEN-1：φ →(χ → φ)
* THEN-2：(φ → (χ → ψ)) →((φ → χ)→(φ → ψ))
* AND-1：φ ∧ χ → φ
* AND-2：φ ∧ χ → χ
* AND-3：φ →(χ → (φ ∧ χ))
* OR-1：φ → φ ∨ χ
* OR-2：χ → φ ∨ χ
* OR-3：(φ → ψ)→((χ → ψ)→(φ ∨ χ → ψ))
* NOT-1：(φ → χ)→((φ → ¬ χ)→ ¬ φ)
* NOT-2：φ →(¬ φ → χ)
* NOT-3：φ ∨ ¬ φ

公理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叫做[[排中律]]（[[拉丁语]]{{lang|la|tertium non datur}}：“排除第三者”）并反映了命题公式的语义求值：公式的真值要么是真要么是假。至少在经典逻辑中，没有第三个真值。[[直觉逻辑]]不接受公理NOT-3。

=== 推理规则 ===
推理规则是[[肯定前件]]：
* <math> \phi, \ \phi \rightarrow \chi \vdash \chi </math>.
如果还使用双箭头的等价算子的话，则要增加如下"自然"推理规则：
* IFF-1：<math> \phi \leftrightarrow \chi \vdash \chi \rightarrow \phi </math>
* IFF-2：<math> \phi \rightarrow \chi, \ \chi \rightarrow \phi \vdash \phi \leftrightarrow \chi </math>

=== 元推理规则 ===
设一個推導被表示为[[相继式]]，各個假设在十字转门（turnstile）的左侧，而结论在十字转门的右侧。则[[演绎定理]]可以被陈述如下：
:如果相继式
::<math> \phi_1, \ \phi_2, \ ... , \ \phi_n, \ \chi \vdash \psi </math>
:已经被证明了，则也有可能证明相继式
::<math> \phi_1, \ \phi_2, \ ..., \ \phi_n \vdash \chi \rightarrow \psi </math>。

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

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

DT的逆定理也是有效的：
:如果相继式
::<math> \phi_1, \ \phi_2, \ ..., \ \phi_n \vdash \chi \rightarrow \psi </math>
:已经被证明了，则也有可能证明相继式
::<math> \phi_1, \ \phi_2, \ ... , \ \phi_n, \ \chi \vdash \psi </math>
实际上，DT的逆定理的有效性相对于DT而言是平凡的：
:如果
:: <math> \phi_1, \ ... , \ \phi_n \vdash \chi \rightarrow \psi </math>
:则
:: 1：<math> \phi_1, \ ... , \ \phi_n, \ \chi \vdash \chi \rightarrow \psi </math>
:: 2：<math> \phi_1, \ ... , \ \phi_n, \ \chi \vdash \chi </math>
:并且可以演绎自（1）和（2）
:: 3：<math> \phi_1, \ ... , \ \phi_n, \ \chi \vdash \psi </math>
:通过肯定前件的方式，Q.E.D.

DT的逆命题有着强有力的蕴涵：它可以用来把公理转换成推理规则。例如，公理AND-1
: <math> \vdash \phi \wedge \chi \rightarrow \phi </math>
可以通过演绎定理的逆定理的方式被转换成推理规则
: <math> \phi \wedge \chi \vdash \phi </math>
这是[[合取除去]]，是前面给出的自然演绎命题演算中使用的十个推理规则中的一个。

=== 证明的例子 ===
下面是（语法上）证明的一个例子，只涉及到公理THEN-1和THEN-2：<br>
'''要证明：'''A → A（蕴涵的自反性）。<br>
'''证明：''' 
:1.(A → ((B → A)→ A)) →((A → (B → A)) →(A → A))     
::公理THEN-2通过φ = A, χ = B → A, ψ = A
:2. A →((B → A)→ A)
::公理THEN-1通过φ = A, χ = B → A
:3.(A → (B → A)) →(A → A)
::得自（1）和（2）通过肯定前件。
:4. A →(B → A)    
::公理THEN-1通过φ = A, χ = B
:5. A → A
::得自（3）和（4）通过肯定前件。

==等价于等式逻辑==

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

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

在布尔代数和Heyting代数中，可以使用不等式x ≤ y代替等式。等式x = y可以被表达为一对不等式x ≤ y和y ≤ x。反过来不等式x ≤ y可被表达为等式x∧y = x或x∨y = y。不等式的重要性在于它对应于希尔伯特系统的演绎或蕴涵符号<math>\vdash</math>。蕴涵
::<math> \phi_1, \ \phi_2, \ldots, \ \phi_n \vdash \psi </math>

被转换为代数框架下的不等式
::<math> \phi_1\ \land\ \phi_2\ \land\ \ldots\ \land \ \phi_n\ \ \le\ \ \psi </math>

反过来代数不等式x ≤ y被转换为蕴涵
::<math>x\ \vdash\ y</math>

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

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

== 其他逻辑演算 ==

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

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

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

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

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

==参见==
{{div col|4}}
*[[逻辑]]
*[[零阶逻辑]]
* [[演绎推理]]
* [[希尔伯特演绎系统]]
* [[自然演绎]]
* {{link-en|推理规则列表|List of rules of inference}}
* [[相继式演算]]
* [[布尔逻辑]]
* [[布尔代数]]
* [[一階邏輯]]
{{div col end}}

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

== 外部链接 ==
* [[Kevin C. Klement|Klement, Kevin C.]] (2006), "Propositional Logic", in James Fieser and Bradley Dowden(eds.), [[Internet Encyclopedia of Philosophy]], [http://www.iep.utm.edu/p/prop-log.htm Eprint]{{Wayback|url=http://www.iep.utm.edu/p/prop-log.htm |date=20090508160150 }}.
* [http://www.ltn.lv/~podnieks/mlog/ml2.htm Introduction to Mathematical Logic]{{Wayback|url=http://www.ltn.lv/~podnieks/mlog/ml2.htm |date=20200321024306 }}
* [https://web.archive.org/web/20060905025800/http://www.visualstatistics.net/Scaling/Propositional%20Calculus/Elements%20of%20Propositional%20Calculus.htm Elements of Propositional Calculus]
* [http://www.fecundity.com/logic/ forall x: an introduction to formal logic]{{Wayback|url=http://www.fecundity.com/logic/ |date=20100908125101 }}, by P.D. Magnus, covers formal semantics and proof theory for sentential logic.
* [[PlanetMath:3475|Propositional Logic]] ([[GNU自由文档许可证|GFDL]]ed)

==參考資料== 
{{Reflist|2}} 

{{-}}
{{逻辑联结词}}
{{数理逻辑|state=expanded}}

[[Category:邏輯]]
[[Category:數理邏輯|M]]
[[Category:形式逻辑系统]]
[[Category:命题演算]]