04 哥德尔完备性定理

我们已经说明了基于一阶逻辑语言的相继式演算具有可靠性(soundness)，也即：选定符号集$S$，对于任意$S$-formula集合$\Phi$和$S$-formula $\varphi$，如果$\Phi\vdash \varphi$成立，那么一定有$\Phi \models \varphi$成立。可靠性是简单而直接的，我们只是把定义展开就得出了结论。更困难的反过来的问题。我们想证明基于一阶逻辑语言的相继式演算的完备性(completeness)：任何$\Phi$与$\varphi$，只要$\Phi \models \varphi$成立，就有$\Phi \vdash \varphi$成立。

完备性的问题最早由哥德尔给出了证明，称为哥德尔完备性定理。一旦有了完备性，今后我们便只需要根据相继式演算在字符串上的语法来检查形式化证明的正确性，就可以验证数学事实上的正确性。我们不再需要用模糊的自然语言来描述证明，而可以用清晰、可验证的形式语言来取而代之。进而，机器也可以代替人类做证明：相比于人类，机器有能力准确无误地对形式符号做变换，这比人类用自然语言论证的证明可靠得多（当然，人类可以依据直觉跳跃地得出结论，但机器只能按照演算规则做运算）。

哥德尔原始的完备性定理的证明比较复杂。后人在此基础上做了改进，给出了一个更简单的证明（尽管还是比较复杂）。

一致性

尽管相继式演算的推导规则是可靠的，但如果前提$\Phi$中本身就“包含了矛盾”，就会根据Modified Contradiction Rule能够导出一切命题，包括错误的命题。例如，$\Phi=\{t\equiv t,\neg t\equiv t\}$就能够演算出一切$S$-formula。所以，我们要定义一种对$\Phi$的描述，要求$\Phi$中“不包含矛盾”，这称之为一致性(consistency)：如果一个$S$-formula集合$\Phi$对于任意的$S$-formula $\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$成立。所以，$\text{Inc }\Phi$等价于：对于任意的$\psi$都有$\Phi \vdash \psi$成立。因此$\text{Con }\Phi$等价于：存在一个$\psi$使得$\Phi \vdash \psi$不成立。也就是说，一个一致的公式集一定有一个“证不出来”的命题。我们把“$\Phi \vdash \psi$不成立”记为$\Phi \not\vdash \psi$。

Remark: 注意区分“$\Phi \vdash \neg\varphi$”和“$\Phi \not\vdash \varphi$”，这二者的定义截然不同。$\Phi \vdash \neg \varphi$的含义是，存在一个相继式演算的算式，其横线下方是sequence $\Phi \ \neg\varphi$。也即，存在一个有限长的形式化证明从$\Phi$出发得出一阶逻辑formula $\neg\varphi$。而$\Phi \not\vdash \varphi$的含义是，任何一个相继式演算的算式横下下方都不可能是$\Phi \ \varphi$。也即，不存在一个形式化证明能从$\Phi$出发推出$\varphi$。

同理，$\Phi \models \neg\varphi$和$\Phi\not\models \varphi$的含义也截然不同。前者的含义是，对于任意$\mathfrak{I}$，只要$\mathfrak{I}(\Phi)=true$，就有$\mathfrak{I}(\varphi)=false$；后者的含义是，存在$\mathfrak{I}$使得$\mathfrak{I}(\Phi)=true$而$\mathfrak{I}(\varphi)=false$。在绝大多数情况下，二者是不等价的。

一个可满足的(satisfiable)公式集一定是一致的。证明：假设存在$\mathfrak{I}$使得$\mathfrak{I}( \Phi)=true$。如果$\Phi$不一致，那么存在$\varphi$，又有$\Phi \vdash \varphi$又有$\Phi \vdash \neg \varphi$。根据可靠性，又有$\Phi \models \varphi$又有$\Phi \models \neg \varphi$。所以又有$\mathfrak{I}(\varphi)=true$又有$\mathfrak{I}( \varphi)=false$，这在数学事实上是矛盾的。因此$\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$等价于“存在$\mathfrak{I}$使得$\mathfrak{I}(\Phi)=true$而$\mathfrak{I} (\varphi)=false$”，等价于“存在$\mathfrak{I}$使得$\mathfrak{I}(\Phi \cup \{\neg\varphi\})=true$”，也即$\text{Sat} (\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\}$可满足，所以存在$\mathfrak{I}$使得$\mathfrak{I}(\Phi)=true$且$\mathfrak{I}(\neg\neg\psi)=true$，因此$\text{Sat }\Phi$。

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

Henkin's Theorem

为了证明“一致性是否意味着可满足性”，我们容易想到采用构造性证明：为每个一致的公式集构造一个能满足它的interpretation。我们自然地期待，我们能找到一种统一的构造方式。

对于每个一致的公式集$\Phi$，只需要能找到一个$\mathfrak{I}=(\mathfrak{A},\beta)$使得：对于任意$\varphi \in \Phi$，都有$\mathfrak{I}(\varphi)=true$。为此，只需证明存在这个$\mathfrak{I}$，对于任意满足$\Phi \vdash \varphi$的formula $\varphi$都有$\mathfrak{I}(\varphi)=true$。对于任意的term $t_1,t_2$，当$\varphi$形如$t_1\equiv t_2$时，我们可以要求$\Phi \vdash t_1\equiv t_2 \implies$ $\mathfrak{I}(t_1)=\mathfrak{I}(t_2)$。于是自然地，我们可以基于“项的等价类”来定义$\mathfrak{I}$的论域：

如果$\Phi \vdash t_1\equiv t_2$，就称$t_1,t_2$等价，记为$t_1\sim t_2$（之所以可以称为等价，是因为论域中的（数学事实上的）相等是等价关系）。把$t$所在的等价类记为$\bar{t}=\{t'\in T^S\mid t\sim t'\}$。所有等价类的集合记为$T^\Phi=\{\bar t\mid t \in T^S\}$，我们就把这个集合作为$\mathfrak{I}$的论域，上标$\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 $\mathfrak{I}^\Phi =(\mathfrak{T}^\Phi,\beta^{\Phi})$，称为term interpretation。

下面证明，term interpretation确实满足对任意$t\in T^S$满足$\mathfrak{I}^\Phi(t)=\bar t$。只需对$t$结构归纳：

• 原子性的情况，$\mathfrak{I}^{\Phi}(x)=\bar x$与$\mathfrak{I}^\Phi(c)=\bar c$根据定义已经成立；
• $\mathfrak{I}^\Phi(ft_1\cdots t_n)$ $=f^{T^\Phi}(\mathfrak{I}^\Phi(t_1),\cdots,\mathfrak{I}^\Phi(t_n))$ $=f^{T^\Phi}(\bar t_1,\cdots, \bar t_n)$ $=\overline{ft_1\cdots t_n}$；

接着我们用term interpretation为formula赋予语义。对于原子性的情况：

• 当$\varphi=t_1\equiv t_2$时，我们已经确认$\Phi \vdash \varphi \implies \mathfrak{I}^\Phi(\varphi)=true$确实成立；
• 当$\varphi = Rt_1\cdots t_n$时，$\Phi \vdash Rt_1\cdots t_n$当且仅当$R^\Phi(\bar t_1,\cdots,\bar t_n)$成立当且仅当$\mathfrak{I}^{\Phi}(Rt_1\cdots t_n)=true$。

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

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

考虑$S=\{R\}$，$\Phi=\{Rx \lor Ry\}$。那么$\Phi \vdash Rx\lor Ry$，我们想要推出$\mathfrak{I}^{\Phi} (Rx\lor Ry)=true$，也即“$\mathfrak{I}^{\Phi}(Rx)=true$或$\mathfrak{I}^{\Phi}(Ry)=true$”。假如$\mathfrak{I}^{\Phi} (Rx)=true$成立，这等价于$\Phi \vdash Rx$，由可靠性得$\Phi \models Rx$。此时可以构造$\mathfrak{I}_1$：论域为自然数$\{0,1\}$，$R(0)$成立$R(1)$不成立，$\beta(x)=1,\beta(y)=0$，那么$\mathfrak{I}_1(Rx\lor Ry)=true$但是$\mathfrak{I}_1(Rx)=false$，这说明$\Phi \not\models Rx$，矛盾。同理，$\mathfrak{I}^{\Phi}(Ry)=true$也不成立。说明$\mathfrak{I}^{\Phi} (Rx\lor Ry)=false$。这里的问题出自“或”这一连接词，它导致我们不能推出由“或”连接的任意一个子formula究竟是真是假。例如上面我们已经证明了$\Phi \vdash Rx$不成立，还可以证明$\Phi \vdash \neg Rx$也不成立：如果$\Phi \vdash \neg Rx$，那么$\Phi \models \neg Rx$，可以构造一个$\mathfrak{I}_1'$令universe为自然数$\{0,1\}$，$R(0)$成立$R(1)$不成立，$\beta(x)=0,\beta(y)=1$，那么$\mathfrak{I}_1'(\Phi)=true$但$\mathfrak{I}_1'(\neg Rx)=false$，矛盾。换言之，对于$\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的结构归纳了。我们证明加强后的命题$\mathfrak{I}^{\Phi} (\varphi)=true \iff \Phi \vdash \varphi$。

• 左推右，假设$\mathfrak{I}^{\Phi} (\neg\varphi)=true$，也即$\mathfrak{I}^{\Phi} (\varphi)=false$，根据归纳假设$\Phi \not\vdash \varphi$，于是由negation complete得到$\Phi \vdash \neg\varphi$必须成立；右推左，假设$\Phi \vdash \neg \varphi$，由于$\Phi$一致，所以$\Phi \not\vdash \varphi$，根据归纳假设$\mathfrak{I}^{\Phi} (\varphi)=false$；
• 左推右：假设$\mathfrak{I}^{\Phi} (\varphi \lor \psi)=true$，也即$\mathfrak{I}^{\Phi} (\varphi)=true$或$\mathfrak{I}^{\Phi} (\psi)=true$，由归纳假设这当且仅当$\Phi \vdash \varphi$或$\Phi \vdash \psi$。无论前者成立还是后者成立，都可以由规则七得$\Phi \vdash (\varphi \lor \psi)$。右推左：假设$\Phi \vdash (\varphi \lor \psi)$，假如$\Phi \vdash \varphi$成立，由归纳假设$\mathfrak{I}^{\Phi} (\varphi)=true$；假如$\Phi \vdash \varphi$不成立，由negation complete得到$\Phi \vdash \neg\varphi$必须成立，由Moified Or Rule推出$\Phi \vdash \psi$，由归纳假设$\mathfrak{I}^{\Phi} (\psi)=true$；
• 由The Substitution Lemma，$\mathfrak{I}^{\Phi} (\exists x\varphi)=true$等价于存在$t\in T^S$使得$\mathfrak{I}^{\Phi} (\varphi\dfrac{t}{x})=true$，由归纳假设这等价于存在$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 $\mathfrak{I}^{\Phi}$使得$\Phi\vdash \varphi \iff \mathfrak{I}^{\Phi} (\varphi)=true$。这称为Henkin's Theorem。由此容易推出$\mathfrak{I}^{\Phi} (\Phi)=true$，可见对于contain witness以及negation complete的公式集如果是一致的就是可满足的。在这样的特殊限制下，完备性成立。

符号集为可数集时的完备性

我们已经发现，如果不对$\Phi$加以特殊的限制，那么$\Phi$的term interpretation不足以作为那个能够满足$\Phi$的interpretation。事实上，我们也难以找到一个其它的自然的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$，$x$为$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（因为contain witness是对所有$L^S$中形如$\exists x\varphi$的formula定义的）。这样我们就最终对于每个一致的且自由变量不超过有限个的$\Phi$，找到了一个一致的、contain witness的、negation complete的集合，由Henkin's Theorem它可以被term interpretation满足，由此推出$\Phi$也可满足（这个满足$\Phi$的解释$\Theta$上的term interpretation限制到$\Phi$以后的版本）。

最后我们需要去掉“$\Phi$中出现的所有自由变量不超过有限个”的约束。我们发现，在“可满足性”的意义下一个自由变量和一个常量在语义上并没有区别，所以我们其实可以构造一个等价的公式集$\Phi'$，其中所有的自由变量都用常数符号替换，这样做了以后用作witness的变量就不会和普通变量发生冲突了。我们只需证明这种替换在可满足性的意义下是等价的，而这其实已经包含在The Coincidence Lemma所表达的含义当中了。具体地，令$S':=S\cup \{c_0,c_1,\cdots\}$，其中$c_i$是全新引入的常量符号。对于每个$\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'$的所有有限子集$\Phi'_0=\{\varphi_1',\cdots,\varphi_n'\}$都是可满足的。记$\Phi_0=\{\varphi_1,\cdots,\varphi_n\}$，它是$\Phi$的一个子集因此是关于$S$一致的，而$\Phi_0$是有限集因此只包含有限个自由变量，可以由已经证明的结论推出它是关于$S$可满足的。设$S$-interpretation $\mathfrak{I}$满足$\mathfrak{I}(\Phi_0)=true$，那么可以把每个$c_i$赋值为$\mathfrak{I}(v_i)$而扩展得到一个$S'$下的interpretation $\mathfrak{I}'$。于是，根据The Substitution Lemma得到$\mathfrak{I}'( \varphi\dfrac{c_0,\cdots c_{n(\varphi)}}{v_0,\cdots,v_{n(\varphi)}})=$ $\mathfrak{I}'\dfrac{\mathfrak{I}'(c_0),\cdots,\mathfrak{I}' (c_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}(\varphi)=$ $\mathfrak{I}'\dfrac{\mathfrak{I}(v_0),\cdots \mathfrak{I}(v_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}(\varphi)$，由The Coincidence Lemma这就等于$\mathfrak{I}\dfrac{\mathfrak{I}(v_0),\cdots \mathfrak{I}(v_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}(\varphi )=$ $\mathfrak{I}(\varphi)=true$。所以$S'$-interpretation $\mathfrak{I}'$满足$\mathfrak{I}'(\Phi_0')=true$。

因为$\Phi'$的所有有限子集都是可满足的，所以$\Phi'$的所有有限子集都是一致的。这说明$\Phi'$是一致的：如果$\Phi'$不一致，那么存在一个$\psi$使得$\Phi'\vdash \psi$和$\Phi'\vdash\neg \psi$同时成立，这对应于两个相继式演算证明$S_1,S_2$。因为$S_1,S_2$都是有限长的，所以取这两个证明中所用到的$\Phi'$中的前件，构成$\Phi'$的一个有限子集，这个有限子集是不一致的，这就推出了矛盾。

由于$\Phi'$中实际上没有自由变量，并且是一致的，所以根据已经证明的结论推出$\Phi'$是可满足的（因为“自由变量为空”是“自由变量有限”的一种特殊情况），设这个满足$\Phi'$的interpretation是$\mathfrak{I}'$。根据The Coincidence Lemma，我们可以任意修改$\mathfrak{I}'$中对变量的赋值而不影响其对$\Phi'$的满足性。例如，可以令$\mathfrak{I}'(v_i):=\mathfrak{I}'(c_i)$。于是对于任意$\varphi\in \Phi$，$\mathfrak{I}'(\varphi')=\mathfrak{I}'(\varphi\dfrac{c_0,\cdots, c_{n(\varphi)}}{v_0,\cdots,v_{n(\varphi)}})$ $=\mathfrak{I}'\dfrac{\mathfrak{I}'(c_0),\cdots \mathfrak{I}'(c_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}(\varphi)$ $=\mathfrak{I}'\dfrac{\mathfrak{I}'(v_0),\cdots \mathfrak{I}'(v_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}(\varphi)$ $=\mathfrak{I}'(\varphi)$，可见$\mathfrak{I}'(\Phi)=true$当且仅当$\mathfrak{I}'(\Phi')=true$。所以$\mathfrak{I}'(\Phi)=true$，也即$\Phi$是可满足的，证毕。

这样我们就在符号集可数的前提下证明了完备性。

符号集为不可数集时的完备性

下面我们在符号集不可数的前提下给出完备性的证明。

首先，我们还是想让一个$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$-解释为$\mathfrak{I}$。对于$\exists x_i\varphi_i$，如果$\mathfrak{I}(\exists x_i\varphi_i)=true$，那么可以取$a_i$满足$\mathfrak{I}\dfrac{a_i}{x_i}(\varphi_i)=true$，否则我们可以取某个固定的$a$使得$a_i=a$。令$c_i=a_i$，那么可以扩展得到一个$S^\ast$下的解释$\mathfrak{I}^\ast$。由于$\Phi_0$中没有出现新增的常数符号，因此$\mathfrak{I}^\ast(\Phi_0)=true$。同时根据我们的构造（以及The Substitution Lemma），$\mathfrak{I}^\ast(\exists x_i\varphi_i\to\varphi_i\dfrac{c_i}{x_i})=true$，综上可得$\mathfrak{I}^\ast(\Phi_0^\ast)=true$，因此$\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}$可以看作以集合的包含关系为偏序关系的一个偏序集。对于$\mathfrak{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$中存在极大元。上一段证明了，$\mathfrak{U}$中任意一条链$\mathfrak{B}$都有上界$\bigcup\limits_{\Phi\in \mathfrak{B}}\Phi$，并且这个上界也是一个一致的公式集，也即属于偏序集$\mathfrak{U}$，所以根据Zorn's Lemma偏序集$\mathfrak{U}$有最大元，也即存在$\Theta\in \mathfrak{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\varphi$当且仅当$\Phi \models \varphi$。或等价地，$\text{Con} \ \Phi$当且仅当$\text{Sat} \ \Phi$。

参考文献

[1] H.-D. Ebbinghaus, J.Flum, W. Thomas: Mathematical Logic