03 形式化证明

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

相继式演算

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

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

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

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

1. \begin{array}{aligned} \\ \hline & \Gamma & \varphi &\\ \end{array} \text{ if } \varphi \in \Gamma \text{ (Assumption Rule)}，这个规则允许我们把某个前件作为后件。这可以作为的起点。正确性：当$\varphi\in \Gamma$时，对任意$\I$，只要$\I(\Gamma)=true$，那么$\I(\varphi)=true$，所以$\Gamma\models \varphi$成立；
2. \begin{array}{aligned} \\ \hline & t\equiv t &\\ \end{array}\text{ (Reflexivity)}，等式的自反性恒成立。这也可以作为形式化证明的起点。正确性：对于任意$\I$，$\I(t)=\I(t)$；
3. \begin{array}{aligned} & \Gamma & \varphi\\ \hline & \Gamma' & \varphi &\\ \end{array}$\text{ if } $\Gamma \subseteq \Gamma'$ $\text{ (Antecedent Rule)}$，这个规则会允许我们可以添加任意多个新的前件或改变已有的各个前件的顺序。正确性：对于任意$\mathfrak{I}$，如果$\mathfrak{I}(\Gamma')=true$，要证$\mathfrak{I}(\varphi)=true$。因为$\Gamma \subseteq \Gamma'$，所以$\mathfrak{I}(\Gamma)=true$。而已知$\Gamma\models \varphi$，所以$\mathfrak{I}(\Gamma)=true$意味着$\mathfrak{I}(\varphi)=true$。综上，对任意$\mathfrak{I}$只要$\mathfrak{I}(\Gamma')=true$就有$\mathfrak{I}(\varphi)=true$，所以$\Gamma'\models \varphi$；
4. \begin{array}{aligned} & \Gamma & \psi&\varphi\\ & \Gamma & \neg\psi&\varphi\\ \hline & \Gamma & &\varphi &\\ \end{array} \text{ (Proof by Case)}，这个规则允许我们做分类讨论。正确性：对于任意$\mathfrak{I}$，如果$\mathfrak{I}(\Gamma)=true$，此时从数学事实上$\mathfrak{I}(\psi)=true$和$\mathfrak{I}(\neg\psi)=true$只能恰好有一个成立。假如是前者成立，那么$\mathfrak{I}(\Gamma\cup\{\psi\})=true$，那么由第一行的sequent得到$\mathfrak{I}(\varphi)=true$；如果是后者成立，那么由第二行的sequent得到$\mathfrak{I}(\varphi)=true$。综上，对于任意$\mathfrak{I}$，只要$\mathfrak{I}(\Gamma)=true$就有$\mathfrak{I}(\varphi)=true$。所以$\Gamma\models \varphi$；
5. \begin{array}{aligned} & \Gamma & \neg\varphi&\psi\\ & \Gamma & \neg\varphi&\neg\psi\\ \hline & \Gamma & &\varphi &\\ \end{array} \text{ (Contradiction Rule)}，这个规则允许我们做反证法。正确性：对于任意$\mathfrak{I}$，如果$\mathfrak{I}(\Gamma)=true$，假如此时$\mathfrak{I}(\neg\varphi)=true$，那么由第一行的sequent可以得到$\mathfrak{I}(\psi) =true$，由第二行的sequent可以得到$\mathfrak{I}(\neg\psi)=true$。但这在数学事实上是矛盾的。所以只能是$\mathfrak{I}(\varphi)=true$。所以$\Gamma\models \varphi$；
6. \begin{array}{aligned} & \Gamma & \varphi&\chi\\ & \Gamma & \psi&\chi\\ \hline & \Gamma &(\varphi\lor \psi) &\chi &\\ \end{array} \text{ (Or Rule for Antecedent)}，这个规则允许我们用或连接词合并两个sequent。正确性：对于任意$\mathfrak{I}$，如果$\mathfrak{I}(\Gamma)=true$且$\mathfrak{I}(\varphi\lor \psi)=true$，$\mathfrak{I}(\varphi)=true$与$\mathfrak{I}(\psi)=true$中至少有一个成立，那么由第一行或第二行的sequent就可以推出$\mathfrak{I}(\chi)=true$成立；
7. \begin{array}{aligned} & \Gamma & \varphi\\ \hline & \Gamma & (\varphi\lor\psi) &\\ \end{array}, \ \ \begin{array}{aligned} & \Gamma & \varphi\\ \hline & \Gamma & (\psi\lor\varphi) &\\ \end{array} \text{ (Or Rule for Succeedent)}，这个规则会允许我们在后件中用或并上一个别的命题。正确性：对于任意$\mathfrak{I}$，如果$\mathfrak{I}(\Gamma)=true$，由第一行的sequent得到$\mathfrak{I}(\varphi)=true$，那么“$\mathfrak{I}(\varphi)=true$或$\mathfrak{I}(\psi)=true$”一定成立，所以$\mathfrak{I}(\varphi\lor\psi)=true$；
8. \begin{array}{aligned} & \Gamma & \varphi\dfrac{t}{x}\\ \hline & \Gamma &\exists x\varphi &\\ \end{array}