介紹
形式系統(Formal System),包含字母、字的集合及由關係組成的有限集合。例如:
集合論、布林代數、
歐幾里得平面幾何及貝克式正規形式(Backus Normal Form)都是形式系統。
常用的形式系統有:語言、數理規則和邏輯。其中由於
數學的研究對象是形式系統中唯一天生的邏輯自洽系統,因此數學也被一些人稱為:
形式科學。而語言大類中,部分為邏輯自洽的形式系統,如計算編程用的各類程式語言等。
在數學領域裡,形式證明是形式系統的產物,由一些
公理與演繹規則組成。定理便是形式證明可能的最後一行結論。這幾個步驟總和起來便是數學界通稱的
形式主義。
大衛·希爾伯特創立
元數學以作為討論形式系統的學科。任何用於討論形式系統的語言稱為
元語言。元語言也許像普通語言一樣自然,或它可能部分形式化,但它通常比起受檢驗系統的形式語言來得較不正規化。此形式語言稱為
對象語言,意指問題議論的對象。
某些理論學家將形式主義粗略視為形式系統的同義詞,但此詞也同時指稱特定風格的
符號,例如
保羅·狄拉克的
狄拉克符號。
組成要素
在數學中的形式系統由以下要素組成:
一群有限數量,且可用於建構公式的符號集合。
一套文法,說明了如何以上述符號建構形式良好的
公式(通稱
合式公式,或Wellformedformula)。通常會要求有一個判定某公式是否為形式良好的算法。
一群公設或公理模式的陳述,每個公理都必須是
合式公式。
一群推理規則。
用途
對於程式語言的設計、實施及研究等方面而言,形式系統扮演的角色越來越重要。
延伸閱讀
Raymond M. Smullyan, 1961.Theory of Formal Systems: Annals of Mathematics Studies, Princeton University Press (April 1, 1961) 156 pagesISBN 069108047X
S. C. Kleene, 1967.Mathematical LogicReprinted by Dover, 2002.ISBN 0486425339
Geoffrey Hunter, 1996.Metalogic: An Introduction to the Metatheory of Standard First-Order LogicUniversity of California Press 1996.ISBN 0520023560
Douglas Hofstadter, 1979,.Gödel, Escher, Bach: An Eternal Golden BraidISBN 978-0465026562. 777 pages.