命題邏輯

題演算語言題量（占符（））句/判決算（連詞）。式句操符建造式。描述標準題演算。式系統存，價列：

⑴語言（哪操符量語言）；

⑵哪（）；

⑶採用了哪些推理規則。

語言的構成：

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

表示連結詞（connective)（或邏輯運算元）的符號：¬；、∧、∨、→、?。（我們可以使用更少的運算元（和相應的符號），因為一些運算元是簡寫形式—例如，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叫做"排中律"（拉丁語tertiumnondatur:"排除第三者")並反映了命題公式的語義求值：公式可以有的真值要麼是真要麼是假。至少在經典邏輯中，沒有第三個真值。直覺邏輯不接受公理NOT-3。

推理規則

推理規則是肯定前件：

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

如果還使用雙箭頭的等價運算元的話，則要增加如下"自然"推理規則：

IFF-1:$\backslash phi\backslash leftrightarrow\backslash chi\backslash vdash\backslash chi\backslash rightarrow\backslash phi$

IFF-2:$\backslash phi\backslash rightarrow\backslash chi,\backslash \backslash chi\backslash rightarrow\backslash phi\backslash vdash\backslash phi\backslash leftrightarrow\backslash chi$

設示範被表示為相繼式，假設在十字轉門（turnstile）的左側而結論在十字轉門的右側。則演繹定理可以被陳述如下：

如果相繼式

已經被證明了，則也有可能證明相繼式

$\backslash phi\_1,\backslash \backslash phi\_2,\backslash ...,\backslash \backslash phi\_n\backslash vdash\backslash chi\backslash rightarrow\backslash psi$；。

這個演繹定理（DT）自身沒有公式化為命題演算：它不命題演算的定理，而是關於命題演算的一個定理。在這個意義上，它是元定理，相當於關於命題演算可靠性和完備性的定理。

在另一方面，DT對與簡化語法上的證明過程是如此的有用以至於它看作和用做推理規則，同肯定前件一起使用。在這個意義上，DT對應於自然條件證明推理規則，它是在本文中提出的第一個版本的命題演算的一部分。

DT的逆定理也是有效的：

如果相繼式

已經被證明了，則也有可能證明相繼式

實際上，DT的逆定理的有效性相對於DT而言是平凡的：

如果

則

1:$\backslash phi\_1,\backslash ...,\backslash \backslash phi\_n,\backslash \backslash chi\backslash vdash\backslash chi\backslash rightarrow\backslash psi$

2:$\backslash phi\_1,\backslash ...,\backslash \backslash phi\_n,\backslash \backslash chi\backslash vdash\backslash chi$

並且可以演繹自⑴和⑵

3:$\backslash phi\_1,\backslash ...,\backslash \backslash phi\_n,\backslash \backslash chi\backslash vdash\backslash psi$

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

DT的逆命題有著強有力的蘊涵：它可以用來把公理轉換成推理規則。例如，公理AND-1,

可以通過演繹定理的逆定理的方式被轉換成推理規則

這是合取除去，是（在本文中）第一個版本的命題演算中使用的十個推理規則中的一個。

證明的例子

下面是（語法上）證明的一個例子，只涉及到公理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

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