形式系统

把公理系统形式化而得的系统。一个公理系统以若干初始概念和一组公理作为出发点，用初始概念定义系统中的其它概念，从公理出发证明系统中的定理。把一个公理系统或理论形式化，就是用一种人工语言——形式语言陈述所形式化的理论，把所形式化的理论中的概念转换为形式语言中的符号或符号表达式，把所形式化的理论中的公理和定理转换为形式语言中的符号公式，并且把普通公理系统中证明定理时用的逻辑工具转换为形式语言中的一组符号公式和关于符号变换的变形规则，而把定理的证明转换成符号公式的变形，把一个证明转换为符号公式的有穷序列。一个普通的公理系统中的概念，公理等都是有意义的，意义是抽象的，往往不容易精确理解和掌握。并且用自然语言表达的概念和命题，往往达不到精确严格的要求，容易产生歧义。而形式系统中的符号、公式以及公式的变形等等，都是具体的对象，并且满足某些明确的要求，能够对它们作精确严格的处理和研究，从而通过对具体对象的研究而达到对抽象的东西的把握。

一个形式系统包括3个部分。①语言。建立一个语言，首先要列出各种初始符号，然后是列出一组形成规则。初始符号的有穷序列称为表达式。形成规则规定怎样的表达式是合式公式，简称公式。在形式系统中，初始符号和公式都只是一些没有任何意义的具体对象。但是，对它们作解释后，其中一部分就成为逻辑概念，有的则成为一个有意义的理论的基本概念。有的表达式是无意义的符号组合，而根据形成规则组成的表达式——公式，经解释后就成为有意义的命题。形式系统的语言通常称为形式语言。

②形式系统的第二个组成部分是它的公理。公理是挑选出来作为出发点的一组公式。对公理的唯一要求是，每一公理都是形式系统的语言的公式。但是，在挑选公理时，通常都希望使得由公理所组成的系统具有某些重要的性质。

③形式系统的第三个组成部分是一组变形规则，也称为推理规则或推演规则，简称规则。每一变形规则规定怎样从一个或一组公式(称为规则的前提)通过符号变换得出另一公式(称为规则的结论)。变形规则使人们能从公理推导出定理。形式系统的定理如下归纳地定义：1，系统的每一公理都是定理；2，如果一个规则的所有前提都是系统的定理，则该规则的结论也是定理。

严格的形式化和形式系统的概念，与精确的机械的程序概念和能行可判定概念分不开。所谓机械的程序，就是每一步都由事先给定的规则明确规定了的：第一步如何作，在完成某一步之后下一步如何作，并且在有穷步内能够结束。所谓能行可判定，是指对一类问题有一机械的程序，对任给该类中的问题，能在有穷步内确定它是否有某个性质，或者任给一个对象能在有穷步内确定它是否属于该类。

对于形式系统的一个重要的要求，就是有机械的程序并可能行地判定：①任给一符号是不是系统中的初始符号。②任给一符号的有穷序列是不是系统中的合式公式。③任给一公式是不是系统的公理。④任给一公式是不是从给定的公式(作为规则的前提)根据一规则而得的。⑤任给一公式的有穷序列是不是一个证明。由于一个形式系统满足这样一些要求，因而可以对形式系统的许多重要的性质作系统深入的研究。但是，任给一公式是不是系统的定理，一般不是能行地可判定的。

由以上对形式系统的说明可知，一个形式系统是由它的符号、公式、公理和规则等完全确定了的。虽然每个形式系统都有逻辑推理系统或数学公理系统作为它的背景，即式系统可以被解释为逻辑推理规律的理论或某个数学理论，但是系统的解释或意义不认为是系统的一部分。这就使得形式系统本身成为一个纯语法的对象。把公理、定理等作为形式语言的公式、语句来研究，称为公理系统的语法研究。形式系统是公理系统的语法部分，形式系统的解释或意义称为语义。例如形式系统的公式在一个解释下的真假就是一个语义性质，真假是语义概念。模型、解释等也是语义概念，这方面的研究称为语义研究。

明确的形式化和形式系统的概念，是D．希尔伯特在20世纪20年代初提出的。形式化的明确提出和形式系统的建立对数理逻辑的发展有十分重大的意义，也对数学特别是数学基础的研究有重要的意义。对形式系统能作严格的数学处理，讨论其性质，包括语法的性质和语义的性质，得出关于形式系统的元逻辑性质的一般结论。例如，哥德尔完全性定理和哥德尔不完全性定理，都是关于形式系统的性质的重要定理。形式系统的建立，开辟了以形式系统为研究对象的元逻辑研究领域。