命题演算

在邏輯和數學裡，**命題演算**（或稱**句子演算**）是一個形式系統，有著可以由以邏輯運算子結合原子命題來構成代表「命題」的公式，以及允許某些公式建構成「定理」的一套形式「證明規則」。

## 術語

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

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

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

命題運算的語言包括：（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 \}\,$ 。

　
: 有些作者會用～來替代 ¬，也有的用 & 或 $\cdot $ 來取替 $\land $ 。邏輯值所構成的集合也有許多不同的符號表示，如 {假，真} 、{F,T} 或 {0,1} 來取替 { $\bot $ , $\top $ }，這些都常見於各個論著之中。

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

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

1. 基本元素： $\mathrm {A} \!$ 內的任何元素都是 ${\mathcal {L}}$ 的公式。
2. 步驟（a）：如果 p 是公式，則 ¬p 也會是公式。
3. 步驟（b）：如果 p 和 q 是公式，則 ( $\,\!p$ $\land $ $\,\!q$ )、( $\,\!p$ $\lor $ $\,\!q$ )、( $p\,\!\rightarrow q\,\!$ ) 和 ( $\,\!p\leftrightarrow q\,\!$ ) 也都會是公式。
4. 封閉性：其他都不會是 ${\mathcal {L}}$ 的公式。

透過重複應用這三個規則，可以建構出複雜的公式來。例如：

1. 依規則 1，p 是公式。
2. 依規則 2，¬p 是公式。
3. 依規則 1，q 是公式。
4. 依規則 3，(¬p ∨ q) 是公式。
 * $\mathrm {Z} \!$ 集合是「轉換規則」（當作為邏輯應用時則稱之為「推理規則」）之所構成的有限集合。 $\mathrm {Z} \!$ 集合的「轉換規則」是用「原子公式」和「邏輯運算子」構成的。
 * $\mathrm {I} \!$ 是「起始點」（當得到邏輯解釋時則稱之為「公理」）所構成的有限集合。

## 例子

### 簡單的公理系統

設 ${\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\}\,$ 。

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

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

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

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

有一個公理系統是揚・武卡謝維奇所發現的，而這系統可以如下地公式化為此語言中的命題演算。各個公理都是由下列的公理模式作代換所得。

　
: : * $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)$

其推理規則為肯定前件（即可由 p 和 (p → q) 導出 q）。而 a ∨ b 和 a ∧ b 則是分別被定義為 ¬a → b 和 ¬(a → ¬b)。

### 自然演繹系統

設 ${\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）推理，這意味著在規則的前提中，我們可以臨時的假定一個（未證明的）假設作為推導出的公式集合的一部分，來檢視我們是否能推導出一個特定的其他公式。因為前九個規則不是這樣而通常被描述為「非假言」規則，而最後一個則被稱為「假言」規則。

**否定介入：從 φ → ¬ ψ 和 φ → ψ 中可推出 ¬ φ。**
**雙重否定除去：從 ¬ ¬ φ 中可推出 φ。**
**合取介入：從 φ 和 ψ 中可推出 (φ ∧ ψ)。**
**合取除去：從 (φ ∧ ψ) 中可推出 φ 和 ψ。**
**析取介入：從 φ 中可推出 (φ ∨ ψ)。**
**析取除去：從 (φ ∨ ψ)、(φ → χ) 和 (ψ → χ) 可推出 χ。**
**雙條件介入：從 (φ → ψ) 和 (ψ → φ) 中可推出 (φ ↔ ψ)。**
**雙條件除去：從 (φ ↔ ψ) 中可推出 (φ → ψ) 和 (ψ → φ)。**
**肯定前件（條件除去）：從 φ 和 (φ → ψ) 中可推出 ψ。**
**條件證明（條件介入）：若假定 φ 為真可證明出 ψ，可推出 (φ → ψ)。**

#### 證明的例子

以下推導將用編號後的行的列表來表示，在每行之上有一個單一的公式和一個理由（justification）。論證的各個前提會在列表的首行給出。結論將在最後一行。一個推導稱為完備的，若所有行都是通過正確的應用一個規則而從前面的行得出的。

下面是（語法上的）證明的一個例子： 
**要證明：** $A\rightarrow A$ 
**證明：** 

　
:

 $A\vdash A$ 可解釋為「假定 A，推導出 A」。 $\vdash A\rightarrow A$ 為「不假定任何東西，推導出 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）把這個語言中的所有命題上加置一個「次序」。（比如，字母表次序），並把它們編號為 E1, E2, ...
  * （b）歸納的定義集合 (G0, G1, ...) 的一個序列 Gn 為如下。

　
: : : （i）G0=G。

　
: （ii）如果 Gk ∪ {Ek+1} 證明 φ，則 Gk+1=Gk。

　
: （iii）如果 Gk ∪ {Ek+1} 不證明 φ，則 Gk+1=Gk ∪ {Ek+1}。

* * （c）定義 G\* 為所有 Gn 的聯集。（就是說，G\* 在任何 Gn 中的所有命題的集合）
  * （d）可以容易地驗證

　
: : : （i）G\* 包含（是其超集）G（通過 (b.i)）；

　
: （ii）G\* 不證明 φ（因為如果它證明 φ，則某些命題被增加到某個 Gn 上而導致它證明了 φ；但是這被定義所排除）；

　
: （iii）G\* 是（關於 φ）"最大化的集合"：如果任何更多的命題不管怎樣的被增加到 G\*，它就會證明 φ。（因為如果有可能增加任何更多的命題，再次根據定義，在構造 Gn 期間被遇到的時候它們就應當已經被增加進去了。）

* 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 叫做排中律（拉丁語 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 → A（蘊涵的自反性）。 
**證明：**

　
: 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。不等式的重要性在於它對應於希爾伯特系統的演繹或蘊涵符號 $\vdash $ 。蘊涵

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

被轉換為代數框架下的不等式

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

反過來代數不等式 x ≤ y 被轉換為蘊涵

　
: : $x\ \vdash \ y$

在實質條件（implication）x → y 和不等式或者蘊涵（entailment）x ≤ 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)