一阶逻辑的完备性

PDF版本：一阶逻辑的完备性

每一套严格的数学理论(theory)都应当具有这样的形式：有若干条假定成立的公理，每一条定理都由公理推导而来。用来说明一个定理是怎样从公理推导而来的论证称为一个“证明(proof)”。然而，在各个数学领域中可以在证明中使用的演绎规则往往是没有严格规定的，换言之数学证明是基于自然语言的。因此，数学的形式化的下一个任务就是如何形式地定义“证明”的概念。

在定义了一阶逻辑的语法和语义之后，我们已经可以用一阶逻辑来表示许多数学的公理或定理了。并且我们强调，虽然还没有说明具体怎么做到，原则上一阶逻辑是可以表示所有数学定理的。对于每个特定的数学理论，我们会选定一个符号集$S$和一个interpretation$I$。公理是$S$-formula集合$\Phi$，满足$I\models \Phi$（$\Phi$中的formula往往都是sentence）。每个满足$I\models\varphi$的formula$\varphi$就称为该理论中的一个定理。在这里，为什么能由$I\models \Phi$推出$I\models \varphi$是在语义层面（自然语言）说明的。这种语义上的推导大多数情况是显而易见地自明的，并且我们期望这种推导是不依赖于具体解释$I$的而是$\Phi$和$\varphi$在语义上存在因果关系$\Phi\models \varphi$。为了把这种推导形式化，我们希望能抽象出一套字符串意义下的变换规则，作为一阶逻辑的证明规则，使得如果formula集合$\Phi$能通过这套规则演绎得到formula$\varphi$，当且仅当在非常谨慎的自然语言下$\Phi$与$\varphi$有因果关系$\Phi\models \varphi$。说明每条规则对应到语义上都是正确的是一个相对容易的工作，但反过来说明每个语义上正确的推导都能被我们选出的证明规则形式化就是一个比较困难的工作了。这称为一阶逻辑的完备性(completeness)问题，最早由哥德尔给出了证明，称为哥德尔完备性定理。有了完备性，今后我们便只需要在字符串语法上检查证明的正确性，而不必陷入自然语言的模糊性当中。进而，机器也可以做一些证明，因为机器有能力按照规则做形式串的变换，而人类有能力读出每个形式串在自然语言中的语义。

Sequent Calculus

我们观察到，一个数学证明可以看作有限个步骤，每个步骤是由一些已知的命题根据证明规则推出一个“新命题”。在通过一个证明步骤得到了一个新命题以后，这个新命题可以作为新的已知的命题，在下一个步骤中当作已知命题使用。如果需要，我们也可以剔除一些不需要的已知命题。有时，我们会用到反证法，把一个命题的否定当作已知命题，并同时推出一个命题以及它的否定已知，此时我们得到那个被我们否定后假定为已知的命题。于是我们总结发现，每个证明步骤都是由若干个称为前件(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$。这个序列的变换过程就是一个证明，我们把它称为一个序列演算(sequent calculus)下的证明。序列演算的规则就是我们想要形式化定义的证明规则。

我们像算数中的“列竖式”一样用横线来表示一条演算规则。用$\Gamma$表示有限的一列formula$\psi_1\psi_2\cdots \psi_k$，\begin{array}{aligned} & \Gamma & \varphi\\ \hline & \Gamma' & \psi &\\ \end{array}表示序列$\Gamma \ \varphi$可以变换为$\Gamma' \ \psi$。如果在自然语言下$\Gamma \models \varphi$总是能推出$\Gamma'\models \psi$，就说明这条证明规则是“正确”的（这里我们把sequence的序列转化为了sequence的集合）。下面我们逐一定义演算规则，共十条，并验证每条规则的正确性：（由语义的等价性，我们依然只需考虑$\neg,\lor,\exists$这三个逻辑符号）

1. \begin{array}{aligned} \\ \hline & \Gamma & \varphi &\\ \end{array} \text{ if } \varphi \in \Gamma \text{ (Assumption Rule)}，这个规则会允许我们把某个前件作为后件，这可以作为证明的起点。正确性：当$\varphi\in \Gamma$时$\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)}，这个规则会允许我们可以添加新的前件或改变已有的各个前件的顺序。正确性：假如$\Gamma\models \varphi$，$\Gamma \subseteq \Gamma'$，那么显然$\Gamma'\models \varphi$；
4. \begin{array}{aligned} & \Gamma & \psi&\varphi\\ & \Gamma & \neg\psi&\varphi\\ \hline & \Gamma & &\varphi &\\ \end{array} \text{ (Proof by Case)}，这个规则允许我们做分类讨论。正确性：对于任意$I$，假如有$I\models \Gamma$，那么$I\models \psi$和$I\models \neg\psi$只能有一个成立（在自然语言中一个数学命题不是真的就是假的）。假如是前者成立，那么$I\models \Gamma\psi$，由第一行的sequent得到$I\models \varphi$；如果是后者成立，那么由第二行的sequent得到$I\models \varphi$。综上，$I\models \varphi$。所以对任意$I$可以由$I\models \Gamma$推出$I\models \varphi$，所以$\Gamma\models \varphi$；
5. \begin{array}{aligned} & \Gamma & \neg\varphi&\psi\\ & \Gamma & \neg\varphi&\neg\psi\\ \hline & \Gamma & &\varphi &\\ \end{array} \text{ (Contradiction Rule)}，这个规则允许我们做反证法。正确性：对于任意满足$I\models \Gamma$的$I$，假如有$I\models\neg\varphi$，那么由第一行的sequent可以得到$I\models \psi$，由第二行的sequent可以得到$I\models \neg\psi$。但一个命题在语义上不可能既真又假，所以$I\models \neg\varphi$不成立，也即$I\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。正确性：对于任意满足$I\models \Gamma(\varphi\lor \psi)$的$I$，$J\models \Gamma\varphi$与$J\models \Gamma\psi$中至少有一个成立，那么由第一行或第二行的sequent就可以推出$I\models \chi$成立；
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)}，这个规则会允许我们在后件中用或并上一个别的命题。正确性：对于任意$I\models \Gamma$，由第一行的sequent得到$I\models \varphi$，那么“$I\models \varphi$或$I\models \psi$”为真，也即$I\models(\varphi\lor\psi)$；
8. \begin{array}{aligned} & \Gamma & \varphi\dfrac{t}{x}\\ \hline & \Gamma &\exists x\varphi &\\ \end{array} \text{ (Rule for }\exists\text{ in Succedent)}，这个规则允许：当我们要证存在$x$使得$\varphi$成立时，只需举出一个$x$的一个实例$t$，所以这里的$t$称为$\varphi$成立的witness(见证)。这里的$\varphi\dfrac{t}{x}$就是我们在语义一节中定义的substitution。自然地，对这一规则的正确性验证会用到“语法替换”与“语义替换”的等价性：对于任意满足$I\models \Gamma$的$I$，由$\Gamma\models \varphi\dfrac{t}{x}$得到$J\models \varphi\dfrac{t}{x}$，由The Substitution Lemma这等价于$I\dfrac{I(t)}{x}\models \varphi$，也即存在$a=I(t)$使得$I\dfrac{a}{x}\models \varphi$，由语义的定义$I\models \exists x\varphi$；
9. \begin{array}{aligned} & \Gamma & \varphi\dfrac{y}{x} & \psi\\ \hline & \Gamma &\exists x\varphi & \psi\\ \end{array} \text{ if }y\not\in \text{free}(\Gamma),\text{free}(\exists x\varphi),\text{free}(\psi)$\text{ (Rule for }\exists\text{ in Antecedent)}$，这个规则允许我们在前件中做推断“$\varphi\dfrac{y}{x}$”$\implies$“$\exists x\varphi$”。正确性：对于任意的满足$I\models \Gamma \ \exists x\varphi$的$I$，$\mathfrak{I} \models \exists x \varphi$意味着$a \in A$使得$\mathfrak{I}\dfrac{a}{x} \models \varphi$。由于$y \notin \text{free}(\exists x \varphi)$，$y \notin \text{free}(\varphi)$，因此$\left(\mathfrak{I}\dfrac{a}{y}\right)\dfrac{a}{x}$与$\mathfrak{I}\dfrac{a}{x}$在所有自由变量上有相同的解释，由The Coincidence Lemma可得$\mathfrak{I}\dfrac{a}{x} \models \varphi \iff \left(\mathfrak{I}\dfrac{a}{y}\right)\dfrac{a}{x} \models \varphi$。而$\mathfrak{I}\dfrac{a}{y}(y)=a$，于是$\left(\mathfrak{I}\dfrac{a}{y}\right)\dfrac{a}{x}\models \varphi \iff$$\left(\mathfrak{I}\dfrac{a}{y}\right)\dfrac{\mathfrak{I}\dfrac{a}{y}(y)}{x}\models \varphi\iff$$\mathfrak{I}\dfrac{a}{y}\models \varphi \dfrac{y}{x}$。由于$y \notin \text{free}(\Gamma)$，于是再次由The Coincidence Lemma得$\mathfrak{I}\dfrac{a}{y}\models \Gamma \iff \mathfrak{I} \models \Gamma$，因此$\mathfrak{I}\dfrac{a}{y} \models \Gamma$。所以由第一行的sequent得$\mathfrak{I}\dfrac{a}{y}\models \psi$。那么由于$y \notin \text{free}(\psi)$，再次根据The Coincidence Lemma得$\mathfrak{I}\dfrac{a}{y}\models \psi \iff \mathfrak{I} \models \psi$。综上$\mathfrak{I} \models \psi$；（特别应当注意的是，这条规则中对$y$的限制是必要的，不然会做出错误的证明。考虑以下反例：已知$(x\equiv f y)\dfrac{y}{x}$推出$y\equiv fy$，此时$y$是自由变量，不能应用本条规则。否则会得到$\exists x \ x\equiv fy$能推出$y\equiv fy$，显然不正确）
10. \begin{array}{aligned} & \Gamma && \varphi\dfrac{t}{x}\\ \hline & \Gamma \&t\equiv t' & \varphi\dfrac{t'}{x}\\ \end{array}$\text{ (Substitution Rule for Equality)}$，这个规则允许我们根据前件中的等式做替换。正确性：设$I\models \Gamma,I(t)=I(t')$，由第一行的sequent得$I\models \varphi\dfrac{t}{x}$，根据The Substitution Lemma得到$I\dfrac{I(t)}{x}\models \varphi$，而$I(t)=I(t')$，所以$I\dfrac{I(t')}{x}\models \varphi$，再次根据The Substitution Lemma有$I\models \varphi\dfrac{t'}{x}$；

以以上十条规则为基础，可以进一步总结出一些新的规则（这些规则本身都是这十条规则演算得到的），我们在此列出一些重要的：

• \text{Tertium non datur: }\begin{array}{aligned} \\ \hline & (\varphi \lor \neg\varphi)\\ \end{array}，排中律；
• \text{Chain Rule: }\begin{array}{aligned} & \Gamma & &\varphi\\ & \Gamma & \varphi & \psi\\ \hline & \Gamma & &\varphi\\ \end{array}，链式法则；
• \text{Modus ponens: }\begin{array}{aligned} & \Gamma & (\varphi\to\psi)\\ & \Gamma & \varphi\\ \hline & \Gamma &\psi\\ \end{array}，肯定前件；
• \text{Moified Or Rule: }\begin{array}{aligned} & \Gamma & (\varphi\lor\psi)\\ & \Gamma & \neg\varphi\\ \hline & \Gamma &\psi\\ \end{array}，肯定前件；
• \text{Modified Contradiction Rule: }\begin{array}{aligned} & \Gamma & \psi\\ & \Gamma & \neg\psi\\ \hline & \Gamma &\varphi &\\ \end{array}，如果一个前件能推出矛盾的后件，则这个前件可以推出任意命题；

我们以Modified Contradiction Rule为例，展示如何用Sequent演算做证明：对第一行的sequent应用规则三得到$\Gamma \ \ \neg \varphi \ \ \psi$，对第二行的sequent应用规则三得到$\Gamma \ \ \neg \varphi \ \ \neg\psi$，对这两个sequent应用规则五得到$\Gamma \ \ \varphi$，证明结束。

一个Sequent calculus是关于一个特定的符号集$S$定义的。例如，当符号集不同时能作为证明起点的$t\equiv t$的formula并不相同。所以在会引起歧义的场合，应当指出这是关于哪个符号集定义的sequent calculus。通常我们把一个sequent calculus记为$\mathfrak{S}$，关于符号集$S$的sequent calculus记为$\mathfrak{S}_S$。

Correctness

我们逐一验证了这十条演算规则的正确性：如果横线以上的每一条sequent$\Gamma_i \ \varphi_i$都满足$\Gamma_i\models \varphi_i$，那么横线下的sequent$\Gamma \ \varphi$满足$\Gamma\models \varphi$。所以，如果一个sequent calculus最终演算出了一条sequent$\Gamma_n \ \varphi_n$，就有$\Gamma_n\models \varphi_n$（只需在语义层面做归纳证明即可）。而如果每一条规则都是正确的，那么连在一起就能得到整个证明都是正确的（对演算的步骤归纳即可）。所以，如果对于一个有限的formula集合$\Phi$，可以由Sequent Calculus演算得到$\Phi \ \varphi$，那么一定成立$\Phi \models \varphi$。这称为一阶逻辑中的证明(Sequent Calculus)的“正确性(correctness)”。

我们把“可以由Sequent Calculus演算得到$\Phi \ \varphi$”用符号定义为$\Phi \vdash \varphi$（关于特定符号集$S$，记为$\Phi \vdash_S \varphi$）。它的否定记为$\Phi\not\vdash \varphi$，表示不能演算得到$\varphi$，或“$\varphi$不可证”。

那么一阶逻辑的正确性就可以表述为：对于任意有限的$S$-formula集合$\Phi$和$S$-formula$\varphi$，$\Phi\vdash_S \varphi \implies \Phi \models \varphi$。也就是说，每一条由Sequent Calculus生成的formula都是完全在语义上可信任的，我们对证明的形式化的定义永远不会引发错误，不会产生错误的定理。

我们注意到，因为一个证明一定是有限长的，因此即便$\Phi$是一个包含无穷多个formula的集合，我们一定能找到$\Phi$的有限子集$\Phi_0$使得$\Phi_0\vdash \varphi$。同理，能满足$\Phi \models \varphi$的$\Phi$也一定有一个有限子集$\Phi_0'$使得$\Phi_0'\models \varphi$。所以我们通常不必强调$\Phi$是一个有限的集合还是一个无限的集合。

Completeness

于是，一个自然的疑问就是：是不是每个语义上正确的定理都可以根据这十条演算规则有一个形式化的证明呢？也即是否成立“对任意的$S$-formula集合$\Phi$和$S$-formula$\varphi$，$\Phi \models \varphi \implies \Phi \vdash_S \varphi$”？这称为一阶逻辑的完备性(completeness)问题。

对这个问题的回答是肯定的，最早由哥德尔给出了证明，称为哥德尔完备性定理。相比之下，完备性的证明要比正确性复杂得多。我们下面要展示的这个证明并不是哥德尔原始的证明，而是后人改良了的较为简洁的版本。

Consistency

尽管我们验证了一阶逻辑的证明规则是不会产生错误的，但如果前提中本身就“包含了矛盾”，就会推出矛盾的结论，进而根据Modified Contradiction Rule能够产生一切结论。例如，$\Phi=\{t\equiv t,\neg t\equiv t\}$就能够演算出一切$S$-formula。我们可以定义一种对$\Phi$的描述，要求$\Phi$中不包含矛盾，我们称之为一致性(consistency)：如果一个formula集合$\Phi$对于任意的$\varphi$都不会有$\Phi \vdash \varphi$和$\Phi \vdash \neg\varphi$同时成立，就称它是一致的(consistent)，记为$\text{Con }\Phi$。

如果$\Phi$不是一致的，就称$\Phi$是不一致的(inconsistent)，记为$\text{Inc }\Phi$。根据定义，$\text{Inc }\Phi$等价于存在一个$\varphi$使得$\Phi \vdash \varphi$和$\Phi \vdash \neg \varphi$同时成立。根据Modified Contradiction Rule，这说明对于任意的$\psi$都有$\Phi \vdash \psi$成立（这里其实我们是取了$\Phi$中的一个有限子集并将其变为了一个sequent，在后文的表述中我们也会做这样的简化）。如果对于任意的$\psi$都有$\Phi \vdash \psi$成立，那么存在一个$\varphi$使得$\Phi \vdash \varphi$和$\Phi \vdash \neg \varphi$同时成立。因此$\text{Inc }\Phi$等价于对于任意的$\psi$都有$\Phi \vdash \psi$成立。因此$\text{Con }\Phi$等价于存在一个$\psi$使得$\Phi \vdash \psi$不成立。也就是说，一个一致的公式集一定有一个“证不出来”的命题。

注意，我们现在还不能证明“$\Phi \not\vdash \psi$”等价于“$\Phi \vdash \neg\varphi$”。我们只知道“$\Phi\not\models \psi$”等价于“$\Phi\models \neg\varphi$”。而根据Correctness又有$\Phi \not\vdash \psi \implies \Phi\not\models\psi$，所以要证“$\Phi \not\vdash \psi$”等价于“$\Phi \vdash \neg\varphi$”就是要证$\Phi \vdash \neg\varphi \implies \Phi\models \neg\varphi$，这就需要用到完备性的结论。

一个可满足的(satisfiable)公式集是一致的。这是因为“可满足”意味着语义上没有矛盾。证明：假设存在$I$使得$I\models \Phi$是可满足的，如果$\Phi$不一致，那么又有$\Phi \vdash \varphi$又有$\Phi \vdash \neg \varphi$。根据Correctness，又有$\Phi \models \varphi$又有$\Phi \models \neg \varphi$。所以又有$I\models \varphi$又有$I\not\models \varphi$，矛盾。因此$\Phi$一定是一致的。

$\Phi \vdash \varphi$等价于$\text{Inc } (\Phi \cup \{\neg \varphi\})$。证明：左推右，由规则一$\Phi\cup\{\neg\varphi\}\vdash \neg\varphi$，而$\Phi\vdash \varphi$所以由规则三$\Phi\cup \{\neg\varphi\}\vdash \varphi$，因此$\Phi \cup \{\neg\varphi\}$不一致；右推左，不一致说明能推出所有命题，所以$\Phi\cup \{\neg\varphi\}\vdash \varphi$，由规则一$\Phi\cup\{\varphi\}\vdash \varphi$，那么根据规则四$\Phi \vdash \varphi$。

最后，我们证明“对于任意的$\Phi,\varphi$，$\Phi \models \varphi \implies\Phi \vdash \varphi$”等价于“对于任意的$\Phi$，$\text{Con }\Phi \implies \text{Sat }\Phi$”。左边命题的逆否命题为“ 对于任意的$\Phi,\varphi$，$\Phi \not\vdash \varphi\implies \Phi \not\models \varphi$”，其中$\Phi \not\vdash \varphi$等价于“$\Phi\cup\{\neg\varphi\}$一致”，$\Phi \not\models \varphi$等价于“存在$J$使得$J\models\Phi$而$J \not\models \varphi$”，等价于“存在$I$使得$J \models \Phi \cup \{\neg\varphi\}$”，也即$\Phi \cup \{\neg\varphi\}$是可满足的。于是，左边命题等价于“对于任意的$\Phi,\varphi$，$\text{Con }(\Phi \cup \{\neg \varphi\}) \implies$$\text{Sat }(\Phi \cup \{\neg \varphi\})$”（A）。下面证明这等价于“对于任意的$\Phi$，$\text{Con }\Phi \implies \text{Sat }\Phi$”（B）。（B）推（A），用$\Phi \cup \{\neg \varphi\}$代入$\Phi$即可；（A）推（B），如果$\Phi$一致，取某一$\psi \in \Phi$，可以证明$\Phi \cup \{\neg\neg \psi\}$一致（由sequent calculus可以证明$\psi$和$\neg\neg\psi$有“等价性”，具体步骤略），那么由（A）可得$\Phi \cup \{\neg\neg \psi\}$可满足，所以存在$J$使得$I \models \Phi$且$I \models \neg\neg \psi$，因此$\text{Sat }\Phi$；

这样我们就把完备性问题等价转化为了“一致性是否意味着可满足性”的问题了。

Henkin’s Theorem

因此为了证明完备性，我们容易想到采用构造性证明：为每个一致的公式集构造一个能满足它的interpretation。我们自然地期待，我们能找到一种统一的构造方式。

对于每个一致的公式集$\Phi$，只需要能找到一个I=(\A,\beta)使得$\Phi\vdash \varphi\implies I\models \varphi$。对于任意的term$t_1,t_2$，当$\varphi$形如$t_1\equiv t_2$时，我们要求$\Phi \vdash t_1\equiv t_2 \implies$$I(t_1)=I(t_2)$。于是自然地，我们可以基于“项的等价类”来定义universe：如果$\Phi \vdash t_1\equiv t_2$，就称$t_1,t_2$等价，记为$t_1\sim t_2$（之所以可以称为等价，是因为我们可以通过sequent calculus证明自反、传递、对称性），把$t$所在的等价类记为$\bar{t}=\{t'\in T^S\mid t\sim t'\}$，所有等价类的集合记为$T^\Phi=\{\bar t\mid t \in T^S\}$。我们就把这个集合作为$I$的universe，上标$\Phi$表示这一等价类模型是基于$\Phi$中能证出的结论而构造的。对符号集的解释也容易定义：定义$R^{T^\Phi}\bar t_1\cdots \bar t_n$成立当且仅当$\Phi \vdash Rt_1\cdots t_n$；定义$f^{T^\Phi}(\bar t_1,\cdots, \bar t_n)=$$\overline{ft_1\cdots t_n}$；定义$c^{T^\Phi}=\bar c$。这样我们就定义好了一个structure，称为term structure，记为$\mathfrak{T}^\Phi$。定义对变量的解释$\beta^{\Phi}(x)=\bar x$，我们得到了一个interpretation$I^\Phi =(\mathfrak{T}^\Phi,\beta^{\Phi})$，称为term interpretation。

下面证明，term interpretation确实满足对任意$t\in T^S$满足$I^\Phi(t)=\bar t$。只需对$t$结构归纳：原子性的情况，$I^{\Phi}(x)=\bar x$与$I^\Phi(c)=\bar c$根据定义已经成立；$I^\Phi(ft_1\cdots t_n)$$=f^{T^\Phi}(I^\Phi(t_1),\cdots,I^\Phi(t_n))$$=f^{T^\Phi}(\bar t_1,\cdots, \bar t_n)$$=\overline{ft_1\cdots t_n}$。

接着我们试着用term interpretation对公式做解释。对于“原子性”的$\varphi \in L^S$，我们可以验证$\Phi \vdash \varphi \implies I^\Phi \models \varphi$确实成立。此时这个关系是当且仅当的，也就是我们可以验证进一步有$\Phi \vdash \varphi \iff It \models \varphi$：当$\varphi = t_1\equiv t_2$时，$\Phi \vdash t_1\equiv t_2$当且仅当$\bar t_1=\bar t_2$当且仅当$It(t_1)=It(t_2)$当且仅当$It \models t_1\equiv t_2$；当$\varphi = Rt_1\cdots t_n$时，$\Phi \vdash Rt_1\cdots t_n$当且仅当$R^\Phi(\bar t_1,\cdots,\bar t_n)$成立当且仅当$It\models Rt_1\cdots t_n$。

然而不幸的是，当我们想要基于原子性情况成立做结构归纳时，在遇到量词和连接词的时候出了问题：

考虑$S=\{R\}$，$\Phi=\{\exists xRx\}\cup \{\neg Ry\mid y\text{ is a variable}\}$。那么$\Phi \vdash \exists xRx$，我们想要推出$It \models \exists xRx$。假如$It \models \exists xRx$，那么存在$\bar t$使得$It\dfrac{\bar t}{x} \models Rx$，也即存在$t\in T^S$使得$It \dfrac{I(t)}{x}\models Rx$，由The Substitution Lemma等价于$It\models Rx\dfrac{t}{x}$，也即存在$t$使得$It \models Rt$。根据上一段的证明这当且仅当$\Phi\vdash Rt$。但是由于符号集里只有$R$，于是$t$只能是变量，也即存在变量$v$使得$\Phi \vdash Rv$。但是$\Phi \vdash \neg Rv$，这样$\Phi$就是不一致的了。但事实上，$\Phi$是一致的，只需构造一个解释$I_0$说明它是可满足的：universe是两个自然数$\{0,1\}$，$R(0)$成立$R(1)$不成立，把所有变量都解释为$1$。于是有$J_0\models \Phi$（存在$0$使得$R$成立，所有变量上$R$都不成立）。这就推出了矛盾，说明$It\not\models \exists xRx$。这里的问题出自term interpretation会根据$\Phi$推出的等式把term划分到不同的等价类，但实际的情况可能需要我们把不同等价类中的变量解释为同一个值才能满足。在我们的例子中，对所有term的解释并不是到值域的满射，这就使得$\exists xRx$这样的formula允许为引入$x$变量的解释之外的值，换言之这样的含存在量词的formula即便缺少witness（见证）也是能够成立的。

考虑$S=\{R\}$，$\Phi=\{Rx \lor Ry\}$。那么$\Phi \vdash Rx\lor Ry$，我们想要推出$It \models Rx\lor Ry$，也即$It \models Rx$或$It \models Ry$。假如$It \models Rx$成立，等价于$\Phi \vdash Rx$，由Correctness$\Phi \models Rx$。此时可以构造$I_1$令universe为自然数$\{0,1\}$，$R(0)$成立$R(1)$不成立，$\beta(x)=1,\beta(y)=0$，那么$I_1\models Rx\lor Ry$但是$I_1\not\models Rx$，这说明$\Phi \not\models Rx$，矛盾。同理，$It\models Ry$也不成立。说明$It \not \models Rx\lor Ry$。这里的问题出自“或”这一连接词，它导致我们不能推出由“或”连接的任意一个子formula究竟是真是假。例如上面我们已经证明了$\Phi \vdash Rx$不成立，还可以证明$\Phi \vdash \neg Rx$也不成立：如果$\Phi \vdash \neg Rx$，那么$\Phi \models \neg Rx$，可以构造一个$I_1'$令universe为自然数$\{0,1\}$，$R(0)$成立$R(1)$不成立，$\beta(x)=0,\beta(y)=1$，那么$I_1'\models \Phi$但$I_1'\not\models \neg Rx$，矛盾。换言之，对于$\Phi$存在一个命题$\varphi$使得$\Phi \vdash \varphi$与$\Phi \vdash \neg \varphi$都不成立，这就使得我们无法对“或”连接词做归纳了：因为即便两个子命题的正面和反面都不可证，这两个子命题的“或”却是可证的。

由此可见，如果我们想继续使用term interpretation做证明，就必须采取一些补救措施，也即给$\Phi$加上特殊的规定，使得以上两种情况不会出现。对于第一种情况，我们要求$\Phi$对所有存在量词包含见证(contain witness)，定义为：对于所有$L^S$中形如$\exists x\varphi$的formula，存在term$t$使得$\Phi \vdash (\exists x\varphi\to \varphi\dfrac{t}{x})$。对于第二种情况，我们要求$\Phi$总能证出每个命题的正面或者反面， 也即对于否定是完备的(negation complete)，定义为：对于所有的$\varphi \in L^S$，$\Phi \vdash \varphi$和$\Phi \vdash \neg\varphi$至少一者成立（由于我们总是对一致的公式集用term interpretation，所以其实是“恰好一者”成立）。

现在假设一致的公式集$\Phi$还同时满足contain witness与negation complete两个条件，我们可以继续对formula的结构归纳了。我们证明加强后的命题$It \models \varphi \iff \Phi \vdash \varphi$。

• 左推右，假设$It\models \neg\varphi$，也即$It\not\models \varphi$，根据归纳假设$\Phi \not\vdash \varphi$，于是由negation complete得到$\Phi \vdash \neg\varphi$必须成立；右推左，假设$\Phi \vdash \neg \varphi$，由于$\Phi$一致，所以$\Phi \not\vdash \varphi$，根据归纳假设$It\not\models \varphi$；
• 左推右：假设$It \models (\varphi \lor \psi)$，也即$It \models \varphi$或$It \models \psi$，由归纳假设这当且仅当$\Phi \vdash \varphi$或$\Phi \vdash \psi$。无论前者成立还是后者成立，都可以由规则七得$\Phi \vdash (\varphi \lor \psi)$。右推左：假设$\Phi \vdash (\varphi \lor \psi)$，假如$\Phi \vdash \varphi$成立，由归纳假设$It\models \varphi$成立；假如$\Phi \vdash \varphi$不成立，由negation complete得到$\Phi \vdash \neg\varphi$必须成立，由Moified Or Rule推出$\Phi \vdash \psi$，由归纳假设$It\models \psi$成立；
• 由The Substitution Lemma，$It \models \exists x\varphi$等价于存在$t\in T^S$使得$It \models \varphi\dfrac{t}{x}$，由归纳假设这等价于存在$t\in T^S$使得$\Phi \vdash \varphi\dfrac{t}{x}$。只需证这等价于$\Phi \vdash \exists x\varphi$。左推右：应用规则八即可；右推左，根据contain witness存在$t$使得$\Phi \vdash (\exists x\varphi \to \varphi\dfrac{t}{x})$，由Modus ponens可得$\Phi \vdash \varphi \dfrac{t}{x}$;

这样，我们就证明了对于contain witness以及negation complete的公式集$\Phi$，如果它是一致的，那么可以找到term interpretaion$It$使得$\Phi\vdash \varphi \iff It \models \varphi$。这称为Henkin’s Theorem。由此容易推出$It \models \Phi$，可见对于contain witness以及negation complete的公式集如果是一致的就是可满足的，也即在这样的特殊规定下完备性成立。

The Countable Case

所以我们发现，$\Phi$的term interpretation不足以作为那个能够满足$\Phi$的解释。事实上，我们也难以找到一个其它的自然的interpretation构造使得它能直接满足$\Phi$。然而事实上，term interpretation距离完备性已经很接近了。我们想让完备性对于一般的不满足contain witness和negation complete的公式集也成立，可以证明对于一般的一个一致的公式集$\Phi$，我们总可以做一些扩展——往$\Phi$里面“加入”若干条formula——从而在保持一致性的前提下使得它变得contain witness和negation complete。假设经过扩展以后的公式集是可满足的，那么$\Phi$作为它的子集自然也是可满足的了。

我们首先在限定符号集是可数集（或有限集）的情况下给出证明。

第一步，我们想对于一个一致的公式集$\Phi$，找到一个一致的公式集$\Psi$使得$\Phi \subseteq \Psi$同时$\Psi$contain witness。然而这是一个假命题，考虑以下反例：$\Phi = \{v_0\equiv t\mid t\in T^S\}\ \cup$$\{\exists v_0\exists v_1\neg v_0\equiv v_1\}$，$\Phi$是可满足的（只需把所有变量和函数值都解释为自然数$0$，并令universe为$\{0,1\}$）因此是一致的。然而，假如存在一致的$\Psi$包含$\Phi$且contain witness，那么对于任意$\varphi$和任意变量$x$都满足存在$t$使得$\Psi \vdash (\exists x\varphi \to \varphi \dfrac{t}{x})$，取$\varphi$为$\exists v_1\neg v_0\equiv v_1$，$x$为$v_0$就有$\Psi \vdash (\exists v_0\exists v_1\neg v_0\equiv v_1$$\to \exists v_1\neg v_0\equiv v_1 \dfrac{t}{v_0})$，于是$\Psi \vdash \exists v_1\neg t \equiv v_1$。再取$\varphi = \neg t \equiv v_1$，得到$\Psi \vdash \neg t \equiv t'$，但是由等式的传递性$\Psi \vdash t\equiv t'$，与$\Psi$一致矛盾。这里出现的问题是，实际上不存在能够充当$\{\exists v_0\exists v_1\neg v_0\equiv v_1\}$的witness的变量，因为每个witness变量本身都会被$v_0\equiv t$吸收，而不能真正指向那个在interpretation中未被用来赋值的值。

为此，我们再添加一条限制，规定$\Phi$中出现的所有自由变量不超过有限个（也即$\text{free}(\Phi):=$$\bigcup\limits_{\varphi \in \Phi}\text{free}(\varphi)$是有限集），这样就总能找到一个全新的变量来充当witness。下面证明，如果$\Phi$是一致的且$\text{free}(\Phi)$有限，那么存在$\Psi$包含$\Phi$且contain witness。因为一阶逻辑的alphabet有限且formula长度有限，并且符号集是可数的，因此$L^S$也是可数的，可以依次列出所有带有存在量词的formula$\exists x_0\varphi_0,\exists x_1\varphi_1,\cdots$。归纳地定义$\psi_n:=(\exists x_n\varphi_n\to\varphi_n\dfrac{y_n}{x_n})$，其中$y_n$是不属于$\text{free}(\exists x_0\varphi)\cup \text{free}(\Phi)\cup$\bigcup\limits_{m\<n}\text{free}(\psi_m)的下标最小的变量$y_n$（这是可以做到的因为自由变量的总个数是有限的），令\Phi_n=\Phi \cup \{\psi_m\mid m\<n\}，$\Psi=\bigcup\limits_{n\in \mathbb{N}}\Phi_n$，显然$\Psi$contain witness且包含$\Phi$，所以只需证明$\Psi$是一致的。首先证明每个$\Phi_n$都是一致的，对$n$归纳，$\Phi_0=\Phi$时显然成立；假设$\Phi_{n+1}=\Phi_n\cup \psi_{n}$不一致，那么对于任意$\varphi$都有$\Phi_{n}\cup (\neg\exists x_n\varphi_n\lor \varphi_n\dfrac{y_n}{x_n})\vdash \varphi$，根据sequent calculus得到$\Phi_n\cup \neg\exists x_n\varphi_n\vdash \varphi$与$\Phi_n\cup \varphi_n\dfrac{y_n}{x_n}\vdash \varphi$，而后者根据规则九得到$\Phi_n\cup \exists x_n\varphi_n \vdash \varphi$，于是根据规则四（分类讨论规则）得到$\Phi_n\vdash \varphi$对任意$\varphi$成立，与$\Phi_n$一致矛盾。最后证明$\Psi$是一致的，假如$\Psi$不一致，那么存在$\Psi$的一个有限子集$\Psi_0$使得存在$\varphi$使得$\Psi_0\vdash \varphi$且$\Psi_0\vdash \neg\varphi$，而$\Phi_0\subseteq \Phi_1\subseteq \cdots$，一定存在某个$\Phi_m$包含$\Psi_0$，这就推出$\Phi_m$不一致，矛盾。证毕。

第二步，我们想对于每个一致的公式集$\Psi$，找到一个一致的公式集$\Theta$使得$\Psi\subseteq \Theta$同时$\Theta$negation complete。这里的构造很简单，我们只需列出全部的$L^S$中的公式$\varphi_0,\varphi_1,\cdots$，依次试着把每个公式“合并”到$\Psi$上同时确保一致性成立。具体的，令$\Theta_0:=\Psi$，$\Theta_{n+1}:=\Theta_n\cup \varphi_n$如果$\Theta_{n}\cup\varphi_n$是一致的，否则$\Theta_{n+1}=\Theta_n$。令$\Theta:=\bigcup\limits_{n\in \mathbb{N}}\Theta_n$。显然$\Theta$包含$\Psi$并且是一致的（运用与第一步中相同的论证），只需证明它negation complete。对于任意$\varphi$，它对应着某个下标$\varphi_i$。如果$\Theta\vdash \neg\varphi_i$不成立，也即等价地$\Theta \cup \varphi_i$一致，那么其子集$\Theta_{i}\cup \varphi_i$也一致，说明$\Theta_{i+1}=\Theta_i\cup \varphi_i$，因此$\Theta \vdash \varphi_i$。这就说明$\Theta \vdash \neg\varphi_i$与$\Theta\vdash \varphi_i$中总是至少有一个是成立的，也即negation complete。

这样，对于我们在第一步中得到的contain witness的$\Psi$，应用第二步的结论我们可以找到一个包含它的negation complete的$\Theta$。$\Theta$既然包含一个contain witness的集合，当然也contain witness。这样我们就最终对于每个一致的且自由变量不超过有限个的$\Phi$，找到了一个一致的、contain witness的、negation complete的集合，由Henkin’s Theorem它可以被term interpretation满足，由此推出$\Phi$也可满足（这个满足$\Phi$的解释就是term interpretation“经过某些修正后的”版本）。

最后我们需要去掉“$\Phi$中出现的所有自由变量不超过有限个”的约束。我们发现，在“可满足性”的意义下一个自由变量和一个常量在语义上并没有区别，所以我们其实可以构造一个等价的公式集$\Phi'$，其中所有的自由变量都用常数符号替换，这样做了以后用作witness的变量就不会和普通变量发生冲突了。我们只需证明这种替换在可满足性的意义下是等价的，而这其实已经包含在The Coincidence Lemma所表达的含义当中了。

具体地，令$S':=S\cup \{c_0,c_1,\cdots\}$，对于每个$\varphi \in L^S$，做替换$\varphi':=\varphi\dfrac{c_0,\cdots,c_{n(\varphi)}}{v_0,\cdots,v_{n(\varphi)}}$，其中$n(\varphi)$是$\varphi$中下标最大的自由变量的下标。令$\Phi':=\{\varphi'\mid \varphi \in \Phi\}$，下面证明$\Phi'$在$S'$下是可满足的，只需证它的所有有限子集$\Phi'_0=\{\varphi_1',\cdots,\varphi_n'\}$都是可满足的（如果能满足每个有限子集，那么就满足全集。因为假如不满足全集，就一定不满足某个公式（所在的有限子集），矛盾）。记$\Phi_0=\{\varphi_1,\cdots,\varphi_n\}$，它是$\Phi$的一个子集因此是关于$S$一致的，而它是有限集因此只包含有限个自由变量，可以由已经证明的结论推出它是关于$S$可满足的。设$I\models_S \Phi_0$，那么可以把每个$c_i$赋值为$I(v_i)$而扩展得到一个$S'$下的interpretation$I'$。于是，根据The Substitution Lemma得到$I'\models \varphi\dfrac{c_0,\cdots c_{n(\varphi)}}{v_0,\cdots,v_{n(\varphi)}}$当且仅当$I'\dfrac{I'(c_0),\cdots I'(c_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}\models \varphi$当且仅当$I'\dfrac{I(v_0),\cdots I(v_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}\models \varphi$，由The Coincidence Lemma这当且仅当$I\dfrac{I(v_0),\cdots I(v_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}\models \varphi$，当且仅当$I\models \varphi$。所以$I'\models_{S'} \Phi_0'$。

由于$\Phi_0'$中实际上没有自由变量，所以根据The Coincidence Lemma我们可以任意修改$I'$中对变量的赋值而不影响其对$\Phi_0'$的满足性，于是可以令$I'(v_n)=I'(c_n)$，于是$I'\models \varphi'$当且仅当$I'\models \varphi\dfrac{c_0,\cdots c_{n(\varphi)}}{v_0,\cdots,v_{n(\varphi)}}$当且仅当$I'\dfrac{I'(c_0),\cdots I'(c_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}\models \varphi$当且仅当$I'\dfrac{I'(v_0),\cdots I'(v_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}\models \varphi$当且仅当$I'\models \varphi$，可见$I'\models \Phi$，所以$\Phi$是可满足的，证毕。

综上，我们在符号集可数的前提下证明了完备性。

The General Case

首先，我们还是想让一个$S$下一致的公式集$\Phi$能找到一个包含$\Phi$的公式集$\Psi$使得$\Psi$contain witness。在$S$可数的情况下，我们可以列出每个带有存在量词的公式，并为每个公式单独“分配”witness。但是当$S$不可数时，公式是不可列的，而变量只有可列个，显然不能保证每次都能找到一个全新的变量作为witness。但是当$S$不可数时，常数的个数可以是不可数个，所以我们可以每次找一个全新的常量——找到一个不属于$S$的常量符号并把它加入符号集——来充当witness，这样做肯定能保证contain witness。但是每次引入一个新的常量符号，就会产生许多新的包含这个新常量符号的公式，根据定义我们也需要为这些新公式赋予witness。于是再引入新常量符号，再赋予新的公式witness，不断迭代。我们需要证明这样一步一步扩充符号集的方法的确是可行的：

对于符号集$S$，我们为$L^S$中每个带有存在量词的公式$\exists x\varphi$分配一个特定的常量符号，记为$c_{\exists x\varphi}$，定义符号集的拓展$S^\ast:=S \cup \{c_{ \exists x \varphi } \mid \exists x \varphi \in L^S\}$，定义$\Phi^\ast:=\Phi \cup \{(\exists x\varphi\to\varphi\dfrac{c_{ \exists x \varphi }}{x})\mid \exists x\varphi \in L^S\}$。我们证明$\Phi^\ast$在$S^\ast$下是一致的。只需证明$\Phi^\ast$的每个有限子集都是一致的。$\Phi^\ast$的每个有限子集$\Phi_0^\ast$都可以写作$\Phi_0\cup \{\exists x_i\varphi_i \to \varphi_i\dfrac{c_i}{x_i}\mid 1\leq i \leq n\}$，其中$\Phi_0$是$\Phi$的一个有限子集。由于$\Phi_0$有限，它只用到了有限个符号，所以可以取某个$S$的有限子集$S_0$，由The Countable Case可得$\Phi_0$在$S_0$下是可满足的，因此自然也是$S$下可满足的，设这个可满足的$S$-解释为$I$。对于$\exists x_i\varphi_i$，如果$I\models \exists x_i\varphi_i$，那么可以取$a_i$满足$I\dfrac{a_i}{x_i}\models \varphi_i$，否则我们可以取某个固定的$a$使得$a_i=a$。令$c_i=a_i$，那么可以扩展得到一个$S^\ast$下的解释$I^\ast$。由于$\Phi_0$中没有出现新增的常数符号，因此$I^\ast\models \Phi_0$。同时根据我们的构造（以及The Substitution Lemma），$I^\ast\models (\exists x_i\varphi_i\to\varphi_i\dfrac{c_i}{x_i})$，综上可得$I^\ast\models \Phi_0^\ast$，因此$\Phi_0^\ast$一致，证毕。

归纳地，我们令$S_0=S,S_{n+1}=S_n^\ast=S_n\cup\{c_{\exists x\varphi}\mid \exists x\varphi\in L^{S_n}\}$，令$\Phi_0=\Phi$，$\Phi_{n+1}=\Phi_n\cup$$\{(\exists x\varphi\to\varphi\dfrac{c_{\exists x\varphi}}{x})\mid \exists x\varphi \in L^{S_n}\}$。根据上一段的证明，归纳可得每个$\Phi_n$都是一致的。令$\Psi=\bigcup\limits_{n\in \mathbb{N}}\Phi_n$，由于$\Phi_{n}\subseteq \Phi_{n+1}$，可见$\Psi$的任意有限子集都被包含在某个$\Phi_m$里，所以$\Psi$是一致的。令$S'=\bigcup\limits_{n\in \mathbb{N}}S_n$，由于$S_{n}\subseteq S_{n+1}$，所以对于任意的$\exists x\varphi\in L^{S'}$都可以找到某个$S_m$使得$\exists x\varphi\in L^{S_m}$，因此对任意$\exists x\varphi\in L^{S'}$都可以找到某个常量符号$c\in L^{S'}$使得$(\exists x\varphi\to\varphi\dfrac{c}{x})\in \Psi$，也即$\Psi$contain witness。这样我们就证完了每个$S$下一致的公式集$\Phi$能找到一个包含$\Phi$的公式集$\Psi$使得$\Psi$contain witness。

接下来，只需证明对任意$S$下一致的集合$\Psi$都可以找到一个包含它的一致的集合$\Theta$使得$\Theta$是negation complete的。在The Countable Case中，我们通过依次列出所有公式并尝试把每个公式“塞进”$\Psi$里从而通过对自然数的归纳完成了证明。但是现在$L^S$是不可数的，我们不再能这么做了。我们这样做证明：

取出所有$L^S$中包含$\Psi$的一致的集合，得到$\mathfrak{U}:=\{\Phi\mid \Psi\subseteq \Phi \subseteq L^S \text{ and Con}_S \ \Phi\}$。$\mathfrak{U}$可以看作以集合的包含关系为偏序关系的一个偏序集。对于\U上任意的一条链$\mathfrak{B}$，把$\mathfrak{B}$上的公式集全都并且来得到$\Theta_1=\bigcup\limits_{\Phi\in \mathfrak{B}}\Phi$，可以证明$\Theta_1$是一致的：只需证明$\Theta_1$的任意有限子集$\Theta_0$是一致的，记$\Theta_0=\{\varphi_1,\cdots,\varphi_n\}$，那么对于每个$\varphi_i$都可以找到某个$\Phi_i\in \mathfrak{B}$使得$\varphi_i\in \Phi_i$。而$\mathfrak{B}$是链，所以可以取出序关系最大的那个$\Phi_k$，它满足$\Theta_0\subseteq \Phi_k$。而$\Phi_k$是一致的，因此$\Theta_0$也是一致的，证毕。

引入Zorn’s Lemma：在偏序集$P$中，如果$P$的每一条链都有一个$P$中元素作为上界，那么$P$中存在极大元。我们在上一段中证明了，\U中任意一条链$\mathfrak{B}$都有上界$\bigcup\limits_{\Phi\in \mathfrak{B}}\Phi$，并且这个上界也是一个一致的公式集，也即属于偏序集\U，所以根据Zorn’s Lemma偏序集\U有最大元，也即存在\Theta\in \U满足$\text{Con}_S \ \Theta$且不存在$\text{Con}_S \ \Theta'$使得$\Theta\subsetneq \Theta'$。下面证明$\Theta$是negation complete的：如果不是这样，那么存在$\varphi$使得$\Theta\vdash \varphi$和$\Theta\vdash \neg\varphi$都不成立，$\Theta\vdash \varphi$等价于$\Theta \cup\{\neg\varphi\}$不一致，$\Theta\vdash \neg \varphi$等价于$\Theta\cup \{\varphi\}$不一致，所以得到$\Theta \cup\{\neg\varphi\}$和$\Theta \cup\{\varphi\}$都是一致的。但是$\Theta$是最大元，那么只能是$\Theta \cup\{\neg\varphi\}=\Theta \cup\{\varphi\}=\Theta$，也即$\varphi$与$\neg\varphi$都属于$\Theta$，与$\Theta$一致矛盾。证毕。

---

这样，我们最终完成了整个完备性的证明：对于任意的符号集$S$，任意$\Phi \subseteq L^S$和$\varphi\in L^S$满足$\Phi \vdash_S \varphi$当且仅当$\Phi \models \varphi$。等价地，$\text{Con}_S \ \Phi$当且仅当$\text{Sat}_S \ \Phi$。