布林邏輯與公理系統· 把數學程式化

布林邏輯只有兩個值，那就是0 與1 ，所以可以說是最簡單的數學體系了，就讓我們從布林邏輯開始，理解何謂公理系統吧！ 何謂嚴格的數學證明？ 當我還是個學生時，我總是困惑 ... 把數學程式化--使用JavaScript的Rlab套件 Introduction Rlab科學計算套件 數值表示法 布林邏輯與公理系統 計算理論 集合論 測度論 代數 代數結構：群與體 求解方程式 微積分 微分方程 矩陣 線性代數 機率 統計 函數逼近 幾何學 PoweredbyGitBook 布林邏輯與公理系統 布林邏輯與公理系統 想要理解甚麼是數學，最快速的捷徑是從公理系統下手，因為公理系統是數學證明的核心，理解了公理系統之後，就可以看懂數學家到底在玩甚麼遊戲了！ 但是、很多數學的公理系統太過複雜，因此很難解釋，讀者往往在還沒入門之前，就已經先恍神了，所以為了讓大家很容易的理解公理系統，我們選擇了一個最簡單的數學體系，那就是布林邏輯。

布林邏輯只有兩個值，那就是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)的真值表，只要透過列舉的程序就可以檢查完畢。

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

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

公理1:-A|B 公理2:-B|C 公理3:A 當我們制定完公理系統之後，這些公理就無條件地成立了，而且每一條都成立。

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

讓我們列出上述系統的真值表，看看這樣的公理系統代表甚麼意義？ A B C -A｜B -B｜C 0 0 0 1 1 0 0 1 1 1 0 1 0 1 0 0 1 1 1 1 1 0 0 0 1 1 0 1 0 1 1 1 0 1 0 1 1 1 1 1 在上述真值表中，那些不符合公理者都可以先刪除，這樣我們就得到下列的《剩餘真值表》。

A B C -A｜B -B｜C 1 1 1 1 1 結果只剩下一個可能性，也就是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的真值表定義，也就是下列的三個表格。

x -x 0 1 1 0 x y x&y 0 0 0 0 1 0 1 0 0 1 1 1 x y x｜y 0 0 0 0 1 1 1 0 1 1 1 1 根據AND,OR,NOT三個表格，我們可以建構出一些定理，舉例而言，在布林邏輯裏很有用的《迪摩根定理》就可以用真值表檢核如下： x y -(x｜y) -x&-y -(x&y) -x｜-y 0 0 1 1 0 0 0 1 0 0 0 0 1 0 0 0 0 0 1 1 0 0 1 1 您可以發現-(x｜y)和-x&-y兩者的真值是一樣的，-(x&y)與(-x｜-y)兩者的真值也是一樣的。

因此、我們得到下列兩個定理： -(x｜y)=-x&-y -(x&y)=-x｜-y 這就是所謂的《迪摩根定理》(DeMorgan'slaws)。

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

問題是、如果不用真值表，那麼還有甚麼方法可以《找出定理》呢？ 答案當然是有的、那就是用《推論法則》！ 肯定前項(ModusPoens) 舉例而言，以下是布林邏輯的一組推論法則。

前提1:-p|q 前提2:p ------------------- 結論：q 各位心裡應該不免納悶，為何這樣的推論法則成立呢？ 其實這樣的法則，一樣是從《真值表》得來的！ 我們就可以列出上述推論法則中，前提與結論的真值表如下： p q -p｜q 0 0 1 0 1 1 1 0 0 1 1 1 在上述真值表中，凡是無法滿足前提的列，就代表該項目違反前提，可以被刪除(不符合前提)： 在上述表格中，前兩條的p為0，因此不滿足前提2，而第三條的-p|q為0，不滿足前提1，因此符合前提的項目就只剩下了一個如下。

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

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

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

前提1:p→q 前提2:p ------------------ 結論：q 於是我們可以得到下列《代換式》，這種代換式就是一組推論法則。

p;p→q ----------- q 以上這組推論法則，稱為Modusponens，中文可以稱為《肯定前項》！ 有了上述推論法則後，我們就可以進行知識推理了，讓我們看看前面知識庫的例子。

公理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 否定後項(ModusTollens) 當然、布林邏輯的推理法則不只《肯定前項》一種，您還可以想出很多種推理法則。

另一種正確的推理法則，是採用《否定後項》的方式，其形式如下： 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年JohnAlanRobinson提出的syntacticalunificationalgorithm改良後，得到了一個《完備》的推論法則，也就是可以推出所有定理的推論法則。

以下是Resolution推論法則的形式： 前提1:-p|q 前提2:p|r =============== 結論：q|r 我們可以用下列真值表，證明這個推論法則是對的， p q r -p｜q p｜r 0 0 0 1 0 0 0 1 1 1 0 1 0 1 0 0 1 1 1 1 1 0 0 0 1 1 0 1 0 1 1 1 0 1 1 1 1 1 1 1 當我們將不符合前提的項目拿掉之後，以上的真值表就只剩以下這些項目。

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

p q r -p｜q p｜r q｜r p｜q 0 0 1 1 1 1 0 0 1 1 1 1 1 1 1 1 0 1 1 1 1 1 1 1 1 1 1 1 但是如果我們檢查這些項目中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都是對的。

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

(所有邏輯法則都無法被否認) 謂詞邏輯(PredicateLogic) 在布林邏輯中，只有用來代表真假值的簡單變數，像是A,B,C,X,Y,Z....等，所以邏輯算式看來通常如下： P&(P=>Q)=>Q. A&B&C=>D|E. -(A&B)<=>-A|-B. 這種布林命題邏輯裏沒有函數的概念，只有簡單的命題(Proposition)，因此布林邏輯也稱為命題邏輯(PropositionalLogic)。

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

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

∀People(x)=>Mortal(x)\forallPeople(x)=>Mortal(x)∀People(x)=>Mortal(x);人都是會死的。

People(Socrates)People(Socrates)People(Socrates);蘇格拉底是人。

Mortal(Socrates)Mortal(Socrates)Mortal(Socrates);蘇格拉底會死。

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

∃x(Person(x)∧∀y(Time(y)=>Canfool(x,y))).\existsx(Person(x)\wedge\forally(Time(y)=>Canfool(x,y))).∃x(Person(x)∧∀y(Time(y)=>Canfool(x,y))). 二階邏輯(Second-OrderLogic) 如果一階邏輯中的謂詞，放寬成可以是變項的話(這些變項可以加上∀\forall∀與∃\exists∃等符號的約束)，那就變成了二階邏輯，以下是一些二階邏輯的規則範例。

∃P(P(x)∧P(y)).\existsP(P(x)\wedgeP(y)).∃P(P(x)∧P(y)). ∀P∀x(x∈P∣x∉P).\forallP\forallx(x\inP|x\notinP).∀P∀x(x∈P∣x∉P). ∀P(P(0)∧∀y(P(y)=>P(succ(y)))=>∀yP(y)).\forallP(P(0)\wedge\forally(P(y)=>P(succ(y)))=>\forallyP(y)).∀P(P(0)∧∀y(P(y)=>P(succ(y)))=>∀yP(y)). (最後一條是《數學歸納法》規則) 對於上述這些邏輯系統而言，描述能力愈強大者，通常也愈複雜，而且《公理系統》與《推論的複雜度》也會提高，要建構出《很完美的數學體系》，難度也就愈來愈高了！ 邏輯推論的程式 我們在rlab當中實作了兩個《邏輯推論引擎》，一個是《命题逻辑》(布林邏輯)，另一種是《謂詞邏輯》，以下是其執行範例。

範例一：簡易測試 規則庫：test.kb A<=B.B<=C&D.C<=E.D<=F.E.F.Z<=C&D&G. 執行結果： D:\Dropbox\github\rlab\example>nodekbQuery.jstest.kb ["A<=B","B<=C&D","C<=E","D<=F","E","F","Z<=C&D&G",""] rule:head=Aterms=["B"] rule:head=Bterms=["C","D"] rule:head=Cterms=["E"] rule:head=Dterms=["F"] rule:head=Eterms="" rule:head=Fterms="" rule:head=Zterms=["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>nodekbQuery.jsanimal.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:FormalVerification 維基百科：命題邏輯 相關討論：為甚麼國中的數學證明是從「歐式幾何」開始教，而不從「布林代數」開始教呢？ 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 resultsmatching"" Noresultsmatching""