13、数学证明：形式化与逻辑完备性探索

数学证明：形式化与逻辑完备性探索

1. 数学证明的构建与挑战

在数学领域，证明是通过逐步推导句子来构建的。推导过程中，我们可以运用逻辑规则从已有的句子中得出新的句子，例如亚里士多德就使用过的“肯定前件式”规则（modus ponens），即若已知“ϕ”和“若 ϕ，则 ψ”，那么可以推导出“ψ”。

在构建证明时，每一步都有多种选择，要证明的句子只能提供一些线索，并没有通用的策略。数学家们在日常工作中常常会发现，找到一个给定句子的证明有时极其困难。

一旦我们列出语言中使用的所有符号、公理和规则，证明的概念就完全形式化了。证明实际上是一系列满足特定句法规则的符号。与英语句子的句法相比，描述证明的句法要简单得多，甚至无需考虑英语词汇的复杂性。所有逻辑学家都认为证明的概念可以完全形式化，但部分数学家怀疑数学家们实际产生的所有证明是否都能转化为这种形式证明。

真正的数学证明目的并非呈现一串可被机械检查的符号，而是传达证明背后的思路，并让读者相信该思路可以实现。例如，当证明需要考虑几个类似情况时，可能只给出其中一个情况的证明，其余留给读者自行完成，或者仅说明如何修改第一个情况的证明以适用于其他情况。而且，这类证明中的步骤并非像形式证明那样是基本步骤，更像是小跳跃，读者理解时需要付出或多或少的努力和创造力。仔细检查一篇十页的文章可能需要几天时间，有些甚至需要更长时间。那么，如果尝试将一个真正长的证明转化为形式证明，会遇到什么问题呢？

2. 所有数学证明能否形式化

有人认为，如果有必要，我们只需付出适度的努力就能将任何证明形式化。计算机的发展为此提供了足够清晰的例证，经验表明任何算法都可以形式化。在计算机出现之前，没人在意将算法正式写