布林邏輯與公理系統

想要理解甚麼是數學，最快速的捷徑是從公理系統下手，因為公理系統是數學證明的核心，理解了公理系統之後，就可以看懂數學家到底在玩甚麼遊戲了！

但是、很多數學的公理系統太過複雜，因此很難解釋，讀者往往在還沒入門之前，就已經先恍神了，所以為了讓大家很容易的理解公理系統，我們選擇了一個最簡單的數學體系，那就是布林邏輯。

布林邏輯只有兩個值，那就是 0 與 1 ，所以可以說是最簡單的數學體系了，就讓我們從布林邏輯開始，理解何謂公理系統吧！

何謂嚴格的數學證明？

當我還是個學生時，我總是困惑著如何應付老師的考試，其中一個重要的數學困擾是，老師要我們「證明」某個運算式。

最大的問題不在於我不會「證明」，因為在很多科目的證明題當中，我也都「答對了」，但是這種答對總是讓我感到極度的沒有把握，因為有時老師說「這樣的證明是對的」，但有時卻說「這樣的證明是錯的」。

更神奇的是，老師的證明永遠都是對的，他們可以突然加入一個「推論」，而這個推論的根據好像之前沒有出現過，然後他們說：「由此可證」、「同理可證」....。

直到有一天，我終於懂了。

因為課堂上老師的證明往往不是「嚴格的證明」，因為嚴格的證明通常「非常的困難」，每個證明都可以是一篇論文，甚至在很多論文當中的證明也都不是嚴格的。

所以在課堂上，老師總是可以天外飛來一筆的，跳過了某些「無聊的步驟」，奇蹟式的證明了某些定理，而這正是我所以感到困擾的原因。

一般的證明

一般而言，日常生活中的證明，通常是不嚴格的。

舉例來說，我可以「證明」某人殺了死者，因為殺死死者的兇刀上有「某人」的指紋。

但是這樣的證明並不嚴格，因為有很少的可能性是「某人摸過兇刀、但是並沒有殺人」。

所以我們總是可以看到那個「外表看似小孩，智慧卻過於常人」的「名偵探柯南」，總是天外飛來一筆的「證明」了某人是兇手，這種證明與數學證明可是完全不同的。

嚴格的證明

數學的證明通常不能是「機率式」的，例如：「我證明他 99% 殺了人」，這樣的證明稱不上是嚴格的證明。

嚴格的證明也並非結果一定要是 100% 的正確 (當然也不是說結果不正確)，真正的證明是一種過程，而不是結果。

怎麼說呢？

數學其實很像程式領域的演算法，或者就像是電腦的運作過程，當我們設計出一顆 CPU 之後，你必須用該 CPU 的指令撰寫出某些函數，以便完成某個程式。

那麼，數學的 CPU 是甚麼呢？

答案是「公理系統」 (Axioms)！

只有透過公理系統，經由某種演算方式，計算出待證明定理在任何情況下都是真的，這樣才算是證明了該定理。

這些公理系統其實就是數學的 CPU 指令集。

布林代數大概是數學當中最簡單的系統了，因為布林代數的値只有兩種--「真與假」 (或者用 0 與 1 代表)。

為了說明嚴格的數學證明是如何進行的，我們將從布林代數的公理系統 (CPU?) 開始，說明如何證明布林代數的某些定理，就好像是如何用指令集撰寫程式一樣。

布林邏輯

對於單一變數 x 的布林系統而言，x 只有兩個可能的值 (0 或 1)。

對於兩個變數 x, y 的布林系統而言，(x, y) 的組合則可能有 (0,0), (0,1), (1,0), (1,1) 四種。

對於三個變數 x, y, z 的布林系統而言，(x, y, z) 的組合則可能有 (0,0, 0), (0,0,1), (0,1,0), (0,1,1), (1,0, 0), (1,0,1), (1,1,0), (1,1,1) 八種。

基本的布林邏輯運算有三種，AND (且), OR (或), NOT (反)，在布林代數當中，通常我們在符號上面加一個上標橫線代表 NOT，用 $\wedge$ 代表 AND，用 $\vee$ 代表 OR。

但是在程式裏面，受到 C 語言的影響，很多語言用驚嘆號 ! 代表 NOT，用 & 代表 AND，用 | 代表 OR。

我們以下將採用NOT，用 & 代表 AND，用 | 代表 OR，但是卻用負號 - 代表 not，來解說公理系統的作用。

假如我們想知到某個邏輯式的真值表，例如 (-x | y) 的真值表，只要透過列舉的程序就可以檢查完畢。

接著，我們就可以定義一些公理系統，這些「公理系統」就像是數學推理的指令集，讓我們可以推論出哪些邏輯式在這個公理系統下是真的 (定理)，哪些邏輯式這個公理系統下不一定是真的。

知識庫推理系統

舉例而言，假如我們制定了一個公理系統如下所示。

公理 1: -A | B
公理 2: -B | C
公理 3: A

當我們制定完公理系統之後，這些公理就無條件地成立了，而且每一條都成立。

換句話說，上述系統裏的 (-A | B) & (-B | C) & A 這個陳述是成立的。

讓我們列出上述系統的真值表，看看這樣的公理系統代表甚麼意義？

在上述真值表中，那些不符合公理者都可以先刪除，這樣我們就得到下列的《剩餘真值表》。

結果只剩下一個可能性，也就是 A=1, B=1, C=1 。

但是在上述公理系統中，我們並沒有《規定 A=1, B=1, C=1 》，而是規定了 (-A | B)=1, (-B | C)=1, A=1 這三條公理。

但那三條公理，導出來的結果，其實就是 A=1, B=1, C=1。換句話說， B=1, C=1 在這個公理系統下，都是定理。

上述的那個系統，比較不像《數學系統》，而是一個《知識庫系統》，我們可以透過《知識庫》裏的《事實陳述》，用《真值表》的方式，刪除《不符合事實》的項目，然後在留下的世界裏尋找《符合該世界體系，卻又沒有直接說出來的事實》，這種過程基本上就是一種推理。

布林邏輯的公理系統

在布林邏輯裏，其實就隱含了一組公理系統，這個公理系統其實就是 AND, OR, NOT 的真值表定義，也就是下列的三個表格。

根據 AND, OR, NOT 三個表格，我們可以建構出一些定理，舉例而言，在布林邏輯裏很有用的《迪摩根定理》就可以用真值表檢核如下：

您可以發現 -(x｜y) 和 -x&-y 兩者的真值是一樣的，-(x&y) 與 (-x｜-y) 兩者的真值也是一樣的。

因此、我們得到下列兩個定理：

1. -(x｜ y) = -x & -y
2. -(x & y) = -x｜-y

這就是所謂的《迪摩根定理》(De Morgan's laws)。

推論法則

但是、上述的定理是用《列舉真值表》的方式得到的，這種方式不太有效率，因為對於 n 個變數的世界而言，真值表會有 $2^n$ 列 (在 n 比較大的時候，這真的會非常巨大，萬一有無窮多個變數，那麼根本就列不完了)。

問題是、如果不用真值表，那麼還有甚麼方法可以《找出定理》呢？

答案當然是有的、那就是用《推論法則》！

肯定前項 (Modus Poens)

舉例而言，以下是布林邏輯的一組推論法則。

前提 1: -p | q
前提 2: p
-------------------
結論： q

各位心裡應該不免納悶，為何這樣的推論法則成立呢？

其實這樣的法則，一樣是從《真值表》得來的！

我們就可以列出上述推論法則中，前提與結論的真值表如下：

在上述真值表中，凡是無法滿足前提的列，就代表該項目違反前提，可以被刪除 (不符合前提)：

在上述表格中，前兩條的 p 為 0，因此不滿足前提 2，而第三條的 -p|q 為 0，不滿足前提 1，因此符合前提的項目就只剩下了一個如下。

在這個滿足公理系統的真值表當中，我們可以看到 q 只能是 1，也就是 q 在那兩個前提下必然為真，也就是 q 其實是該前提下的必然結論。

換句話說、從 p & (-p | q) 可以推論出 q。

如果我們把 -p|q 簡寫為 p → q，則上述推論法則可以改寫如下，這樣的推論法則稱為 Modus Ponus (中文翻成「肯定前件」)。

前提 1: p → q
前提 2: p
------------------
結論： q

於是我們可以得到下列《代換式》，這種代換式就是一組推論法則。

 p ; p → q
-----------
    q

以上這組推論法則，稱為 Modus ponens ，中文可以稱為《肯定前項》！

有了上述推論法則後，我們就可以進行知識推理了，讓我們看看前面知識庫的例子。

公理 1: -A | B
公理 2: -B | C
公理 3: A

由於 -p|q 被簡寫為 p → q，所以上述《公理》改寫如下：

公理 1: A → B
公理 2: B → C
公理 3: A

於是我們可以開始利用剛剛得到的推論法則，也就是下列這組代換式進行推理。

 p ; p → q
-----------
    q

如果把 p 代換為 A, q 代換為 B，那麼會得到

 A ; A → B
-----------
    B

也就是從《公理1》 和《公理3》可以推出 B，因此 B 在這個系統下是真的，換句話說就是定理。

同樣的我們可以從《定理》 B 與《公理 1》繼續套用推論法則，於是得到 C 也是該系統下的真理 (事實)。

 B ; B → C
-----------
    C

否定後項 (Modus Tollens)

當然、布林邏輯的推理法則不只《肯定前項》一種，您還可以想出很多種推理法則。

另一種正確的推理法則，是採用《否定後項》的方式，其形式如下：

 p → q ; -q
-----------
    -p

其中的 p → q 一樣是 -p｜q 的縮寫。

假如我們有下列《公理系統》，那麼就可以反過來推論，得到 -B 與 -A 的結論。

公理 1: A → B
公理 2: B → C
公理 3: -C

推論過程如下：

公理 2: B → C
公理 3: -C
-------------
定理 1: -B

得出結論 -B ，然後繼續推論：

公理 1: A → B
定理 1: -B
-------------
定理 2: -A

得出結論 -A ，於是我們知道在該系統下，-C, -B, -A 都是真理。

歸結推論 (Resolution)

不管是《肯定前項》還是《否定後項》，都沒有辦法推論出《命題邏輯》(也就是布林邏輯+知識庫) 的所有定理。

但是在 1960 年 Davis 和 Putnam 提出了下列的 Resolution 推論法則 (中文稱為歸結推論法)，經過 1965 年 John Alan Robinson 提出的 syntactical unification algorithm 改良後，得到了一個《完備》的推論法則，也就是可以推出所有定理的推論法則。

以下是 Resolution 推論法則的形式：

前提 1: -p | q
前提 2:  p | r
===============
結論： q | r

我們可以用下列真值表，證明這個推論法則是對的，

當我們將不符合前提的項目拿掉之後，以上的真值表就只剩以下這些項目。

此時，如果我們檢查這些項目中 q|r 的真值表，會發現 q|r 為真者其結果全部為 1 ，因此 q|r 在這個前提下是真理。

但是如果我們檢查這些項目中 p|q 的真值表，會發現有一項為 0 ，因此 p|q 在這個前提下並非真理。

所以 q|r 在此前提下是一個定理，但 p|q 則不是。

說明：在上述邏輯推論系統當中， -p|q 可以簡寫為 p → q，而 p|r 則可以想成 -(-p)|r ，於是寫成 -p → r。

於是推理法則可用箭頭的方式改寫為：

前提 1: p→q
前提 2: -p→r
===============
結論： -q→r   (也就是 q|r)

透過這樣的改寫，您可以觀察到當 p=1 時 q=1，當 p=0 時 r=1，而 p 只有可能是 1 或 0，於是 q 與 r 兩者至少有一個成立，這也就是推論出的定理 q|r 成立的原因了。

有了 Resolution 推論法則後，我們就可以證明一些單獨用《肯定前項》和《否定後項》所無法推出的定理了，舉例而言，假如我們有一個知識庫系統，擁有下列《公理》。

公理1 : -A|B
公理2 : A|C
公理3 : -(B|C)|E

那麼我們可以用 Resolution 推論如下：

公理1 : -A|B
公理2 : A|C
================
定理1： B|C

然後再用結論 B|C 與公理3，繼續推論：

公理3 : -(B|C)|E
定理1： B|C
================
定理2： E

於是我們得到了 B|C 與 E 在該《公理系統》下都是《定理》的結論。

必須注意的是，單靠 Resolution 推論法則是無法推論出所有《定理》的， 1965 年 Robinson 提出的方法，採用《反證法》，也就是當你想證明某個定理 Q 是對的，你必須先將那個定理反過來，變成 -Q 加入《公理系統》KB，然後開始推論。

假如可以由 KB+(-Q) 推出《空子句》的話，那麼就代表 KB+(-Q) 會產生矛盾。

此時如果 KB 本身是無矛盾的，那麼就代表 -Q 與 KB 矛盾，反過來看就是 Q 為真理。

因此 Robinson 的方法是一種反證法。

我們同樣用上述的公理，但是改用 Robinson 的反證法來進行推論。

公理1 : -A|B
公理2 : A|C
公理3 : -(B|C)|E

請問 E 是否為真？

首先將 -E 加入系統，得到：

公理1 : -A|B
公理2 : A|C
公理3 : -(B|C)|E
反問句：-E

然後用下列推論：

公理3 : -(B|C)|E
待證明：-E
================
結論1： -(B|C)

接著再用推論：

公理1 : -A|B
公理2 : A|C
================
結論2： B|C

最後用推論：

結論1： -(B|C)
結論2： B|C
================
結論3：

由於上式產生了《空字句》，所以證明了 KB+(-E) 有矛盾，於是 E 是真理。

公理系統有矛盾會怎樣？

假如在布林邏輯裏，我們創造出以下這樣的公理系統。

公理 1: A
公理 2: -A

那麼會發生甚麼事呢？

根據 Robinson 的推論方法，我們先把 KB+(-Q) 放進去推論，由於 KB 本身就包含了 A 與 -A ，根據 Robinson 的推論方法可以改寫如下：

公理 1: A
公理 2: -A
反問句：-Q

於是可以推論出：

公理 1: A
公理 2: -A
================
結論：

這樣就推論出《空字句》了，於是不管 Q 是甚麼，Robinson 的方法在 KB+(-Q) 之後都會推論出《空字句》，也就是任何陳述 Q 都是對的。

如果用真值表來看，一個空無一物的真值表世界裏，任何陳述都無法被否證，所以任何陳述都可以是《定理》。(所有邏輯法則都無法被否認)

謂詞邏輯 (Predicate Logic)

在布林邏輯中，只有用來代表真假值的簡單變數，像是 A, B, C, X, Y, Z .... 等，所以邏輯算式看來通常如下：

• P & (P=>Q) => Q.
• A & B & C => D | E.
• -(A & B) <=> -A | -B.

這種布林命題邏輯裏沒有函數的概念，只有簡單的命題 (Proposition)，因此布林邏輯也稱為命題邏輯 (Propositional Logic)。

而在《謂詞邏輯》(Predicate logic) 裏，則有「布林函數」的概念，因此其表達能力較強，例如以下是一些謂詞邏輯的範例。

• Parent(x,y) <= Father(x,y).
• Parent(John, Johnson).
• Ancestor(x,y) <= Parent(x,y).
• Ancestor(x,y) <= Ancestor(x,z) & Parent(z,y).

您可以看到在這種邏輯系統裏，有「布林變數」的概念 (像是 x, y, z 等等)，也有函數的概念，像是 Parent(), Father(), Ancestor() 等等。

一階邏輯(First-Order Logic)

在上述這種謂詞邏輯系統中，如果我們加上 $\forall$ (對於所有) 或 $\exists$ (存在) 這兩個變數限定符號，而其中的謂詞不可以是變項，而必須要是常項，這種邏輯就稱為一階邏輯。

• $\forall People(x) => Mortal(x)$ ; 人都是會死的。
• $People(Socrates)$ ; 蘇格拉底是人。
• $Mortal(Socrates)$ ; 蘇格拉底會死。

當然、規則可以更複雜，像是以下這個範例，就說明了「存在一些人可以永遠被欺騙」。

• $\exists x (Person(x) \wedge \forall y (Time(y) => Canfool(x,y))).$

二階邏輯 (Second-Order Logic)

如果一階邏輯中的謂詞，放寬成可以是變項的話 (這些變項可以加上 $\forall$ 與 $\exists$ 等符號的約束)，那就變成了二階邏輯，以下是一些二階邏輯的規則範例。

• $\exists P (P(x) \wedge P(y)).$
• $\forall P \forall x (x \in P | x \notin P).$
• $\forall P (P(0) \wedge \forall y( P(y)=>P(succ(y)) ) => \forall y P(y) ).$

(最後一條是《數學歸納法》規則)

對於上述這些邏輯系統而言，描述能力愈強大者，通常也愈複雜，而且《公理系統》與《推論的複雜度》也會提高，要建構出《很完美的數學體系》，難度也就愈來愈高了！

邏輯推論的程式

我們在 rlab 當中實作了兩個《邏輯推論引擎》，一個是《命题逻辑》(布林邏輯)，另一種是《謂詞邏輯》，以下是其執行範例。

範例一：簡易測試

規則庫：test.kb

A<=B. B<=C&D. C<=E. D<=F. E. F. Z<=C&D&G.

執行結果：

D:\Dropbox\github\rlab\example>node kbQuery.js test.kb
["A<=B","B<=C&D","C<=E","D<=F","E","F","Z<=C&D&G",""]
rule:head=A terms=["B"]
rule:head=B terms=["C","D"]
rule:head=C terms=["E"]
rule:head=D terms=["F"]
rule:head=E terms=""
rule:head=F terms=""
rule:head=Z terms=["C","D","G"]
addFact(E)
addFact(F)
addFact(C)
addFact(D)
addFact(B)
addFact(A)
facts=["E","F","C","D","B","A"]
?-

範例二：動物世界

規則庫：animal.kb

哺乳類 <= 有毛. 
哺乳類 <= 泌乳. 
鳥類   <= 有羽毛. 
鳥類   <= 會飛 & 生蛋. 
食肉類 <= 哺乳類 & 吃肉.
食肉類 <= 有爪 & 利齒 & 兩眼前視.
有蹄類 <= 哺乳類 & 有蹄.
偶蹄類 <= 哺乳類 & 反芻.
獵豹   <= 哺乳類 & 吃肉 & 斑點.
老虎   <= 哺乳類 & 吃肉 & 條紋.
長頸鹿 <= 有蹄類 & 長腿 & 斑點.
斑馬   <= 有蹄類 & 條紋.
鴕鳥   <= 鳥類 & 長腿.

執行結果：

D:\Dropbox\github\rlab\example>node kbQuery.js animal.kb
["哺乳類 <= 有毛","哺乳類 <= 泌乳","鳥類   <= 有羽毛","鳥類   <= 會飛 & 生蛋","
食肉類 <= 哺乳類 & 吃肉","食肉類 <= 有爪 & 利齒 & 兩眼前視","有蹄類 <= 哺乳類 &
有蹄","偶蹄類 <= 哺乳類 & 反芻","獵豹   <= 哺乳類 & 吃肉 & 斑點","老虎   <= 哺乳
類 & 吃肉 & 條紋","長頸鹿 <= 有蹄類 & 長腿 & 斑點","斑馬   <= 有蹄類 & 條紋","鴕
鳥   <= 鳥類 & 長腿",""]
rule:head=哺乳類 terms=["有毛"]
rule:head=哺乳類 terms=["泌乳"]
rule:head=鳥類 terms=["有羽毛"]
rule:head=鳥類 terms=["會飛 "," 生蛋"]
rule:head=食肉類 terms=["哺乳類 "," 吃肉"]
rule:head=食肉類 terms=["有爪 "," 利齒 "," 兩眼前視"]
rule:head=有蹄類 terms=["哺乳類 "," 有蹄"]
rule:head=偶蹄類 terms=["哺乳類 "," 反芻"]
rule:head=獵豹 terms=["哺乳類 "," 吃肉 "," 斑點"]
rule:head=老虎 terms=["哺乳類 "," 吃肉 "," 條紋"]
rule:head=長頸鹿 terms=["有蹄類 "," 長腿 "," 斑點"]
rule:head=斑馬 terms=["有蹄類 "," 條紋"]
rule:head=鴕鳥 terms=["鳥類 "," 長腿"]
facts=[]
?- 有毛
addFact(有毛)
addFact(哺乳類)
facts=["有毛","哺乳類"]
?- 斑點
addFact(斑點)
facts=["有毛","哺乳類","斑點"]
?- 吃肉
addFact(吃肉)
addFact(食肉類)
addFact(獵豹)
facts=["有毛","哺乳類","斑點","吃肉","食肉類","獵豹"]
?-

您可以看到該推理程式，根據動物知識庫，在輸入《有毛、斑點、吃肉》之後推理出了符合的動物是《獵豹》。

該程式的主要部分為於下列網址，想要仔細研究的人可以參考閱讀。

• https://github.com/ccckmit/rlab/blob/master/example/kbQuery.js
• https://github.com/ccckmit/rlab/blob/master/lib/kb.js

後記

大部分的數學系統，都希望能達到這樣嚴格的程度，但可惜的是，並非所有數學系統都能完全達到這樣嚴格的程度。

舉例而言：《歐氏幾何》可以說是公理化的早期經典之作，但其中仰賴圖形輔助的證明仍然有很多，並沒有達到《完美公理化》的程度。

後來 希爾伯特 在1899年發行《幾何基礎》教材，將歐氏幾何重新用現代方式公理化，避免了一些歐幾里得公理中的弱點。

在希爾伯特在 1900 年提出的 23 個數學問題 中，就包含了很多《公理化》的相關問題，列舉如下：

• 第1題 連續統假設
• 第2題 算術公理之相容性
• 第6題 公理化物理

其中第2題是希望建構出一個《一致且完備》的算術公理體系，希望能夠建構出可證明所有算術定理的公理系統。

28年後，《歌德爾的完備定理》讓希爾伯特的這個夢想幾乎達成了，但是又過了一年，《歌德爾的不完備定理》，粉碎了希爾伯特的這個夢想！

這將會是我們下一章《計算理論》的主題。

參考文獻

• Jserv : Formal Verification
• 維基百科：命題邏輯
• 相關討論：為甚麼國中的數學證明是從「歐式幾何」開始教，而不從「布林代數」開始教呢？
  • https://www.facebook.com/ccckmit/posts/10151056707046893
• 數學中的公理化方法 (上) 吳開朗
  • http://w3.math.sinica.edu.tw/math_media/d171/17111.pdf
• 數學中的公理化方法 (下) 吳開朗
  • http://w3.math.sinica.edu.tw/math_media/d172/17203.pdf