形式化公理系统

形式化公理系统介绍

  数学区别于其他科学的特点就是它的规律只有加以证明才能被承认。感性直观只是启发人们发现问题和思考问题的手段，而不能成为判断数学规律成立的依据，但我们并不能对所有的规律都加以证明，总要有些初始的规律是不加证明而被承认的，因为不存在证明它们的更加初始的规律。我们将某些初始的规律称为公理，它们不需要证明即被承认。由公理出发，按一定的逻辑推理规则推出的规律称为定理，推导的过程称为证明。
  数学的概念要求有精确的定义。所谓定义，就是用已有的概念去规定新概念的含义，即揭示新概念的内涵。但总有些初始的概念是不能定义的，因为不存在定义这些概念的更加初始的概念。我们将这些概念称为基本概念，对它们不予定义，即是不能定义的。用基本概念和已经定义的概念定义出的概念，称为导出概念。基本概念与导出概念、公理以及定理组成的结构称为公理系统。公理系统可以是关于某一数学学科全体的，如平面几何、集合论，也可以是关于某一数学学科中的一部分，如实数理论。公理学的发展经历了两个阶段。第一阶段是古典公理学或称为实质公理学，它是密切联系某种特殊对象的，称为公理的对象域。公理是关于这种对象的认识，表达这类对象的性质，而且有直观的明显性，如欧式几何中的公理就是实质公理。第二阶段是现代公理学，或称为形式化公理学，它不要求给定某种具体对象。群、环、线性空间等都是现代公理学或形式化公理学。
  在形式化公理系统中，原始概念的直觉意义被忽略，甚至没有任何预先设定的意义。公理也无需任何实际意义为背景，它们仅仅是一些选定的有穷符号串，唯一可识别的是它们的表示形式，这也是它们唯一有意义的东西。推理规则视为符号串的变形规则，推理或证明视为符号串的变形过程，也就是满足一定条件的有穷符号行的有穷序列。定理当然也是符号的有穷序列。因此，公理系统不再是一些有意义的命题的体系，而是一些符号的有穷序列的体系，只是靠符号形式来区别哪些是公理，哪些是定理。
  当然抽象的形式化公理系统的提出往往是有客观背景的，常常 是因为现实世界的某些对象及其性质需要精确的刻画和深入的研究。但是一旦抽象的形式公理系统建成，它便是超脱客观背景的，它可刻画的对象已不限于原来考虑的那些对象，而是与它们有着（公理所规定的）共同结构的相当广泛的一类对象，因而对它们性质的讨论也必定深刻得多。因此对一个抽象的形式公理系统，一般会有多种解释（释例）。例如，Boole代数抽象公理系统，可以解释为有关命题真值的命题代数，有关电路设计研究的开关代数，也可以解释为讨论 集合的集合代数。
  形式化是数理逻辑的基本特性和重要工具。借助于形式化过程和对形式系统的研讨完成对思维规律或其他对象理论的研究。数理逻辑形式系统的组成如下：

  (1) 用于将概念符号化的语言，通常为一形式语言(formal languages)，包括符号表 $\Sigma$ 及语言的文法，可生成表示对象的语言成分项(terms)，表示概念、判断的公式（formulas）。
  (2) 表示思维规律的逻辑学公理模式和推理规则模式（抽象的形式公理系统），及其依据它们推演出的全部定理组成的理论体系。

  根据其组成，对数理逻辑形式系统的研究包括以下3个方面：

  (1) 语构(syntax)的研究。在形式系统内首先是对系统内定理推演的研究，如哪些是系统内的定理，如何更快地导出这些定理，定理之间有怎样的本质联系等等。由于在形式公理系统中推理规则本质上是一种符号串的重写规则，系统内的推演也只是对给定符号串的一系列重写而已，从而决定一切都是符号、符号串及重写规则的形式，公理的识别、系统内的推演都可以依据公理及推理规则的形式机械地完成，不需要比认读和改写符号及符号串更多的本领和知识，甚至不需要逻辑。因此，这类研究通常被看作是形式系统的语构的研究。
  (2) 语义(semantic)的研究。虽然形式化公理系统并不针对某 一特定的问题范畴，但可以对它做出种种解释，赋予它一定的个体域，即研究对象的集合，赋予它一定的结构，即用个体域中的个体、个体上的运算、个体间的关系去解释系统中的抽象符号。这一过程称 作赋予形式系统一个语义结构，或简称语义。在给定语义结构中可 以讨论形式系统中项所对应的个体，公式所对应的真值（真或假）。对语义的规定以及对形式系统在给定语义下的讨论，便是所谓对形式系统的语义研究。
  (3) 语构与语义关系的研究。由于语义结构通常是抽象出形式系统的那个问题范畴（如抽象出数理逻辑形式系统的问题范畴是“人类思维”）的数学描述，因此一个好的形式系统中的定理，应当都是在所有相关语义中的真命题；反之，所有这些真命题所对应的形式表示，应当都是形式系统的定理。诸如此类的讨论，都可视为对形式系统语构与语义关系的研究。

元理论与元定理

  在数理逻辑形式系统的研究中，通常使用两种语言。一种是形式系统自身所使用的形式语言，这些形式语言是我们的研究对象，称之为对象语言。另一种是用于介绍和研讨该形式系统时使用的语言，为通常所用的数学语言，称之为元语言。元语言也使用大量符号，包括沿用形式系统的符号、表示形式系统中同一类符号的符号即语法变元以及为表达元语言概念引入的新符号。
  对数理逻辑的理论研究包括两方面：一方面是数理逻辑形式系统内的公理、推理规则及其由它们导出的定理所构成的逻辑学理论；另一方面是对这个形式系统进行研究所得的关于系统的性质定理所组成的理论，这个称为元理论(meta theory)，其中的系统性质定理称为元定理(meta theorems)。

元理论的研究与元定理的证明

  尽管我们知道，元理论完全可以在公理集合论内部被严格地形式化，而公理集合论本身也不过是一个特殊的形式系统，但如果我们打算从零开始构建一个数学体系，首要任务便是搭建所需的形式系统。此时我们会发现，不可避免地需要依赖一些先验的概念与推理方法，例如集合、映射、推理规则、自然数、整数、数学归纳法与递推法等。尽管理论上这些概念最终都可以在集合论中被形式化，但我们在建构系统的早期阶段必须先行接受并使用它们。
  由此可见，“从零开始”构建数学体系在绝对意义上是不可行的。我们总要依赖某些先验的语言、规则和表示能力，以启动形式系统的语法与语义框架。在本节关于数理逻辑和形式系统初步的内容中，我们将暂时借助公理集合论中的定义和定理，用以说明形式系统的构造与运行方式。一旦初步系统建立完毕，我们便可以在其内部开展进一步研究，并借助 Gödel 编码等技术研究该系统自身的结构与限制。此时，那些曾依赖先验知识的命题和推理过程，也才能被系统内部正式地复现。
  因此，在本部分的推理和论证中，我们将适度借助集合论中的已有结论，并使用自然语言对若干元定理进行说明。读者应理解：这些结论在系统搭建完成后是可被形式化重构的，我们也将在后续章节中体现这一点。需要说明的是，我们默认公理集合论（尤其是ZF系统）在处理诸如“字符串”等基本对象时，具有良好的表达能力和可靠性，在一定意义上可以视作“对现实世界真理的描述”。当然，这种立场本质上依赖于某种柏拉图主义与认识论的哲学预设，我们在此不深入展开，只暂且接受这些基础作为合理和可信的起点。

  人的伟大之处在于，他是桥梁而非目的；人的可爱之处在于，他是过渡与沉沦。

― Friedrich Wilhelm Nietzsche, 《查拉图斯特拉如是说》