##EasyReadMore##

11.16.2012

公理,定理,引理和系理

對象語言(object language)和後設語言(metalanguage)
當有人用英文研究拉丁文時,對象語言是拉丁文,後設語言是英文。對象語言和後設語言可以是同一套語言,例如用中文研究中文的時候。基本上,後設語言中要具備對象語言裡的所有符號,不然討論對象語言時可能會遇上困難。例如,若只用中文研究英文,便無法寫出「water的意思是水」這種句子,因為後設語言裡沒有英文字母;若後設語言是一套由英文字母和中文構成的語言,就可以。我們在用中文、英文和某邏輯語言的符號,討論該邏輯語言時,對象語言是該邏輯語言,後設語言是一套由中文、英文和該邏輯語言的符號構成的語言。
公理(axiom)
在邏輯系統中,不需要證明就可以拿來用的句式(formula)便是公理。你可以問選這些句式當公理有什麼好處,但沒辦法要求證明這些句式。如果你覺得某邏輯系統的其中一些公理不能滿足你的需求(例如,不能完美模仿人類的推論方式),可以另闢一套邏輯系統,放自己喜歡的公理。但那套系統有沒有研究價值、是否有人想用則是另一回事。
定理(theorem)
僅利用某邏輯系統的公理,或利用公理及系統允許的推論規則就能證明的句式,便是該邏輯系統的定理。根據定義,任一邏輯系統的公理均是其定理。
定理還有另一個意思。對象語言是某套邏輯系統的邏輯文章裡,定理通常指作者主要想證明的句子,這個句子使用後設語言有,但對象語言沒有的符號描述該邏輯系統的性質。因為這種定理中出現了那套邏輯語言沒有的符號,所以無法被該邏輯系統的公理或推論規則證明。語句邏輯的演譯定理(deduction theorem)便是這樣的句子。第二種意思的定理被稱為後設定理(metatheorem)。
引理(lemma)
引理也是用後設語言描述邏輯系統的性質的句子。引理通常指,用來幫助證明後設定理的重要踏腳石。是後設定理還是引理,端賴它在文章中是否為作者的主要目標,因此可能發生,同一個句子在這篇文章中是引理,在另一篇文章中是後設定理的情況。
系理(corollary)
系理也是用後設語言描述邏輯系統的性質的句子。後設定理蘊含的一些重要結果便是系理,至於哪些被蘊含的結果才是重要的,則由作者決定;作者大多會選和他等一下要討論的事有關的結果當系理。一但證明後設定理,要證明該後設定理的系理通常很容易。