[转贴]公理化和形式化

gghhjj

公理化和形式化

axiomatization and formalization


    研究演绎科学理论和构造演绎系统的两种方法。它们被广泛应用于现代逻辑和数学研究中。
    公理化　把一个科学理论公理化，就是用公理方法研究它，建立一个公理系统。每一科学理论都是由一系列的概念和命题组成的体系，公理化的实现就是：①从它的诸多概念中挑选出一组初始概念，即不加定义的概念，该理论中的其余概念，都由初始概念通过定义引入，即都用初始概念定义，称为导出概念；②从它的一系列命题中挑选出一组公理，即不加证明的命题，而其余的命题，都应用逻辑规则从公理推演出来，称为定理。应用逻辑规则从公理推演定理的过程称为一个证明，每一定理都是经由证明而予以肯定的。由初始概念、导出概念、公理以及定理构成的演绎体系，称为公理系统。其中，初始概念和公理是公理系统的出发点。
    公理方法经历了从古代的实质公理学到现代的形式公理学的发展过程。
    公理系统相应地区分为古典公理系统、现代公理系统或称形式公理系统。最有代表性的古典公理系统是古希腊数学家欧几里得在《几何原本》一书中建立的。第一个现代公理系统是D.希尔伯特于1899年提出的。他在《几何基础》一书中，不仅建立了欧几里得几何的形式公理系统，而且也解决了公理方法的一些逻辑理论问题。
    古典公理系统的对象域即公理系统所研究的对象，是先于公理而给定的,概念是对象的反映,公理则反映对这些对象的认识，表达这类对象的重要性质和关系。古典公理系统的初始概念和公理都有直观的具体内容，而系统的公理和定理是关于这对象域的真命题。从认识的发展来看，现代形式公理系统虽然一般也是从某种直观理论得到的，并且通常有预先想到的解释。但是，系统自身并不给初始概念予直观的具体内容，它们的意义完全由公理规定，对初始概念和公理可以给予不同的解释，可以刻划多个不同的对象域，即有多个不同的对象域都可以使得一个公理系统的公理和定理为真，它们在不同的解释下成为不同对象域的真命题。
    公理系统要满足某些一般要求，包括系统的一致性、完全性和范畴性，以及公理的独立性。其中一致性是最重要的，其他几个性质则不是每个公理系统都能满足的，或可以不必一定要求的。
    形式化　公理系统的进一步形式化不仅可以有不同的解释，而且需要应用专门设计的人工符号语言，使一个理论更为精确化和严格化，也就是运用人工的表意符号语言陈述所要形式化的理论。这种人工语言称为形式语言。把一个理论形式化就是把理论中的概念转换为形式语言中的符号，命题转换为符号公式，定理的推演转换成符号公式的变形，并把一个证明转换成符号公式的有穷序列。形式语言的符号和它们所表示的概念之间的对应是确定的，符号公式的结构反映它们的意见。把一个理论形式化后，就可以暂时完全撇开原来理论中的概念、命题的意义，而只从语言符号、公式结构（符号组合的形状）方面研究。意义是抽象的，往往不容易精确理解和掌握。而符号和公式是有穷的具体的对象，能够对其作更精确、更严格的研究，从而通过对具体对象的研究把握抽象的东西。
    形式系统　把一个理论形式化的结果是建立形式系统。形式系统是形式化了的公理系统，它包括以下 3个部分：①形式语言。规定一个形式语言，首先要列出各种初始符号，它们是形式语言的字母，其中一部分是初始概念，包括逻辑概念；然后再列出一组形成规则，形成规则规定怎样由初始符号组合起来的符号序列是系统中的合式公式，只有合式公式才是有意义的命题，而不合式的符号序列则是无意义的。②形式系统的公理。公理是挑选出来作为出发点的一组合式公式，它们经解释后可以是真的命题。③一组变形规则，也称为推导规则。变形规则规定怎样从一个或几个合式公式经过符号变换而推导出另一合式公式。形式系统的证明是合式公式的有穷序列，其中每一公式或是一公理，或者是从在前的公式根据变形规则推导出来的。一个证明也称作它的最后一个公式的证明,一个合式公式也是系统中的定理,当且仅当存在它的一个证明。
    严格的形式化和形式系统的概念，与精确的机械的程序概念和能行可判定概念分不开。所谓机械的程序，每一步都是由事先给定的规则明确规定了的，规则规定了第一步如何作，在完成某一步之后下一步如何作，并且在有穷步后能够结束。所谓能行可判定，是指对一类问题有一机械的程序，对任给该类中的问题，能在有穷步内确定它是否有某个性质，或者任给一对象能在有穷步确定它是否属于该类。
    对于形式系统的一个最重要的要求，就是有机械的程序并可能行地判定：①任给一符号是不是系统中的初始符号；②任给一符号的有穷序列是不是系统中的合式公式； ③任给一合式公式是不是公理；④任给一合式公式是不是从给定的合式公式根据变形规则得到的；⑤任给一合式公式的有穷序列是不是一个证明。根据这些要求，虽然一般地说，在形式系统中给定一公式时，并没有一个机械程序找出它的证明，但只要任给一有穷的公式序列，就能机械地判明它是否确实是本系统中的一个正确的证明。这样就可以对于一个形式化的公理系统的许多逻辑性质进行科学的研究。
    明确的形式化和形式系统的概念是希尔伯特在20世纪20年代初提出的。形式化的明确提出和形式系统的建立，在公理学发展史上有着十分重大的意义。它标志着以形式系统为研究对象的元逻辑或元数学的诞生，对现代逻辑科学的发展起了重大的作用。
     （张尚水）