03 形式化证明

通过一阶逻辑，我们能够形式化许多“数学命题”。接下来我们要讨论如何形式化“数学证明”。“数学证明”是从一些“前提”出发，根据“推导规则”得出“结论”的过程。其中，“前提”有两种，一种是公认的数学事实（公理），一种是在当前证明中假设已经成立的数学命题。事实上，我们可以不用考虑后一种“前提”，例如当我们要基于公理和前提证明结论时，我们可以等价地认为我是在基于公理证明结论，只要我们能给出一套恰当的“推导规则”使得这二者是等价的。“推导规则”是一套由已知成立命题给出一个新的成立的命题的演算法则。即便我们都采用一阶逻辑作为描述数学命题的语言，基于此也可以提出多种“推导规则集合”。每一套“推导规则集合”就构成了一套“一阶逻辑证明系统”。最常用的一阶逻辑证明系统有：希尔伯特系统(Hilbert system)，自然演绎法(Natural Deduction)，相继式演算(Sequent Calculus)。其中，希尔伯特系统是最简单的证明系统，它只引入了极少量的推导规则，这虽然降低了分析的难度，但使得证明的形式化非常冗长；自然演绎法是更接近数学实践的证明系统，但是却增加了分析的难度；相继式演算在自然演绎法的基础上发展而来，重构了部分规则，从而降低了分析的难度。本文把相继式演算作为证明系统，研究一阶逻辑作为命题语言下的形式化证明。

相继式演算

相继式演算基于以下对于“数学证明”的观察：一个数学证明可以看作有限个步骤。每个步骤是由一个“已知的命题集合”根据“证明规则”导出一个“新的已知命题”的过程。在通过一个证明步骤得到了一个新命题以后，这个新命题可以作为新的已知的命题，在下一个步骤中当作已知命题使用。如果需要，我们也可以剔除一些不需要的已知命题。有时，我们会用到反证法：把一个命题的否定暂时加入已知命题集合，然后同时推出某个命题以及它的否定，那么可以认为能推出。

我们总结发现，每个证明步骤都是由若干个称为前件(antecedent)的命题得到一个后件(succedent)，这个过程可以写作一个formula的序列(sequent) ，其中都是前件，是后件。假如恰好就是公理集合中的所有公理，是要证的命题，那么序列就是证明的目标：一个证明就是从某个已知成立的序列（例如）出发做“序列的变换”得到。这个序列的变换过程就是一个用相继式演算的方式表示的形式化证明。

我们像算数中的“列竖式”一样用横线来表示一条演算规则。用表示有限的一列formula ，表示序列可以变换为。对于每一条演算规则，我们都可以用语义后承关系验证其正确性(soundness)：如果成立总是意味着成立，就说明这条演算规则是正确、可靠的（“总是意味着”的意思是，如果在数学事实上成立，也即对于任何解释都有“在数学事实上成立意味着在数学事实上成立，那么一定也在数学事实上成立”。再次强调，数学事实是不依赖于任何文字描述的客观实体）。

下面我们逐一定义相继式演算中可以使用的演算规则，共十条，并验证每条规则的正确性：（由功能完全性，我们依然只需考虑这三个逻辑符号）

1. ，这个规则允许我们把某个前件作为后件。这可以作为的起点。正确性：当时，对任意，只要，那么，所以成立；
2. ，等式的自反性恒成立。这也可以作为形式化证明的起点。正确性：对于任意，；
3. ，这个规则会允许我们可以添加任意多个新的前件或改变已有的各个前件的顺序。正确性：对于任意，如果，要证。因为，所以。而已知，所以意味着。综上，对任意只要就有，所以；
4. ，这个规则允许我们做分类讨论。正确性：对于任意，如果，此时从数学事实上和只能恰好有一个成立。假如是前者成立，那么，那么由第一行的sequent得到；如果是后者成立，那么由第二行的sequent得到。综上，对于任意，只要就有。所以；
5. ，这个规则允许我们做反证法。正确性：对于任意，如果，假如此时，那么由第一行的sequent可以得到，由第二行的sequent可以得到。但这在数学事实上是矛盾的。所以只能是。所以；
6. ，这个规则允许我们用或连接词合并两个sequent。正确性：对于任意，如果且，与中至少有一个成立，那么由第一行或第二行的sequent就可以推出成立；
7. ，这个规则会允许我们在后件中用或并上一个别的命题。正确性：对于任意，如果，由第一行的sequent得到，那么“或”一定成立，所以；
8. ，这个规则允许：当我们要证存在使得成立时，只需举出一个的一个实例。这里的称为成立的witness(见证)。这里的就是我们在上一节中定义的substitution。自然地，对这一规则的正确性验证会用到“语法替换”与“语义替换”的等价性：对于任意，如果，由得到，由The Substitution Lemma这等价于，也即论域中存在一个元素，使得且，这恰好满足语义的定义：；
9. ，这个规则允许我们在前件中做推断“”“”。正确性：对于任意，如果且，意味着论域中存在元素使得。由于，那么，因此与在所有的自由变量上有相同的解释，由The Coincidence Lemma可得。而，于是$\left(\mathfrak{I}\dfrac{a}{y}\right)\dfrac{a}{x}(\varphi)=$\left(\mathfrak{I}\dfrac{a}{y}\right)\dfrac{\mathfrak{I}\dfrac{a}{y}(y)}{x}(\varphi)$=\mathfrak{I}\dfrac{a}{y}(\varphi \dfrac{y}{x})y \notin \text{free}(\Gamma)\mathfrak{I}\dfrac{a}{y}(\Gamma)= \mathfrak{I}(\Gamma)=true\mathfrak{I}\dfrac{a}{y}(\psi)=truey \notin \text{free}(\psi)\mathfrak{I}\dfrac{a}{y}(\psi)= \mathfrak{I}( \psi)=true\Gamma \cup \{\exists x \varphi\} \models \psiy(x\equiv f y)\dfrac{y}{x}y\equiv fyy\exists x \ x\equiv fyy\equiv fy$，而这不是语义后承关系，因此不正确）
10. ，这个规则允许我们根据前件中的等式做替换。正确性：对于任意，如果且，由第一行的sequent得，根据The Substitution Lemma得到，而，所以，再次根据The Substitution Lemma有；

接下来，我们可以根据以上十条规则，进一步给出一系列由以上十条规则的组合使用得到的推导规则。我们在此列出一些重要的：

• ，排中律；
• ，链式法则；
• ，肯定前件式；
• ，或规则的变形；
• ，矛盾规则的变形：如果一个前件能推出矛盾的后件，则这个前件可以推出任意命题；

我们以Modified Contradiction Rule为例，展示上述规则是如何导出的（注意，此时我们不再依据数学事实做证明，而是基于已有规则做形式上的推导）：对第一行的sequent应用规则三antecedent rule，得到；对第二行的sequent应用规则三antecedent rule，得到；对这两个sequent应用规则五contradiction rule得到，证明结束。

形式化证明

当我们从一个永真式出发，依据演算规则不断对算式做变换，直到最后演算出我们想要证明的结论，我们就已经纯粹从形式上给出了一个证明。这就是一个形式化证明(formal proof)。而既然我们已经逐一验证了这十条演算规则的正确性，就说明形式化证明一定是正确的：如果横线以上的每一条sequent 都满足，那么横线下的sequent 就一定满足。要确认这一点，只需在数学事实层面做归纳证明：对演算的步骤归纳，初始步骤是符合数学事实的，每一条规则的应用也是符合数学事实的，而步骤是有限的，因此最终得出的结论也是符合数学事实的。这就是基于一阶逻辑语言的相继式演算的可靠性(Soundness)。

我们必须把语义后承和演算推导区分开来。具体而言，对于一个有限的一阶逻辑formula集合和一个一阶逻辑formula ，如果是的语义后承，我们就记为。的含义是：在任何解释下，数学事实上成立都意味着数学事实上成立。但是这没有涉及任何有关形式化证明的事情。所以，为了讨论命题能否由集合通过形式化证明得到，我们引入新的符号：如果可以由相继式演算得到sequence ，那么记为。

可靠性说的是：任何可以从出发由形式化证明得到的命题，都是数学事实上的语义后承。用新定义的符号来表达：选定符号集，对于任意有限的-formula集合和-formula ，如果成立，那么一定有成立。形式化证明永远不会引发错误，不会由正确的前提导出错误的结论。

Remark: 我们通常不必强调是一个有限的集合还是一个无限的集合。因为一个证明一定是有限长的，因此即便是一个包含无穷多个formula的集合，只要能找到一个形式化证明从推出了，那么我们一定能找到的一个有限子集使得。于是根据可靠性，能满足的也一定有一个有限子集使得。

此时，最自然的一个疑问是：是否对于任何与，只要成立，就有成立？也就是说，是不是任何数学事实上成立的语义后承关系都存在一个形式化的证明（可以写出一个有限长的相继式演算的算式）？这一性质就称为基于一阶逻辑语言的相继式演算的完备性(completeness)。我们将在下一节证明基于一阶逻辑语言的相继式演算是具有完备性的，这就是哥德尔完备性定理(Gödel’s Completeness Theorem)。