哥德尔完备性定理

Sequent Calculus

下面我们要把一阶逻辑的“证明”形式化定义。一个证明可以看作若干个（有限个）步骤，每个步骤是根据一些规则从一些命题推出一个命题。于是，每个步骤就可以写作由$n$个（必须是有限的）formula$\varphi_1\varphi_2\cdots\varphi_n$推出formula $\varphi$。如果这一过程是满足证明法则的，就称$\varphi$是从$\varphi_1\cdots\varphi_n$中derivable的命题，记为$\vdash \varphi_1\cdots\varphi_n \ \varphi$。由formula集合$\Phi$能“证明”出formula $\varphi$，就是指前提都落在$\Phi$内，记为$\Phi \vdash \varphi$。一阶逻辑的“证明法则”是十条basic rules，在此不详细写出。一个证明过程实际上是在给定条件的基础上，反复运用始终可以使用的basic rules，最后推演出想要的结论的过程。操作这一演绎过程的计算法则就称为Sequent Calculus。

我们注意到$\Phi$可能是无限集，但我们能证明$\Phi \vdash \varphi$当且仅当存在$\Phi$的有限子集$\Phi_0$使得$\Phi_0\vdash \varphi$：右推左显然；左推右，由于证明是有限步的，每一步也是有限的，因此一个证明中用到的前提也一定是有限的，取这些用到的前提构成有限的$\Phi_0$即可。这体现了一种“紧性”（有限覆盖）。

Completeness(完备性)

我们注意在一个证明系统中，“可证性”与“真理性”的关系并不是显然的。$\Phi \vdash \varphi$仅仅表明在Sequent Calculus下存在一个机械地推理过程能由$\Phi$中的命题推出$\varphi$。而当我们要说明这一过程在语义上是正确的(correct)，我们说的实际是$\Phi \models \varphi$（只要$\Phi$满足语义上就有$\varphi$满足）。于是一个自然的问题是，是否总是有$\Phi \vdash \varphi \iff \Phi \models \varphi$？也即可证性和真理性是否总是等价的？在一阶逻辑中我们将看到的，可证性与真理性确实是等价的，这称为哥德尔完备性定理——正确的一定是可证的，可证的一定是正确的。

下面证明只要$\Phi \vdash \varphi$成立，就一定有$\Phi \models \varphi$成立。也即，可证的一定是正确的，这个性质称为Soundness。我们首先对于sequent calculus的basic rules证明这一事实成立（此处省略），而任何一个证明都只是basic rules的反复运用，因此归纳地，这一事实在任何证明中都成立。

接下来要证$\Phi \models \varphi$能推出$\Phi \vdash \varphi$成立。也即正确的一定是可证的。我们首先证明，这一命题等价于一个集合的consistency(一致性)能推出satisfiable。为此我们要先定义consistency。

Consistency(一致性)

一个formula集合$\Phi$的consistency是指$\Phi$不能证出两个矛盾的命题，也即不存在$\varphi$使得又有$\Phi \vdash \varphi$又有$\Phi \vdash \neg \varphi$。由此可得，如果$\Phi$不是consistent的（称为inconsistent)，那么存在这样的$\varphi$。我们的basic rules指出，如果一个前提能同时推出两个相反的命题，那么它可以推出任何命题。因此$\Phi$是inconsistent的当且仅当它能推出任何命题。由此可得consistency等价于“存在一个命题是证不出来的”。consistency也有一个类似紧性的性质。

如果$\Phi$是一致的当且仅当它的任何有限子集是一致的（有限覆盖）。左推右显然；右推左，如果$\Phi$不是一致的，那么存在一个Sequent Calculus推出矛盾，这个证明是有限的，因此对应着一个有限子集推出了矛盾，与一致性矛盾。

另外，satisfiable的集合一定是consistent的。假如不一致，那么会又有$\Phi \vdash \varphi$又有$\Phi \vdash \neg \varphi$。此时根据Soundness，又有$\Phi \models \varphi$又有$\Phi \models \neg \varphi$。而在一阶逻辑的语义定义中，矛盾是不允许的。因此$\Phi$一定是不可满足的。

根据basic rules中的case analysis，我们能证明$\Phi \vdash \varphi$等价于$\Phi \cup \{\neg \varphi\}$是不一致的。同理，$\Phi \vdash \neg\varphi$等价于$\Phi \cup \{\varphi\}$是不一致的。由此，如果$\Phi \cup \{\neg \varphi\}$和$\Phi \cup \{\varphi\}$都是不一致的，那么$\Phi \vdash \varphi$和$\Phi \vdash \neg\varphi$都成立，也即$\Phi$是不一致的。逆否命题得到$\Phi$一致能推出$\Phi \cup \{\neg \varphi\}$和$\Phi \cup \{\varphi\}$中至少有一个一致。

于是我们可以说明“$\Phi \models \varphi$能推出$\Phi \vdash \varphi$”等价于“consistency能推出satisfiable”。前者的逆否命题为“ 如果$\Phi \not\vdash \varphi$那么$\Phi \not\models \varphi$”，其中$\Phi \not\vdash \varphi$等价于$\Phi\cup\{\neg\varphi\}$一致；$\Phi \not\models \varphi$等价于存在$\mathfrak{I}$使得$\mathfrak{I}\models\Phi$而$\mathfrak{I} \not\models \varphi$，等价于$\mathfrak{I} \models \Phi \cup \{\neg\varphi\}$，也即$\Phi \cup \{\neg\varphi\}$ is satisfiable。于是，这个命题可以转化为“$\Phi \cup \{\neg \varphi\}$ is consistent可以推出$\Phi\cup \{\neg \varphi\}$ is satisfiable”。下面证明这等价于“$\Phi$ is consistent可以推出$\Phi$ is satisfiable”。上证下，如果$\Phi$ is consistent，取$\psi \in \Phi$，显然$\Phi \cup \{\neg\neg \psi\}$ is consistent，那么得到$\Phi \cup \{\neg\neg \psi\}$ is satisfiable的，所以存在$\mathfrak{I}$使得$\ J \models \Phi$且$\ J \models \neg\neg \psi$，因此$\Phi$是satisfiable的；下证上用$\Phi \cup \{\neg \varphi\}$代入$\Phi$即可。

Henkin's Theorem

因此我们只需证明consistency能推出satisfiable。（本质上我们在证明这二者的等价性，因为satisfiable总能推出consistency。）

假设$\Phi$是一致的。如果存在一个精准刻画“可证”的解释$\mathfrak{I}$，使得对于任何的$\varphi$都有$\mathfrak{I}\models \varphi \iff \Phi \vdash \varphi$，那么此时就能立即得到$\mathfrak{I} \models \Phi$（因为$\Phi$总能证得自身的所有formula）。为此，我们试图构造一个项的等价类模型，它把所有在$\Phi$的证明意义下相等的term收集为一个项的等价类，也即如果有$\Phi \vdash t_1\equiv t_2$就把$t_1$和$t_2$放在同一个等价类里。由此得到的structure的universe就是全体等价类，把所有变量都解释为对应的等价类，我们就得到了关于$\Phi$的项模型解释$\mathfrak{I}^\Phi$。我们希望对$\varphi$归纳，证明任何的$\varphi$都有$\mathfrak{I}^\Phi\models \varphi \iff \Phi \vdash \varphi$。

然而此时我们发现直接归纳是不可行的，因为存在这样的$\Phi$，它使得项模型中所有变量都解释为了某个单一的元素，但formula中的存在符号$\exists$却使得在解释时会用到universe中的其它元素。换言之，要想使用项模型证明，$\Phi$单单满足一致性这一条件是不够的。为此，我们要规定$\Phi$要额外满足negation complete和contain witness这两个条件，前者要求对于任意的formula $\varphi$，$\Phi$必须要能够证出$\varphi$和$\neg \varphi$中的恰好一个，后者要求每个公式$\varphi$和变元$x$都要满足$\Phi$能证出$\exists x\varphi \to \varphi\dfrac{t}{x}$（每个成立的formula都要有见证者，也就是说是真的实际的成立而不是形式上的成立）。在这样的附加条件下，我们就顺利地通过对$\varphi$的结构归纳得到了证明。这就是Henkin's Theorem：如果$\Phi$满足consistent,negation complete和contain witness这三个条件，那么任何的$\varphi$都有$\mathfrak{I}^\Phi\models \varphi \iff \Phi \vdash \varphi$，因此$\mathfrak{I}^\Phi \models \Phi$。因此$\Phi$是可满足的。我们得到了当$\Phi$满足consistent,negation complete和contain witness这三个条件时，完备性成立。

The Countable Case

现在为了证明原来的完备性，我们需要逐步删掉我们在$\Phi$上附加的条件。为此，我们先假设我们讨论的符号集是至多可数的。既然符号可数，而一阶逻辑中每个公式的长度都必须是有限的，那么可以列出所有公式。这时我们可以给每个公式强行分配一个witness，承担witness的变元最好需要是一个全新的变量，所以我们附加上free variable总数有限这一条件。这样构造的集合包含了$\Phi$，并且可以证明是consistent的。在此基础上再次枚举所有公式，对于每个公式，如果把它合并进$\Phi$里依然保持consistent就合并，否则跳过，可以证明这样得到的新集合一定是negation complete。于是我们得到了一个包含$\Phi$的更大集合，它同时满足consistent, negation complete和contain witness。所以它是可满足的，随之$\Phi$也是可满足的。

接下来我们需要删掉free variable总数有限这一条件。在这里我们首先把所有的free variable都用常元代替，这样free variable为空，所以可以用刚才得到的定理得到它是satisfiable的，并且我们能够证明这样得到的新的$\Phi'$是可满足的，并且任意一个公式在原来的解释下满足当且仅当在新的解释下满足。这样我们最终得到$\Phi$是可满足的。

The General Case

最后我们需要删掉符号集可数这一条件。我们还是希望扩张公式集来让他满足negation complete和contain witness，但由于符号集不可数我们无法列出所有公式。而现在常数的数量没有了可数的限制，所以我们可以分配与公式同样多数量的常数来充当witness。证明整体的consistency只需要证明所有有限子集的consistency（紧性），这时就可以直接运用可数情形的结论。而每一次我们加入常元分配witness都为产生许多新的带有这些常元的公式，因此我们要不断地继续为它们发配witness，这个过程将会发生可数次，但consistency依然是始终能够保证的。

接下里需要扩展negation complete，而对negation complete的拓展需要用到Zorn Lemma（证明略），它描述了一个集合意义下的对“取极限”封闭的集合有极大元的性质，我们以公式集的包含关系构造满足Zorn Lemma条件，并发现如果不满足negation complete就会与极大元的性质矛盾。这样我们最终完成了不可数情形的证明。

哥德尔完备性定理与推论

最终，我们得到对于任意的$\Phi$和$\varphi$，$\Phi \vdash \varphi \iff \Phi \models \varphi$，这称为“哥德尔完备性定理”。完备性指出了一阶逻辑中可证性和真理性的等价性，我们也看到了这同时意味着一致性和可满足性的等价性。我们来看看这将预示着什么。

在完备性证明中我们看到，一致的（可满足的）的集合一定存在解释，而可满足用到的解释正是项模型$\mathfrak{I}^\Phi$。而项模型中universe的大小一定不可能超过原来项的个数。因此如果$\Phi$中项的个数是可数的（等价地公式的个数是可数的），就一定存在一个universe可数的解释满足$\Phi$。也就是我们一定有$|A|\leq|T^S|=|L^S|$，其中竖线表示集合的势。这称为The Lowenheim-Skolem Theorem。

我们在Sequent Calculus中指出过$\Phi \vdash \varphi$当且仅当存在$\Phi$的有限子集$\Phi_0$使得$\Phi_0\vdash \varphi$。现在根据完备性得到，$\Phi \models \varphi$当且仅当存在$\Phi$的有限子集$\Phi_0$使得$\Phi_0\models \varphi$。另外我们指出过$\Phi$是一致的当且仅当它的任何有限子集是一致的。现在根据完备性，一致等价于可满足，因此可以有：$\Phi$是可满足的当且仅当它的任何有限子集是可满足的。以上性质都称为紧性，因为它体现了拓扑学中紧集的有限覆盖性质。

在对完备性的讨论中，我们发现了对universe的拓展其实是件难事。一个在更小的universe上存在解释的集合，并不保证在更大的universe上存在解释（不然我们在采用项模型的时候就可以直接结构归纳了）。然而，利用紧性我们可以论证一下事实：如果$\Phi$对于任何自然数$n$都存在universe大小超过$n$的解释$\mathfrak{I}_n$，那么$\Phi$存在一个universe无限的解释。（ 方法就是我们可以往公式集里塞废话，我们很容易构造一个公式集专门刻画universe里至少有$n$个不同元素，对于全体自然数$n$把这些废话塞进$\Phi$里，对于任意有限子集都是存在$\mathfrak{I}_n$的，因此存在满足新集合的解释，这个解释universe无穷大，并且一定满足$\Phi$。）另一个事实是，如果我们已知$\Phi$是存在一个universe无穷的解释的，那么对于$\Phi$的任何解释我们总能找到一个universe更大的解释。（根据紧性，存在universe无穷的解释意味着其是可满足的，因此任意有限子集都是可满足的。我们塞入许多带有全新的常元的废话公式使得能满足新集合的universe必须更大，那么既然新集合的任意有限子集都可满足，新集合就一定可满足，并且universe更大。）