在
逻辑与
数学中,一个形式系统(英语:Formal system)是由两个部分组成的,一个
形式语言加上一个推理规则或转换规则的集合。一个形式系统也许是纯粹抽象地制定出来,只是为了研究其自身。另一方面,也可能是为了描述真实现象或客观现实的领域而设计的。
形式系统(Formal System),包含字母、字的集合及由关系组成的有限集合。例如:
集合论、布林代数、
欧几里得平面几何及贝克式正规形式(Backus Normal Form)都是形式系统。
常用的形式系统有:语言、数理规则和逻辑。其中由于
数学的研究对象是形式系统中唯一天生的逻辑自洽系统,因此数学也被一些人称为:
形式科学。而语言大类中,部分为逻辑自洽的形式系统,如计算编程用的各类程序语言等。
在数学领域里,形式证明是形式系统的产物,由一些公理与演绎规则组成。定理便是形式证明可能的最后一行结论。这几个步骤总和起来便是数学界通称的
形式主义。
大卫·希尔伯特创立
元数学以作为讨论形式系统的学科。任何用于讨论形式系统的语言称为
元语言。元语言也许像普通语言一样自然,或它可能部分形式化,但它通常比起受检验系统的形式语言来得较不正规化。此形式语言称为
对象语言,意指问题议论的对象。
某些理论学家将形式主义粗略视为形式系统的同义词,但此词也同时指称特定风格的符号,例如
保罗·狄拉克的
狄拉克符号。