命題邏輯- 維基百科，自由的百科全書

證明的例子 命題邏輯 維基百科，自由的百科全書 跳至導覽 跳至搜尋 此條目已列出參考文獻，但因為沒有文內引註而使來源仍然不明。

(2014年4月13日)請加上合適的文內引註來改善這篇條目。

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

目次 1術語 2形式描述 3例子 3.1簡單的公理系統 3.2自然演繹系統 3.2.1證明的例子 4規則的可靠性和完備性 4.1可靠性證明的梗概 4.2完備性證明的梗概 5公理化演算 5.1公理 5.2推理規則 5.3元推理規則 5.4證明的例子 6等價於等式邏輯 7其他邏輯演算 8引用 9參見 10外部連結 術語[編輯] 一般地說，演算是一個形式系統，包括一套語法表示式（合式公式）、這些表示式的一個特定子集（公理）和一套定義了特定的二元關係的形式規則，這個二元關係可解釋為表示式空間上的邏輯等價關係。

若形式系統會作為一個邏輯系統，其表示式會被解釋成數學陳述，且其規則，被稱之為「推理規則」，則一般會是保真的。

在此設定下，規則（可能也包括公理）可以被用來，從給定為真的陳述的公式中，推導出表示真的陳述的公式來。

公理的集合可能為空集、非空有限集、可數無限集或由公理模式所給定。

形式文法遞迴地定義了語言的表示式和合式公式。

之外，有時也可以給定一個語義，用以定義真值和賦值（或解釋）。

命題運算的語言包括：（1）一套原始符號，被稱之為「原子公式」、「預留位置」、「命題字母」或「命題變數」；（2）一套運算符號，被稱之為「邏輯運算子」。

一個「合式公式」是任一原子公式，或任一以運算符號依文法規則由原子公式建立起的公式。

在下文中我們描述一種標準命題演算。

很多不同的公式系統存在，它們都或多或少等價但在下列方面不同：（1）它們的語言（就是說哪些原始符號和運算符號是語言的一部分）；（2）它們有哪些（如果有的話）公理；（3）採用了哪些推理規則。

形式描述[編輯] 命題演算是一個形式系統 L = L   ( A ,   Ω ,   Z ,   I ) {\displaystyle{\mathcal{L}}={\mathcal{L}}\(\mathrm{A},\\Omega,\\mathrm{Z},\\mathrm{I})} ，它的公式按如下方式構造： A {\displaystyle\mathrm{A}\!} 集合是由名為「命題符號」或「命題變數」之元素所組成的有限集合，一個「命題變數」可取值為集合里的「命題符號」。

語法上來說，它們是形式語言 L {\displaystyle{\mathcal{L}}} 最基本的元素，亦被稱之為「原子公式」或「終端元素」。

在接著的例子中， A {\displaystyle\mathrm{A}\!} 內的元素一般寫作字母p,q,r之類的形式。

Ω {\displaystyle\Omega\!} 是名為「算子符號」或「邏輯運算子」之元素所組成的有限集合。

集合 Ω {\displaystyle\Omega\!} 被劃分成如下等不相交的子集： Ω = Ω 0 ∪ Ω 1 ∪ … ∪ Ω j ∪ … ∪ Ω m {\displaystyle\Omega=\Omega_{0}\cup\Omega_{1}\cup\ldots\cup\Omega_{j}\cup\ldots\cup\Omega_{m}\,} 。

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

在更熟知的命題演算中， Ω {\displaystyle\Omega\!} 一般被劃分如下： Ω 1 = { ¬ } , {\displaystyle\Omega_{1}=\{\lnot\}\,,} Ω 2 ⊆ { ∧ , ∨ , → , ↔ } {\displaystyle\Omega_{2}\subseteq\{\land,\lor,\rightarrow,\leftrightarrow\}\,} 。

一種常用的做法是把常數邏輯值當作一種零元素算子，即： Ω 0 = { ⊤ ,   ⊥ } {\displaystyle\Omega_{0}=\{\top,\\bot\}\,} 。

有些作者會用~來替代¬，也有的用&或 ⋅ {\displaystyle\cdot} 來取替 ∧ {\displaystyle\land} 。

邏輯值所構成的集合也有許多不同的符號表示，如{假,真}、{F,T}或{0,1}來取替{ ⊥ {\displaystyle\bot} , ⊤ {\displaystyle\top} }，這些都常見於各個論著之中。

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

L {\displaystyle{\mathcal{L}}} 的語言，亦稱之為「公式」或「合式公式」的集合，可由如下規則被歸納或遞迴地定義： 基本元素： A {\displaystyle\mathrm{A}\!} 內的任何元素都是 L {\displaystyle{\mathcal{L}}} 的公式。

步驟（a）：如果p是公式，則¬p也會是公式。

步驟（b）：如果p和q是公式，則( p {\displaystyle\,\!p} ∧ {\displaystyle\land} q {\displaystyle\,\!q} )、( p {\displaystyle\,\!p} ∨ {\displaystyle\lor} q {\displaystyle\,\!q} )、( p → q {\displaystylep\,\!\rightarrowq\,\!} )和( p ↔ q {\displaystyle\,\!p\leftrightarrowq\,\!} )也都會是公式。

封閉性：其他都不會是 L {\displaystyle{\mathcal{L}}} 的公式。

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

例如： 依規則1，p是公式。

依規則2，¬p是公式。

依規則1，q是公式。

依規則3，(¬p∨q)是公式。

Z {\displaystyle\mathrm{Z}\!} 集合是「轉換規則」（當作為邏輯應用時則稱之為「推理規則」）之所構成的有限集合。

Z {\displaystyle\mathrm{Z}\!} 集合的「轉換規則」是用「原子公式」和「邏輯運算子」構成的。

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

例子[編輯] 簡單的公理系統[編輯] 設 L 1 = L   ( A ,   Ω ,   Z ,   I ) {\displaystyle{\mathcal{L}}_{1}={\mathcal{L}}\(\mathrm{A},\\Omega,\\mathrm{Z},\\mathrm{I})} ，這裡的 A ,   Ω ,   Z ,   I {\displaystyle\mathrm{A},\\Omega,\\mathrm{Z},\\mathrm{I}} 定義如下： A {\displaystyle\mathrm{A}\!} 是個含有足夠多元素以應付討論所需的有限集合，如： A = { p , q , r , s , t , u } {\displaystyle\mathrm{A}=\{p,q,r,s,t,u\}\,} 。

在合取、析取和蘊涵（∧、∨和→）這三個運算子之中，可以將其中一個拿來當做基本的，而另兩個則以其和否定（¬）來定義。

實際上，所有的邏輯運算子都可以用自足算子的方式來定義。

而雙條件（↔）當然可由合取和薀涵來定義，亦即a↔b可被定義為(a→b)∧(b→a)。

採用否定和薀涵做為命題演算的兩個基本運算，相當於把omega集 Ω = Ω 1 ∪ Ω 2 {\displaystyle\Omega=\Omega_{1}\cup\Omega_{2}} 劃分如下： Ω 1 = { ¬ } {\displaystyle\Omega_{1}=\{\lnot\}\,} 。

Ω 2 = { → } {\displaystyle\Omega_{2}=\{\rightarrow\}\,} 。

有一個公理系統是揚·武卡謝維奇所發現的，而這系統可以如下地公式化為此語言中的命題演算。

各個公理都是由下列的公理模式作代換所得。

p → ( q → p ) {\displaystylep\to(q\top)} ( p → ( q → r ) ) → ( ( p → q ) → ( p → r ) ) {\displaystyle(p\to(q\tor))\to((p\toq)\to(p\tor))} ( ¬ p → ¬ q ) → ( q → p ) {\displaystyle(\negp\to\negq)\to(q\top)} 其推理規則為肯定前件（即可由p和(p→q)導出q）。

而a∨b和a∧b則是分別被定義為¬a→b和¬(a→¬b)。

自然演繹系統[編輯] 設 L 2 = L   ( A ,   Ω ,   Z ,   I ) {\displaystyle{\mathcal{L}}_{2}={\mathcal{L}}\(\mathrm{A},\\Omega,\\mathrm{Z},\\mathrm{I})} ，這裡的 A ,   Ω ,   Z ,   I {\displaystyle\mathrm{A},\\Omega,\\mathrm{Z},\\mathrm{I}} 定義如下： A {\displaystyle\mathrm{A}\!} 是個含有足夠多元素以應付討論所需的有限集合，如： A = { p , q , r , s , t , u } {\displaystyle\mathrm{A}=\{p,q,r,s,t,u\}\,} 。

Ω = Ω 1 ∪ Ω 2 {\displaystyle\Omega=\Omega_{1}\cup\Omega_{2}} 劃分為如下： Ω 1 = { ¬ } {\displaystyle\Omega_{1}=\{\lnot\}\,} 。

Ω 2 = { ∧ , ∨ , → , ↔ } {\displaystyle\Omega_{2}=\{\land,\lor,\rightarrow,\leftrightarrow\}\,} 。

在此命題演算的例子中，轉換規則被解釋為所謂的「自然演繹系統」下之推理規則。

這裡表述的特定系統沒有起始點，這意味著它對邏輯應用的解釋是從空公理集合中推導出其定理的。

起始點的集合是空的，亦即 I = ∅ {\displaystyle\mathrm{I}=\varnothing\,} 。

轉換規則的集合 Z {\displaystyle\mathrm{Z}\!} 描述如下： 此命題演算有十個推理規則。

這些規則允許我們從給定的一組假定為真的公式中推導出其他為真的公式。

前九個只是簡單地指我們可以從其他合式公式推論出特定的合式公式。

但是最後一個規則使用了假言（hypothetical）推理，這意味著在規則的前提中，我們可以臨時的假定一個（未證明的）假設作為推導出的公式集合的一部分，來檢視我們是否能推導出一個特定的其他公式。

因為前九個規則不是這樣而通常被描述為「非假言」規則，而最後一個則被稱為「假言」規則。

否定介入（英語：Negationintroduction）：從φ→¬ψ和φ→ψ中可推出¬φ。

雙重否定除去：從¬¬φ中可推出φ。

合取介入（英語：Conjunctionintroduction）：從φ和ψ中可推出(φ∧ψ)。

合取除去（英語：Conjunctionelimination）：從(φ∧ψ)中可推出φ和ψ。

析取介入（英語：Disjunctionintroduction）：從φ中可推出(φ∨ψ)。

析取除去（英語：Disjunctionelimination）：從(φ∨ψ)、(φ→χ)和(ψ→χ)可推出χ。

雙條件介入（英語：Biconditionalintroduction）：從(φ→ψ)和(ψ→φ)中可推出(φ↔ψ)。

雙條件除去（英語：Biconditionalelimination）：從(φ↔ψ)中可推出(φ→ψ)和(ψ→φ)。

肯定前件（條件除去）：從φ和(φ→ψ)中可推出ψ。

條件證明（條件介入）：若假定φ為真可證明出ψ，可推出(φ→ψ)。

證明的例子[編輯] 以下推導將用編號後的行的列表來表示，在每行之上有一個單一的公式和一個理由（justification）。

論證的各個前提會在列表的首行給出。

結論將在最後一行。

一個推導稱為完備的，若所有行都是通過正確的應用一個規則而從前面的行得出的。

下面是（語法上的）證明的一個例子： 要證明： A → A {\displaystyleA\rightarrowA} 證明： 編號 公式 理由 1 A 前提 2 A∨A 析取介入自（1） 3 (A∨A)∧A 合取介入自（1）和（2） 4 A 合取除去自（3） 5 A ⊢ {\displaystyle\vdash\,} A 總結（1）到（4） 6 ⊢ {\displaystyle\vdash\,} A→A 條件證明自（5） A ⊢ A {\displaystyleA\vdashA} 可解釋為「假定A，推導出A」。

⊢ A → A {\displaystyle\vdashA\rightarrowA} 為「不假定任何東西，推導出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叫做排中律（拉丁語tertiumnondatur：「排除第三者」）並反映了命題公式的語意求值：公式的真值要麼是真要麼是假。

至少在經典邏輯中，沒有第三個真值。

直覺邏輯不接受公理NOT-3。

推理規則[編輯] 推理規則是肯定前件： ϕ ,   ϕ → χ ⊢ χ {\displaystyle\phi,\\phi\rightarrow\chi\vdash\chi} . 如果還使用雙箭頭的等價算子的話，則要增加如下"自然"推理規則： IFF-1： ϕ ↔ χ ⊢ χ → ϕ {\displaystyle\phi\leftrightarrow\chi\vdash\chi\rightarrow\phi} IFF-2： ϕ → χ ,   χ → ϕ ⊢ ϕ ↔ χ {\displaystyle\phi\rightarrow\chi,\\chi\rightarrow\phi\vdash\phi\leftrightarrow\chi} 元推理規則[編輯] 設一個推導被表示為相繼式，各個假設在十字轉門（turnstile）的左側，而結論在十字轉門的右側。

則演繹定理可以被陳述如下： 如果相繼式 ϕ 1 ,   ϕ 2 ,   . . . ,   ϕ n ,   χ ⊢ ψ {\displaystyle\phi_{1},\\phi_{2},\...,\\phi_{n},\\chi\vdash\psi} 已經被證明了，則也有可能證明相繼式 ϕ 1 ,   ϕ 2 ,   . . . ,   ϕ n ⊢ χ → ψ {\displaystyle\phi_{1},\\phi_{2},\...,\\phi_{n}\vdash\chi\rightarrow\psi} 。

這個演繹定理（DT）自身沒有公式化為命題演算：它不是命題演算的定理，而是關於命題演算的一個定理。

在這個意義上，它是元定理，相當於關於命題演算可靠性和完備性的定理。

在另一方面，DT對於簡化語法上的證明過程是如此的有用以至於它看作和用做推理規則，同肯定前件一起使用。

在這個意義上，DT對應於自然條件證明推理規則，它是在本條目中提出的第二個例子的命題演算的一部分。

DT的逆定理也是有效的： 如果相繼式 ϕ 1 ,   ϕ 2 ,   . . . ,   ϕ n ⊢ χ → ψ {\displaystyle\phi_{1},\\phi_{2},\...,\\phi_{n}\vdash\chi\rightarrow\psi} 已經被證明了，則也有可能證明相繼式 ϕ 1 ,   ϕ 2 ,   . . . ,   ϕ n ,   χ ⊢ ψ {\displaystyle\phi_{1},\\phi_{2},\...,\\phi_{n},\\chi\vdash\psi} 實際上，DT的逆定理的有效性相對於DT而言是平凡的： 如果 ϕ 1 ,   . . . ,   ϕ n ⊢ χ → ψ {\displaystyle\phi_{1},\...,\\phi_{n}\vdash\chi\rightarrow\psi} 則 1： ϕ 1 ,   . . . ,   ϕ n ,   χ ⊢ χ → ψ {\displaystyle\phi_{1},\...,\\phi_{n},\\chi\vdash\chi\rightarrow\psi} 2： ϕ 1 ,   . . . ,   ϕ n ,   χ ⊢ χ {\displaystyle\phi_{1},\...,\\phi_{n},\\chi\vdash\chi} 並且可以演繹自（1）和（2） 3： ϕ 1 ,   . . . ,   ϕ n ,   χ ⊢ ψ {\displaystyle\phi_{1},\...,\\phi_{n},\\chi\vdash\psi} 通過肯定前件的方式，Q.E.D. DT的逆命題有著強有力的蘊涵：它可以用來把公理轉換成推理規則。

例如，公理AND-1 ⊢ ϕ ∧ χ → ϕ {\displaystyle\vdash\phi\wedge\chi\rightarrow\phi} 可以通過演繹定理的逆定理的方式被轉換成推理規則 ϕ ∧ χ ⊢ ϕ {\displaystyle\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。

不等式的重要性在於它對應於希爾伯特系統的演繹或蘊涵符號 ⊢ {\displaystyle\vdash} 。

蘊涵 ϕ 1 ,   ϕ 2 , … ,   ϕ n ⊢ ψ {\displaystyle\phi_{1},\\phi_{2},\ldots,\\phi_{n}\vdash\psi} 被轉換為代數框架下的不等式 ϕ 1   ∧   ϕ 2   ∧   …   ∧   ϕ n     ≤     ψ {\displaystyle\phi_{1}\\land\\phi_{2}\\land\\ldots\\land\\phi_{n}\\\leq\\\psi} 反過來代數不等式x≤y被轉換為蘊涵 x   ⊢   y {\displaystylex\\vdash\y} 在實質條件（implication）x→y和不等式或者蘊涵（entailment）x≤y或 x   ⊢   y {\displaystylex\\vdash\y} 之間的區別在於，前者是內在於邏輯的，而後者是外在的。

在兩個項之間內在的實質條件是同類的另一個項。

在兩個項之間的外在的蘊涵表達了在邏輯語言之外的元真理，並被認為是元語言的一部分。

即使所研究的邏輯是直覺的，蘊涵都通常經典的理解為二值的：要麼左側蘊涵（或小於等於）右側，要麼不蘊涵之。

同代數邏輯之間類似但更加複雜的相互轉換，對於自然演繹系統和相繼式演算也是可能的。

後者的轉換可以被釋義為二值的，但是更有洞察力的釋義是作為集合，它的元素可以被理解為由範疇的態射組成的抽象證明。

在這種釋義下相繼式演算的切規則對應於範疇的複合。

其他邏輯演算[編輯] 命題演算大概是在所有當前使用的邏輯演算中最簡單的一種。

（亞里斯多德的「三段論」演算，在現代邏輯中在很大程度上被替代了，它與命題邏輯相比在某些方面更簡單--但在其他方面更加複雜）。

它可以按很多方式來擴充。

最直接的方式是開發一個更加複雜的邏輯演算，介入對所用於的句子的更精細的細節敏感的規則。

在命題邏輯中的原子句子被分解成項（英語：Singularterm）、變數、謂詞和量詞的時候，它們就生成了一階邏輯，或者叫做一階謂詞邏輯，它保留命題邏輯的所有規則並增加了一些新規則。

（例如，從「所有的狗都是動物」我們可以推出「如果Rover是狗，則Rover是動物」）。

通過一階邏輯的工具，有可能公式化一些理論，要麼帶有顯式的公理要麼通過推理規則，而把它們自身當作邏輯演算。

算術是其中最周知的理論；其他的還包括集合論和分體論。

模態邏輯也提供了一種推理的變體，它不能在命題演算中擷取。

例如，從「必然地p」我們可以推出p。

從p我們可以推出「可能地p」。

多值邏輯是允許句子有除了「真」和「假」之外的值的邏輯。

（例如，「都不」和「都是」是標準的「額外值」；「連續統邏輯」允許每個句子有任何的在「真」和「假」之間的表示「真實程度」的無限個值）。

這些邏輯經常要求與命題邏輯非常不同的運算裝置。

參照[編輯] Brown,FrankMarkham(2003),BooleanReasoning:TheLogicofBooleanEquations,1stedition,KluwerAcademicPublishers,Norwell,MA.2ndedition,DoverPublications,Mineola,NY. Chang,C.C.,andKeisler,H.J.(1973),ModelTheory,North-Holland,Amsterdam,Netherlands. Kohavi,Zvi(1978),SwitchingandFiniteAutomataTheory,1stedition,McGraw–Hill,1970.2ndedition,McGraw–Hill,1978. Korfhage,RobertR.(1974),DiscreteComputationalStructures,AcademicPress,NewYork,NY. Lambek,J.andScott,P.J.(1986),IntroductiontoHigherOrderCategoricalLogic,CambridgeUniversityPress,Cambridge,UK. Mendelson,Elliot(1964),IntroductiontoMathematicalLogic,D.VanNostrandCompany. 參見[編輯] 演繹推理 希爾伯特演繹系統 自然演繹 相繼式演算 布林運算 布林代數 外部連結[編輯] Klement,KevinC.(2006),"PropositionalLogic",inJamesFieserandBradleyDowden(eds.),InternetEncyclopediaofPhilosophy,Eprint（頁面存檔備份，存於網際網路檔案館）. IntroductiontoMathematicalLogic（頁面存檔備份，存於網際網路檔案館） ElementsofPropositionalCalculus forallx:anintroductiontoformallogic（頁面存檔備份，存於網際網路檔案館）,byP.D.Magnus,coversformalsemanticsandprooftheoryforsententiallogic. PropositionalLogic(GFDLed) 閱論編邏輯 概要學術領域 辯論法 價值論 審辯式思維 可計算性理論 形式語意學 邏輯史 非形式邏輯 計算機邏輯 數理邏輯 數學 元邏輯 元數學 模型論 哲學邏輯 哲學 邏輯哲學 數學哲學 證明論 集合論 基礎概念 溯因推理 分析真理 二律背反 先驗 演繹推理 定義 描述 薀涵 歸納推理 推論 邏輯結論 邏輯形式 邏輯薀涵 邏輯真理 名稱 充分條件 意義 悖論 可能世界 假定 機率 理智 推理 指涉 語意學 語句 嚴格條件 交換區 語法學 真理 真值 有效性  哲學邏輯審辯式思維和非形式邏輯 分析 歧義性 論證 信仰 偏見 公信力 證據 解釋 解釋力 事實 謬論 探究 意見 奧卡姆剃刀 前提 政治宣傳 審慎 推理 關聯 修辭學 嚴格 含糊 演繹理論 結構主義 雙面真理說 虛構主義 有限主義 形式主義 直覺主義 邏輯原子論 邏輯主義 唯名論 柏拉圖唯實論 實用主義 唯實論  元邏輯（英語：metalogic）和元數學 康托爾定理 可判定性 邱奇-圖靈論題 相容性 有效方法 數學基礎 哥德爾完備性定理 哥德爾不完備定理 可靠性 完備性 可判定性 解釋 勒文海姆–斯科倫定理 元定理 可滿足性 獨立性 類型-記號區別 使用-提及區別  數理邏輯一般 形式語言 形成規則 形式系統 演繹系統 形式證明 形式語意學 合式公式 集合 元素 類 經典邏輯 公理 自然演繹 推理規則 關係 定理 邏輯結論 公理系統 類型論 符號 語法學 定律 傳統邏輯 命題 推論 論證 有效性 說服力 直言三段論 對立四邊形 文氏圖 命題邏輯和邏輯代數 布林函數 命題邏輯 命題公式 邏輯聯結詞 真值表 謂詞邏輯 一階邏輯 量化 謂詞 二階邏輯 一元謂詞演算 集合論 集合 空集 列舉法 外延性 有限集合 函數 子集 冪集 可數集 遞迴集合 定義域 值域 有序對 不可數集 模型論 模型 解釋 非標準模型 有限模型論 真值 有效性 證明論 形式證明 演繹系統 形式系統 定理 邏輯結論 推理規則 語法學 可計算性理論 遞迴 遞迴集合 遞迴可列舉集合 決定性問題 邱奇-圖靈論題 可計算函數 原始遞迴函數  非傳統邏輯模態邏輯 真性邏輯 價值邏輯 道義邏輯 信念邏輯 認識邏輯 時間邏輯 直覺主義 直覺主義邏輯 結構分析 海廷算術 直覺類型論 結構集合論 模糊邏輯 真實度 模糊規則 模糊集 模糊有限元素 模糊集合運算 亞結構邏輯 結構規則 相干邏輯 線性邏輯 次協調邏輯 雙面真理說 描述邏輯 本體論 本體語言  邏輯學家 安德遜 亞里斯多德 魯世德 西那 貝恩 巴威斯 博內斯 布林 布勒斯 康托爾 卡爾納普 邱奇 克呂西波 加里 德摩根 弗雷格 吉奇 根岑 哥德爾 希爾伯特 克萊尼 克里普克 萊布尼茲 勒文海姆 皮亞諾 皮爾士 普特南 奎因 羅素 施洛德 司各脫 斯科倫 史慕揚 塔斯基 圖靈 懷特黑德 奧卡姆的威廉 維根斯坦 策梅洛  列表主題 邏輯概要 數理邏輯 布林代數 集合論 其它 邏輯學家 推理規則 悖論 謬論 邏輯符號  常見邏輯符號 &   ∨   ¬   ~   →   ⊃   ≡   |   ∀   ∃   ⊤   ⊥   ⊢   ⊨   ∴   ∵ 分類 取自「https://zh.wikipedia.org/w/index.php?title=命题逻辑&oldid=69672875」 分類：​邏輯數理邏輯形式邏輯系統命題演算隱藏分類：​自2014年4月缺少註腳的條目含有拉丁語的條目使用過時的math標籤格式的頁面 導覽選單 個人工具 沒有登入討論貢獻建立帳號登入 命名空間 條目討論 臺灣正體 已展開 已摺疊 不转换简体繁體大陆简体香港繁體澳門繁體大马简体新加坡简体臺灣正體 查看 閱讀編輯檢視歷史 更多 已展開 已摺疊 搜尋 導航 首頁分類索引特色內容新聞動態近期變更隨機條目資助維基百科 說明 說明維基社群方針與指引互助客棧知識問答字詞轉換IRC即時聊天聯絡我們關於維基百科 工具 連結至此的頁面相關變更上傳檔案特殊頁面靜態連結頁面資訊引用此頁面維基數據項目 列印/匯出 下載為PDF可列印版 其他專案 維基共享資源 其他語言 العربيةБеларуская(тарашкевіца)БългарскиCatalàČeštinaCymraegDeutschΕλληνικάEnglishEspañolEestiEuskaraفارسیSuomiFrançaisNordfriiskGalegoעבריתहिन्दीMagyarՀայերենBahasaIndonesiaItaliano日本語한국어КыргызчаLatinaLietuviųNederlandsNorsknynorskNorskbokmålPolskiPortuguêsРусскийSimpleEnglishSlovenčinaSlovenščinaСрпски/srpskiSvenskaไทยTürkçeУкраїнськаTiếngViệt粵語 編輯連結