前言

追问一个公理系统的一致性，我们知道一个模型法，即从现实经验中找到一个模型，能将所有公理映射成此模型的真陈述，但很多系统模型是无穷的，比如想检验“空间中两点能确定一条直线”这个欧氏几何公理在空间模型中的陈述，需要检验所有无穷多的点，这显然不可能做到，这是模型法的固有缺陷。数学家也在尝试建立公理一致性的其他方法。

希尔伯特的方法：一致性的绝对证明

模型法可以视为一种相对证明方法，它将公理体系进行映射到别的体系中。希尔伯特尝试建造的证明方法不依赖任何其他系统的一致性。

完全形式化的系统

上章已经提到过“形式化”这个词，它表示抽离意义，只考虑逻辑上的模式的演绎系统。完全形式化(complete formalization) 是更进一步的操作，它意味着将系统内表达式的所有意义都抽离掉，将系统中的陈述作为空洞的“指号”，可以理解为字符串。这些指号的组合由一套精确陈述的规则说明。

这样的系统中公理和定理是什么样的呢？它们是没有任何意义的“串”，或称为有穷长符号序列。这样的系统中公理是一组串，定理也是一组串，推导只是根据规则将一组串转换为另一组串而已。

必须做出说明的是，这样的完全形式化系统中，“串”本身可以看起来有意义，它们所用的符号也可能强烈暗示它有意义，比如$1+1=2$就是一个串，但就形式系统而言，它并不关注串的意义，它们只是按照规则允许组合而已。

两个层次的陈述

建立一个完全形式化的系统，一个相当重要的目的是让我们区分两种不同层次的陈述，形式系统的和元数学的（meta-mathematics）。以书上的例子说明：

2+3=5	这是一个算术形式系统中的指号串
"2+3=5"是一个算术公式	这不属于算术形式系统中的串，它属于元数学
如果指号"="用于算数公式中，这个指号两边应是数字表达式	属于元数学
用数字"0"代替变元"x"，那么可以从公式"x=x"推出"0=0"	属于元数学
形式系统X是一致的	属于元数学

由此可见，元数学是用于描述形式系统中的串的，严格来说元数学的陈述中，不包含形式系统中的任何指号，上表中，用引号引起来的"2+3=5"，并不是串本身，而是代表这个串的名称。

如果说形式系统是我们研究对象本身，那么元数学就是对这个研究对象的讨论，它处于一个更超脱的视角。一个更明晰的例子是这样的，老鹰是由雄性孵蛋，这个陈述串属于动物学；但如果我们说：“老鹰是由雄性孵蛋”这个断言是扯淡，那么我们讨论的对象不是老鹰，而是动物学中的串，这就属于“元动物学”了。

希尔伯特的尝试

希尔伯特看到了形式系统和元数学的区分，他试图建立一致性的绝对证明，他的设想是：发展一种方法，对于一个完全形式化的演算中表达式有穷多结构特征进行分析，证明一致性。如何分析证明呢？记录形式化盐酸中出现的各种指号，说明如何将它们组合成公式，描述公式如何从其他公式得到，最终目的是检验形式上互相矛盾的公式不能从所给公理中得到。

这个方法有一定的要求，公式不能有无穷多的结构属性，也不能涉及对公示的无穷次运算，总结下来就是要给出一套有限的元数学步骤。

一个形象的例子

上述描述依旧比较晦涩，书中给出了一个形象的国际象棋例子。现在让我们想象国际象棋只有棋盘，棋子，忘掉国际象棋的所有规则。那么我们可以把棋子与棋盘视为基本指号；棋子在棋盘上合法排列视为公式或叫做串（良构串）；棋子初始排列对应系统的公理；游戏规则就是元数学陈述（此时应当叫做“元象棋”）。我们可以给出元象棋的定理，比如白方只有两个马和王，黑方只有王时，白方不可能将死黑方。总而言之，可以通过有限的元象棋步骤，检验所有初始布局的每一种情况。希尔伯特的目的就是通过这种有穷的方法证明一个给定的形式演算中不可能出现形式上矛盾的串。