5/25/2009

formalization of deductive systems(Intro)

我們會在這個世界裡尋找一些關於真的事物, 這些事物通常有普遍上的規律性, 大部分會集中在數學的entity當中。對哲學或者邏輯學而言, 我們不僅要尋找規律性, 我們還要給一些可以支持這些entity的理由和證明。只有證明卻沒有哲學上的理由是無法說服人的。這類工作的源頭, 最早可以追溯至Aristotle, 他掀起了研究邏輯的旗幟, 特別是在演繹邏輯(deduction)的部分。演繹的方法很容易可以理解, 就是從一些前提得到結論並且保證結論為真。同時, 演繹邏輯也顯示了一些確定的方法來classify有效推論(或是有效的邏輯結果(consequence))和無效推論。

一個好的有效推論是建構在一套有用的systematic account上, 研究這類系統的工作叫做形式(formal logic)。

形式邏輯在G.Frege的著作Begriffschrift(1879)出版之後蓬勃發展,不論是在數學上或是哲學上都有相當大的影響。"形式邏輯"這個字眼,往往不能望文生義, 總而言之它是演繹系統家族的一支。現在我要嘗試簡扼地說, 一個演繹系統一般上要包含哪些東西。

(一)一個形式語言(formal language)包含:
1.使用的字元或字母(alphabet), 用途在當作我們做形式推論時,代表我們推論的東西。常常有人覺得, 這種方式和數學很像甚至於一樣。包括在下小女子我也曾經這麼覺得。後來發現, 有許多推論和證明並不是推論結束, 或是證明完成以後就算完工了。這點和數學工作並不全然一樣。
2.一個有限的形式規則(formal rules)所形成的集合。這裡的重點和"集合"並沒有太大關係, 主要是提供我們在做推論的時候, 保證我們寫出的語句都是合法句子(well-formed formula, wff)。就像:

It is raining. 是一個合法句子。但是:
rs Ia gnniiit. 不是一個合法句子。

所以,提供一些formal rules就只是為了保證寫出的句子你都看得懂。taht's all,沒什麼特別的。

(二)提供一套語意學來解讀我們所使用的字元與符號, 這樣, 我們就能夠去得到一個句子的真值(truth value)。這件事情相對上比較重要。因為解讀句子的方法會透出該系統所持的一些理論觀點, 包括它在哲學上的預設及立場。就像我們與別人相處的時候, 我們會用一些方法來解讀我們接收的句子表示什麼意思。粗淺地講就是如此。

我們有了字元和推論規則,再加上語意學, 我們就可以定義"有效"這個概念, 而某些真理就能被刻畫出來。順帶一提, 在邏輯裡, 真理這件事情不是很複雜的事, 有效的句子就是邏輯真理。甚至於有些非古典的邏輯系統並沒有邏輯真理

(三)一個形式系統包含有
1.可以定義"證明(proof/derivation)"概念,
1.1一組式子(formulae)的集合, 這個集合也可能是空集合, 也就是說這個集合裡啥都沒有, 總而言之這個集合叫做公理(axioms),
1.2一組轉換規則所形成的集合, 這個集合是有限的集合, 而這組規則也叫做推論規則(rules of inference),
2.可以定義定理(theoremthood)。

說到裡, 我還要碎碎念一些事。

在邏輯裡, 選擇哪一組推論規則會直接影響到所選擇的型式系統。因為不同型式系統會牽涉到不同語意學。這就像我們選擇用哪些語言溝通一樣, 一個詩人喜歡用某些詞來說話, 一個乞丐也會用他熟悉的方式和其他流浪和溝通, 黑道有黑道的術語, 白道有白道的術語, 若不是同道中人, 大概很難理解他們到底在說什麼吧!類似這樣的感覺。

演繹系統可以分成兩類, 命題邏輯和述詞邏輯。在1930年代,演繹系統就相當於命題邏輯,和述詞邏輯。命題邏輯的演算稱為CPC, 數詞邏輯的演算稱為CQC。後來產生了許多重要的後設定理(metatheorems)和證明成果, 例如compactnes theorem, soundness theoerm, completeness theorem。研究這些後設定理和證明這些後設定裡是形式邏輯最重要的工作之一。

自從形式邏輯發展開始, 後續產生了許多不同建構邏輯系統的方式。但是沒有一套邏輯系統是可以被完全接受的, 發掘更好的邏輯系統是首要工作, 當然我們還是有一些主要的系統:

(a) Hibert-Frege style(axiom)systems,
(b)System of natural deduction,
(c)(Formal) tableaux sytem,
(d)Sequent calauli。

我的翻譯不是很好, 大概就是希爾柏特,佛列格的公理系統,自然演繹系統,形式的真值表系統,最後一個很難翻,基本上就是從一堆語句經過推論規則得到計算果的意思。

這些資訊都是由台大哲學系楊金穆老師自編的教材得來的。

沒有留言:

張貼留言