形式系統

在邏輯與數學中，一個形式系統（英語：Formal system）是由兩個部分組成的，一個形式語言加上一個推理規則或轉換規則的集合。大衛·希爾伯特在1921年推動以形式系統來描述數學知識 。 一個形式系統也許是純粹抽象地制定出來，只是為了研究其自身。另一方面，也可能是為了描述真實現象或客觀現實的領域而設計的。命題邏輯是最簡單的形式系統。

理論

在數學領域裏，形式證明是形式系統的產物，由一些公理與演繹規則組成。定理便是形式證明可能的最後一行結論。這幾個步驟總和起來便是數學界通稱的形式主義。大衛·希爾伯特創立元數學以作為討論形式系統的學科。任何用於討論形式系統的語言稱為元語言。元語言也許像普通語言一樣自然，或它可能部分形式化，但它通常比起受檢驗系統的形式語言來得較不正規化。此形式語言稱為對象語言，意指問題議論的對象。

某些理論學家將形式主義粗略視為形式系統的同義詞，但此詞也同時指稱特定風格的符號，例如保羅·狄拉克的狄拉克符號。

在數學中的形式系統由以下要素組成：

1. 一群有限數量，且可用於建構公式的符號集合。
2. 一套文法，說明了如何以上述符號建構形式良好的公式（通稱合式公式，或Well-formed formula，wff）。通常會要求有一個判定某公式是否為形式良好的演算法。
3. 一群公設或公理模式的陳述，每個公理都必須是合式公式。
4. 一群推理規則。

延伸閱讀

• 雷德蒙·斯穆里安 (Raymond M. Smullyan), 1961. Theory of Formal Systems: Annals of Mathematics Studies, Princeton University Press (April 1, 1961) 156 pages ISBN 069108047X
• S. C. Kleene, 1967. Mathematical Logic Reprinted by Dover, 2002. ISBN 0486425339
• Geoffrey Hunter, 1996. Metalogic: An Introduction to the Metatheory of Standard First-Order Logic University of California Press 1996. ISBN 0520023560
• Douglas Hofstadter, 1979,. Gödel, Escher, Bach: An Eternal Golden Braid ISBN 978-0465026562. 777 pages.

外部連結

• Encyclopædia Britannica, Formal system （頁面存檔備份，存於互聯網檔案館） definition, 2007.
• Christer Blomqvist, an introduction to formal systems, webpage 1997.
• What is a Formal System? （頁面存檔備份，存於互聯網檔案館）: Some quotes from John Haugeland's `Artificial Intelligence: The Very Idea' (1985), pp. 48–64.
• Heinrich Herre Formal Language and systems, 1997.
• Peter Suber, Formal Systems and Machines: An Isomorphism （頁面存檔備份，存於互聯網檔案館）, 1997.