2.5　意义从何而来

聊完了推理，我们现在来聊聊什么叫“形式化”。显然与“现代化”类似，其意思就是“通往形式的过程”。那问题来了：为什么要通往形式呢？有什么好处呢？这个过程又是怎样的呢？我们先来回答第二个问题。

概念2.23　对一个系统的形式化（formalization）是这样的一个过程，我们寻找一个形式系统，使其建模了该系统。

这里又出现了两个新的概念，形式系统与建模。目标系统因我们研究的问题而异可以任意，比如宇宙、爱情、法律、人体，而用于建模的形式系统就是一个很特殊的系统了。

概念2.24　形式系统（formal system）是一门形式语言，以及

· 若干称之为公理（axiom）的合式公式；

· 若干推理规则（inference rule），其规定了以零个或多个公式作为前提（premise），可以得到什么公式作为结论（conclusion）。

看起来很复杂？其实很简单啦。让我们来看一个例子。

例子2.25（一个简单的形式系统）　我们定义如下形式系统：

· 字母表：、⊕、；

· 语法：仅形如的公式合法，其中X,Y,Z要么为空，要么仅由组成；

· 公理：；

· 推理规则：

1．以为前提，可得到结论；

2．以为前提，可得到结论；

让我们在这个形式系统里遨游一番。首先，我们写一些公式呗，比如下面这些：

· ♣

·

·

·

·

这些公式都（符）合（语）法吗？不然。首先，第一个公式用到了不在字母表中的符号♣，所以非法。第二和第五个公式虽然符号没问题，但是不符合语法的要求。所以，只有第三和第四个公式是合式公式。

搞清楚了系统中的合式公式是什么，下面让我们按照规则来推理推理。从什么开始呢？从公理开始：

以它为前提，将规则1作用在公理（2.1）上，我们可以得到一个结论：

规则2作用在公理（2.1）上并没有产生新的结论，于是，此时我们总共得到了包括公理在内的两个结论。继续前进，我们以结论（2.2）为前提再使用一次规则1，得到

同时，对结论（2.2）可以用规则2了！这回得到了一个新的结论：

现在我们便有了四个结论。这个过程可以不停地持续下去，比如可以再对结论（2.3）使用规则1，得到

等等……我们会机械地“推理”出无穷无尽个结论。

怎么样，形式系统也不恐怖吧！顺便说一句，我们上面那样按照规则进行的机械演算，就是形式化了的证明。

概念2.26　我们称一条以公理或已得结论为前提经有限次使用推理规则得到的公式序列为一个证明（proof），其最后一个结论称为定理（theorem）。

不过，相信你证明了几条定理后，肯定也就不想继续了。可能是觉得无聊了，但我想更有可能是因为你一定发现了一个规律：

断言2.27　例子2.25定义的形式系统中的定理一定形如

其中X,Y,Z均由构成，且X与Y中的总数等于Z中的个数。另一方面，任何满足此性质的公式，一定是该系统中的一条定理。

不仅如此，如果你发现了上述规律，肯定会进一步恍然大悟：

洞察2.28　若将例子2.25定义的形式系统中的合式公式

中的X、Y与Z替换成它们包含的个数，⊕替换成+、替换成=，那么该系统中的定理便对应于自然数加法中的等式。另一方面，任何自然数加法中的等式必然对应于该系统中的一条定理。

换句话说，这个系统形式地（formally）刻画了加法！比如

· 即0+0=0

· 即1+0=1

· 即0+1=1

· 即1+1=2

我们的这个发现以及我们在洞察2.28所做的替换，为这么一个本毫无意义、纯形式的系统赋予了意义！

概念2.29　我们称对一个形式语言中的符号按一定规则进行替换的过程为赋予该语言一个解释（interpretation）。

注意，概念2.29是关于形式语言的，而对其上的形式系统，我们有

概念2.30　若一个形式系统中的定理经由解释后成为了另一个系统中的事实⁽¹⁴⁾，那么我们就说前者建模了后者，后者是前者的一个模型（model）。

于是我们说，例子2.25中的形式系统建模了自然数加法。这不得不说是一个了不起的成就。我们创造了一个无意义的世界，在对其进行解释赋予其含义后，竟完美吻合了我们天然进行加法的能力！说不定上帝设计人类心智的宏伟系统中真的就有那么一小部分用的就是我们上面写下的那个呢。