Science 版 (精华区)

发信人: zjliu (分析数学), 信区: Science
标  题: 证明的证明（四）
发信站: 哈工大紫丁香 (Fri Sep 27 14:22:01 2002) , 转信

  

形式化方法并不是“从公理通过逻辑方法来导出整个理论”这么简单，因为逻辑方法本
身也是有争议的。比如说直觉主义的逻辑不允许使用排中律（也就是说即使你能证明一
个命题的否命题不正确，你还是不能得出这个命题是正确的。这种逻辑有些怪诞，但是
直觉主义的数理逻辑哲学无论在历史上还是在现实中，尤其是在信息科学被发展和应用
的今天，都有极其重要的意义。对于直觉主义数理逻辑的评价并不是本文的主题，所以
在此我们不加讨论）。所以我们还得防止“一不小心”用了一种不被允许的推理方式，
被允许使用的推理方式也必须显明地写出来，也必须有明确的机制来验证在证明中只有
“合法”的公理和逻辑推理方法被使用。

　　在数理逻辑中有个分支叫“证明论”，专门以形式化的数学证明为研究对象，来解
决上面所说的问题。因为证明是数学研究的主要方式，所以证明论可以看做是对数学研
究的研究，所以它又被称做“元数学”(Metamathematics)，字面上可以理解为“审视数
学的学问”。所以在下面的讨论中，我们一定要区别两种“理论”，一种是证明论本身
这个数理逻辑的分支理论，另一种是被证明论研究的数学理论。这就好像一本用中文写
成的英语语法书一样，写这本书本身必须使用一种语言，在这里我们用的是中文，而这
书本身研究的却是另一种语言，在这里我们研究的是英语，它们是两种不同的语言。

　　从证明论的角度看来，象初等几何，或者自然数算术这样的数学理论是什么？

　　首先，里面有一些符号。这些符号可以表示数学理论中的对象，比如代表点的A，B
，C，代表自然数的m、n或者x、y，或者是表示常量的符号1、2、3等；它们也可以表示
数学对象间的关系，比如“＞”；也可以用来表示某些逻辑关系，比如大家熟悉的“”
（对于任意）、“”（存在）或“→”（蕴涵），还可以是纯粹的辅助符号，比如括号
。不过要注意的是这些符号具体代表的是什么意思，证明论并不关心，就象上面所说的
“点”和“桌子”。如果你愿意，你完全可以用“＞”来表示“小于”关系，或者用A来
表示左括号，用α来表示右括号。只是因为出于方便的缘故，在研究一个数学理论时，
我们仍旧使用那个理论平时使用的那些符号。

　　其次，我们可以用这些符号来组成表达式，也就是一串有限长度的符号。可是并不
是无论什么表达式在这个数学理论里都有意义。比方说自然数的算术理论中“1+1=2”或
者“2+2=22”或者“(a+b)*c-d=0”都是有意义的表达式（尽管有可能是错的或者意义并
没有完全被确定），但是象“((0++a”这类字符串却毫无意义。所以我们必须知道由什
么样的方式组成的表达式是有意义的，也就是说，理论必须提供这些有意义的表达式（
我们把它们称为公式）的形成规则。

　　最后，也是最关键的，我们必须知道在这个数学理论里公式的变形规则。在这里我
们先要看看在证明论中如何定义“证明”这个概念，怎么样的一段文字才配得上被称作
是一个“证明”？一个数学证明看起来象是什么？就是一串有限个公式组成的公式串，
我们先写下第一个公式，再写下第二个，……。当然不是无论什么样的一堆公式堆在那
里就算是一个证明了。假设这个公式串看起来是这个模样：F1, F2, F3,……,Fn，其中
每一个Fi都是一个公式，那么这里每个公式都必须满足：

1)或者它是公理（也就是一开始就规定的不需要证明就可以使用的公式）；

2)或者它可以从在它前面的那些公式推出，不过这里的“推出”不是我们平时所说的运
用逻辑来得到，因为逻辑规则本身也必须由变形规则来刻划。所以我们宁可说，“它可
以通过从在它前面的那些公式，使用允许的变形规则得来的”；

比方说，在命题逻辑中，如果我们已经证明了命题A蕴涵命题B（“如果A，则B”，用形
式的记号写作A→B），我们也知道命题A是成立的，那么我们可以得出命题B是成立的。
这里的变形规则就是：如果在前面的公式串里我们可以找到两个公式“A→B”和“A”，
那么我们就可以在这个公式串中接下去写上“B”。这里我们清楚地看见我们如何用变形
规则来刻划逻辑规则。另外，事实上公理可以看做是特别的变形规则，就是在任何时候
都可以写下的公式，而不需要考虑它的前面有没有某些特定的公式。在这个时候，我们
就称上面这个公式串是最后那个公式Fn在这个数学理论中的一个证明，Fn就成了这个数
学理论中的一个“定理”。很明显，任何一个公理都是一个定理，只由它本身组成的公
式串就是它的（显而易见的）证明；任何一个证明中的任何一个公式也一定是定理，因
为只要把这个证明截断在这个公式出现的那个位置，就得到了它的证明。

　　如果一个数学理论被这样规定了符号，公式的形成规则，和公式的变形规则（以及
公理）后，我们就说它被形式化了，成为一个形式系统。比如说原先朴素的欧几里得几
何就被希尔伯特形式化了，而朴素的自然数算术理论则被皮亚诺公理体系形式化了。


1)或者它是公理（也就是一开始就规定的不需要证明就可以使用的公式）；

2)或者它可以从在它前面的那些公式推出，不过这里的“推出”不是我们平时所说的运
用逻辑来得到，因为逻辑规则本身也必须由变形规则来刻划。所以我们宁可说，“它可
以通过从在它前面的那些公式，使用允许的变形规则得来的”；

比方说，在命题逻辑中，如果我们已经证明了命题A蕴涵命题B（“如果A，则B”，用形
式的记号写作A→B），我们也知道命题A是成立的，那么我们可以得出命题B是成立的。
这里的变形规则就是：如果在前面的公式串里我们可以找到两个公式“A→B”和“A”，
那么我们就可以在这个公式串中接下去写上“B”。这里我们清楚地看见我们如何用变形
规则来刻划逻辑规则。另外，事实上公理可以看做是特别的变形规则，就是在任何时候
都可以写下的公式，而不需要考虑它的前面有没有某些特定的公式。在这个时候，我们
就称上面这个公式串是最后那个公式Fn在这个数学理论中的一个证明，Fn就成了这个数
学理论中的一个“定理”。很明显，任何一个公理都是一个定理，只由它本身组成的公
式串就是它的（显而易见的）证明；任何一个证明中的任何一个公式也一定是定理，因
为只要把这个证明截断在这个公式出现的那个位置，就得到了它的证明。

　　如果一个数学理论被这样规定了符号，公式的形成规则，和公式的变形规则（以及
公理）后，我们就说它被形式化了，成为一个形式系统。比如说原先朴素的欧几里得几
何就被希尔伯特形式化了，而朴素的自然数算术理论则被皮亚诺公理体系形式化了。
来源:·交大兵马俑BBS站 bbs.xjtu.edu.cn·[FROM:山城梁山]




--

※ 来源:．哈工大紫丁香 http://bbs.hit.edu.cn [FROM: 202.118.229.86]