命題邏輯

命題邏輯是指以邏輯運算符結合原子命題來構成代表“命題”的公式，以及允許某些公式建構成“定理”的一套形式“證明規則”。相對於謂詞邏輯，它是量化的並且它的原子公式是謂詞函式；和模態邏輯，它可以是非真值泛函的。

演算是用來證明有效的公式（就是說它的定理）和論證（argument）的邏輯系統。它是公理或公理模式的集合（它可以為空或是可數無限集合），和推導有效的推理的推理規則。形式文法（或語法）遞歸定義語言的表達式和合式公式（well-formed formula 經常縮寫為wff）。此外給出定義真值和求值（或釋義）的語義。它允許我們確定哪個 wff 是有效的（也就是定理）。

簡介

在命題演算中語言由命題變數（或者叫占位符（placeholder））和句子/判決運算元（或者叫連結詞）。wff 是任何原子公式或在句子操作符之上建造的公式。

在下文中我們描述一種標準命題演算。很多不同的公式系統存在，它們都或多或少等價但在下列方面不同：⑴它們的語言（就是說哪些操作符和變數是語言的一部分）； ⑵ 它們有哪些（如果有的話）公理； ⑶採用了哪些推理規則。

文法

語言的構成：

字母表的大寫字母，表示命題變數。它們是原子公式。慣例上，使用拉丁字母（A,B,C）或希臘字母（χ，φ，ψ），但是不能混合使用。

表示連結詞（connective)（或邏輯運算元）的符號： &not；、∧、∨、→、?。（我們可以使用更少的運算元（和相應的符號），因為一些運算元是簡寫形式 — 例如，P → Q 等價於 ¬ P ∨ Q）。

左右圓括弧： （，）。

合式公式（wff）的集合右如下規則遞歸的定義：

基礎： 字母表的字母（通常是大寫的，如A、B、φ、χ 等）是 wff。

歸納條款 I: 如果 φ 是 wff，則 ¬ φ 是 wff。

歸納條款 Ⅱ 如果 φ 和 ψ 是 wff，則 （φ ∧ ψ）、（φ ∨ ψ）、（φ → ψ） 和 （φ ψ） 是 wff。

閉包條款： 其他東西都不是 wff。

重複的套用這三個公式允許生成複雜的 wff。例如：

通過規則 1，A 是 wff。

通過規則 2，¬ A 是 wff。

通過規則 1，B 是 wff。

通過規則 3，（¬ A ∨ B) 是 wff。

演算

為了簡單化，我們使用自然演繹系統，它沒有公理；或者等價的說，它有空的公理集合。

使用我們的演算的推導將用編號後的行的列表，在每行之上有一個單一的 wff 和一個理由（justification）的形式展示出來。任何前提（premise）都在上部，並帶有 "p" 作為它們的斷定。結論將在最後一行。推導將被看作完備的，條件是所有行都是通過正確的套用一個規則而從前面的行得出的。

（作為一種對比的方式，參見證明樹）。

公理

我們的公理集合是空集。

推理規則

我們的命題演算有十個推理（inference）規則。這些規則允許我們從給定的一組假定為真的公式中推導出其他為真的公式。前八個簡單的陳述我們可以從其他 wff 推論出（infer）特定的 wff。但是最後兩個規則使用了假言(hypothetical）推理，這意味著在規則的前提中我們可以臨時的假定一個（未證明的）假設（hypothesis）作為推導出的公式集合的一部分，來查看我們是否能推導出一個特定的其他公式。因為前八個規則不是這樣而通常被描述為非假言規則，而最後兩個就叫做假言規則。

雙重否定除去

從 wff ¬ ¬ φ，我們可以推出 φ。

合取介入

從任何 wff φ 和任何 wff ψ，我們可以推出 （φ ∧ ψ）。

合取除去

從任何 wff （φ ∧ ψ），我們可以推出 φ 和 ψ。

析取介入

從任何 wff φ，我們可以推出 （φ ∨ ψ） 和 （ψ ∨ φ），這裡的 ψ 是任何 wff。

析取除去

從 （φ ∨ ψ）、（φ → χ） 和 （ψ → χ） 形式的wff，我們可以推出 χ。

雙條件介入

從 （φ → ψ） 和 （ψ → φ） 形式的 wff，我們可以推出 （φ ψ）。

雙條件除去

從 wff （φ ψ），我們可以推出 （φ → ψ） 和 （ψ → φ）。

肯定前件

從 φ 和 （φ → ψ） 形式的 wff，我們可以推出 ψ。

條件證明

如果在假定假設 φ 的時候可以推導出 ψ，我們可以推出 （φ → ψ）。

反證證明

如果在假定假設 φ 的時候可以推導出 ψ 和 ¬ ψ，我們可以推出 ¬ φ。

規則的可靠性和完備性

這組規則的關鍵特性是它們是可靠的和完備的。非形式的，這意味著規則是正確的並且不再需要其他規則。這些要求可以如下這樣正式的提出。

我們定義真值指派為把命題變數映射到真或假的函式。非形式的，這種真值指派可以被理解為對事件的可能狀態（或可能性世界）的描述，在這裡特定的陳述是真而其他為假。公式的語義因而可以被形式化，通過對它們把那些"事件狀態"認定為真的定義。

我們通過如下規則定義這種真值 A 在什麼時候滿足特定 wff:

A 滿足命題變數P若且唯若A(P) = 真

A 滿足 ¬ φ若且唯若A 不滿足 φ

A 滿足 （φ ∧ ψ）若且唯若A 滿足 φ 與 ψ 二者

A 滿足 （φ ∨ ψ）若且唯若A 滿足 φ 和 ψ 中至少一個

A 滿足 （φ → ψ） 若且唯若沒有 A 滿足 φ 但不滿足 ψ 的事例

A 滿足 （φ ψ）若且唯若A 滿足 φ 與 ψ 二者，或則不滿足它們中的任何一個

通過這個定義，我們現在可以形式化公式φ 被特定公式集合 S 蘊涵的意義。非形式的，就是在使給定公式集合 S 成立的所有可能情況下公式 φ 也成立。這導引出了下面的形式化定義： 我們說 wff 的集合 S 語義蘊涵（蘊涵：entail 或 imply）特定的 wff φ，條件是滿足在 S 中的公式的所有真值指派也滿足 φ。

最後我們定義語法蘊涵，φ 被 S 語法蘊涵，若且唯若我們可以在有限步驟內使用我們提出的上述推理規則推導出它。這允許我們精確的公式化推理規則的可靠性和完備性的意義：

可靠性

如果 wff 集合 S 語法蘊涵 wff φ，則 S 語義蘊涵 φ

完備性

如果 wff 集合 S 語義蘊涵 wff φ，則 S 語法蘊涵 φ

對上述規則集合這些都成立。

其它相關

可靠性證明的梗概

（對於多數邏輯系統，這是相當"簡單的"證明方向）

符號約定： 設 "G" 是涉及語句集合的變數。設 "A"、"B" 和 "C" 是涉及句子的變數。我們把 "G 語法蘊涵 A" 寫成 "G 證明 A"。我們把 "G 語義蘊涵 A" 寫成 "G 蘊涵 A"。

我們要展示： (A)(G）（如果 G 證明 A，則 G 蘊涵 A)

我們注意到 "G 證明 A" 有一個歸納定義，這給予我們直接的辦法來證實（demonstrate)"如果 G 證明 A，則 . . ."形式的斷言。所以我們的證明是用歸納法進行的。

I. 基礎。展示： 如果 A 是 G 的成員則 G 蘊涵 A

[Ⅱ. 基礎。展示： 如果 A 是公理，則 G 蘊涵 A

Ⅲ. 歸納步驟： (a) 假定對於任意的 G 和 A，如果 G 證明 A 則 G 蘊涵 A。（如果需要的話，對 B、C 等做同樣的假定）

（b) 對於針對 A 的推論的規則的，導出一個新的句子 B 的每個可能的套用，展示 G 蘊涵 B。

（N.B. 對於上述演算基礎步驟 Ⅱ 可以省略，它是自然演繹系統而沒有公理。基本上，它涉及展示每個公理都是（語義上）邏輯真理。）

基礎步驟證實了對於任何 G 來自 G 的最簡單的可證明的語句都被 G 所蘊涵。（這是簡單的，因為集合蘊涵它的任何一個成員是語義事實，這是平凡的（trivial））。歸納步驟將有系統的覆蓋所有的進一步的可證明的句子--通過考慮我們能夠使用推理規則達成邏輯結論的每種情況--並展示如果一個新句子是可證明的，它也是在邏輯上被蘊涵的。（例如，我們可能有一個告訴我們從 "A" 可以推導出 "A 或 B"。在 Ⅲ.(a) 中我們假定如果 A 是可證明的則是被蘊涵的。我們也知道如果 A 是可證明的，則 "A 或 B" 是可證明的。我們必須展示接著 "A 或 B" 也是被蘊涵的。我們求助於語義定義和我們所做的假定來完成。我們假定了 A 從 G 是可證明出來的。所以它也被 G 所蘊涵。所以使 G 全部為真的任何語義求值也使 A 為真。此外通過"或"的語義定義，使 A 為真的任何求值都使 "A 或 B" 為真。所以使 G 的全部為真的任何求值都使 "A 或 B" 為真。所以 "A 或 B"被蘊涵了。）一般的，歸納步驟將由有一定長度的，卻是推論的所有規則的簡單的逐個例的分析組成的，它展示每個"保持的"語義蘊涵。

通過可證明性的定義，除了 G 的成員、公理、或從規則得出的句子之外沒有是可證明的；所以如果所有這些都是語義上被蘊涵的，則演繹演算是可靠的。

完備性證明的梗概

（這通常是非常困難的證明方向。）

我們接受同上面一樣的符號約定。

我們要展示： 如果 G 蘊涵 A，則 G 證明 A。我們通過反證法來進行： 我們轉而展示如果 G 不證明 A，則 G 不蘊涵 A。

I. G 不證明 A。（假定）

Ⅱ. 如果 G 不證明 A，則我們可以構造一個（有限的）"最大化的集合" G*，它是 G 的超集並且不證明 A。

（a）在這個語言的所有句子上加置一個"次序"。（比如，字母表次序），並把它們編號為 E1,E2,. . .

（b）歸納的定義集合（G0,G1 . . .）的一個序列（series) Gn 為如下 (i)G0=G。（ii) 如果 {Gk,E(k+1）} 證明 A，則 G(k+1）=Gk。（iii) 如果 {Gk,E(k+1）} 不證明 A，則 G(k+1）={Gk,E(k+1）}

（c）定義 G* 為所有 Gn 的並集。（就是說，G* 在任何 Gn 中的所有句子的集合）。

（d) 可以容易的展示 (i) G* 包含（是其超集） G （通過 (b.i））；（ii) G* 不證明 A （因為如果它證明 A 則某些句子被增加到某個 Gn 上而導致它證明了 A; 但是這被定義所排除）；和 (iii) G* 是（關於 A) "最大化的集合": 如果任何更多的句子不管怎樣的被增加到 G*，它就會證明 A。（因為如果有可能增加任何更多的句子，再次根據定義，在構造 Gn 期間被遇到的時候它們就應當已經被增加進去了。）

Ⅲ. 如果 G* 是（關於 A）的最大化集合，則它是"類真理的"。這意味著它包含句子 "A"，只在它不包含非-A 的句子的條件下； 如果它包含 "A" 並且包含 "如果 A 則 B"，則它也包含 "B"；以此類推。

Ⅳ. 如果 G* 是類真理的，則有這個語言的 "G*-規範"求值： 它使在 G* 中每個句子為真而在 G* 之外的所有句子為假，而仍然遵守在這個語言的語義合成（composition）的法則。

V. G*-規範求值將使我們最初的集合 G 全部為真，而使 A 為假。

Ⅵ. 如果有在其上 G 是真而 A 是假的求值，則 G 不（語義上）蘊涵 A。

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。

推理規則

推理規則是肯定前件：

<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>

並且可以演繹自 ⑴ 和 ⑵

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:

要證明： A → A （蘊涵的自反性）。

證明：

⒈ (A → ((A → A) → A)) → ((A → (A → A)) → (A → A))

公理 THEN-2 通過 φ = A，χ = A → A，ψ = A

⒉ A → ((A → A) → A)

公理 THEN-1 通過 φ = A，χ = A → A

⒊ (A → (A → A)) → (A → A)

得自 ⑴ 和 ⑵ 通過肯定前件。

⒋ A → (A → A)

公理 THEN-1 通過 φ = A，χ = A

⒌ A → A

得自 ⑶ 和 ⑷ 通過肯定前件。