形式化了的公理系统。它包括以下三个部分：⑴形式语言。规定一个形式语言，首先要列出各科初始符号，它们是形式语言的字母，其中一部分是初始概念，包括逻辑概念；然后再列出一组形成规则，形成规则规定怎样由初始符号组合起来的符号序列是系统中的合式公式，只有合式公式才是有意义的命题。⑵形式系统的公理。公理是挑选出来作为出发点的一组合式公式，它们经解释后可以是真命题。⑶一组变形规则，也称为推导规则。变形规则规定怎样从一个或几个合式公式经过符号变换而推导出另一合式公式。形式系统的证明是合式公式的有穷序列，其中每一公式或是公理，或者是从在前的公式根据变形规则推导出来的。一个证明也称作它的最后一个公式的证明，一个合式公式也是系统中的定理，当且仅当存在它的一个证明。对于形式系统的一个最重要的要求，就是有机械的程序并可能行地判定：⑴任给一符号是不是系统中的初始符号；⑵任给一符号的有穷序列是不是系统中的合式公式；⑶任给一合式公式是不是公理；⑷任给一合式公式是不是从给定的合式公式根据变形规则得到的；⑸任给一合式公式的有穷序列是不是一个证明。所谓机械的程序的，即每一步都是由事先给定的规则明确规定了，第一步如何作，在完成某一步之后下一步如何作，并且在有穷步后能够结束。所谓能行可判定的，即指对一类问题有一机械的程序，对任给该类中的问题，能在有穷步内确定它是否有某个性质，或者任给一对象能在有穷步确定它是否属于该类。
形式系统(语言)
形式系统(语言)：