形式系统

逻辑数学中,一个形式系统(英语:Formal system)是由两个部分组成的,一个形式语言加上一个推理规则或转换规则的集合。大卫·希尔伯特在1921年推动以形式系统来描述数学知识[1] 。 一个形式系统也许是纯粹抽象地制定出来,只是为了研究其自身。另一方面,也可能是为了描述真实现象或客观现实的领域而设计的。命题逻辑是最简单的形式系统。

理论

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

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

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

  1. 一群有限数量,且可用于建构公式的符号集合。
  2. 一套文法,说明了如何以上述符号建构形式良好的公式(通称合式公式,或Well-formed formula,wff)。通常会要求有一个判定某公式是否为形式良好的算法。
  3. 一群公设或公理模式的陈述,每个公理都必须是合式公式
  4. 一群推理规则

延伸阅读