正規系統

维基百科，自由的百科全书

在邏輯與數學中，一個正規系統（formal system）是由兩個部分組成的，一個正規語言加上一個推理規則（inference rule）或轉換規則（transformation rule）。一個正規系統也許為了其目的，是純粹抽象的方程式，但也可能是為了描述真實現象或實際物件的領域而設計的。

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

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

在數學中的正規系統由以下要素組成：

1. 一群有限數量，且可用於建構公式的符號集合。
2. 一套文法，例如以上述符號建構且形式良好的公式，這樣系統才能發現一個判定此公式是否為形式良好（通稱良好形式公式，或Well-formed formula，wff）的演算法。
3. 一群公設或公設的概述，每個公設都必須是wff。
4. 一群推理規則。
5. 一群理論，此集合包含所有公設，加上所有可從之前完成推導的理論，經由推論規則衍生而來且wff的理論。文法定義的wff，在這裡不一定可找到合適的演算法判定此wff是否為一個合法的理論。（以自然語言為例，合乎文法的句子不一定含有可理解的文義，例如「我的弟弟長得欣欣向榮。」或「天黑了，爸爸陸陸續續回家了。」）