[科普中国]-形式系统

在逻辑与数学中，一个形式系统（英语：Formal system）是由两个部分组成的，一个形式语言加上一个推理规则或转换规则的集合。一个形式系统也许是纯粹抽象地制定出来，只是为了研究其自身。另一方面，也可能是为了描述真实现象或客观现实的领域而设计的。

定义形式系统（Formal System），包含字母、字的集合及由关系组成的有限集合。例如：集合论、布林代数、欧几里得平面几何及贝克式正规形式（Backus Normal Form）都是形式系统。1

分类常用的形式系统有：语言、数理规则和逻辑。其中由于数学的研究对象是形式系统中唯一天生的逻辑自洽系统，因此数学也被一些人称为：形式科学。而语言大类中，部分为逻辑自洽的形式系统，如计算编程用的各类程序语言等。1

理论在数学领域里，形式证明是形式系统的产物，由一些公理与演绎规则组成。定理便是形式证明可能的最后一行结论。这几个步骤总和起来便是数学界通称的形式主义。大卫·希尔伯特创立元数学以作为讨论形式系统的学科。任何用于讨论形式系统的语言称为元语言。元语言也许像普通语言一样自然，或它可能部分形式化，但它通常比起受检验系统的形式语言来得较不正规化。此形式语言称为对象语言，意指问题议论的对象。

某些理论学家将形式主义粗略视为形式系统的同义词，但此词也同时指称特定风格的符号，例如保罗·狄拉克的狄拉克符号。

在数学中的形式系统由以下要素组成：

一群有限数量，且可用于建构公式的符号集合。

一套文法，说明了如何以上述符号建构形式良好的公式（通称**合式公式，**或Wellformedformula）。通常会要求有一个判定某公式是否为形式良好的算法。

一群公设或公理模式的陈述，每个公理都必须是合式公式。

一群推理规则。

用途对于程式语言的设计、实施及研究等方面而言，形式系统扮演的角色越来越重要。2

延伸阅读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.

本词条内容贡献者为:

孙和军 - 副教授 - 南京理工大学