哥德尔完备性定理

我们讨论何为“证明”。一个证明过程实际上是在给定条件的基础上，反复运用始终可以使用的基本规则，最后推演出想要的结论的过程。这个过程可以形式化地描述，称为Sequent Calculus。由formula集合\(\Phi\)能“证明”出formula \(\varphi\)，记为\(\Phi \vdash \varphi\)。

一个可以被证明的事实是，只要\(\Phi \vdash \varphi\)成立，就一定有\(\Phi \models \varphi\)成立。前者是根据证明的基本规则（纯粹语法层面的迭代，与formula的语义无关）表示集合\(\Phi\)可以证出\(\varphi\)；后者是语义层面的推出关系，对于选定的某个解释如果\(\Phi\)成立了那么\(\varphi\)也一定成立。这个事实称为正确性，它的证明可以这样理解：\(\varphi\)能被\(\Phi\)证出，形式化地就是存在一系列推演使得\(\Phi\)内部的一系列formula能直接导出\(\varphi\)，换言之存在\(\Phi\)中的某个子集，\(\varphi\)本身就蕴含在这些formula之中了。因此\(\Phi\)能推出\(\varphi\)在任何使得\(\Phi\)成立的语义解释上都是恒成立的。这个事实称为正确性，可证的一定是正确的。

接下来要讨论的问题是，\(\Phi \models \varphi\)成立能否推出\(\Phi \vdash \varphi\)成立？正确的是否一定是可证的？这称为完备性。我们首先证明，这一命题等价于一致性能推出可满足性（我们证明过可满足一定一致，因此我们现在其实想证明这二者的等价性）。其中，\(\Phi\)的一致性是指\(\Phi\)不能证出两个矛盾的命题，也即不存在\(\varphi\)使得又有\(\Phi \vdash \varphi\)又有\(\Phi \vdash \neg \varphi\)。可满足性即存在一个解释\(\mathfrak{I}\)使得\(\mathfrak{I}\models \Phi\)。

如果我们直接进行结构归纳，我们会发现证不出来，比如可以构造这样的\(\mathfrak{I}\)使得所有变量都解释为了某个单一的元素，但formula中的存在符号却使得在解释时会用到universe中的其它元素。为此，我们要规定\(\Phi\)要额外满足negation complete和contain witness这两个条件，前者要求对于任意的formula \(\varphi\)，\(\Phi\)必须要能够证出\(\varphi\)和\(\neg \varphi\)中的恰好一个，后者要求每个公式\(\varphi\)和变元\(x\)都要满足\(\Phi\)能证出\(\exists x\varphi \to \varphi\dfrac{t}{x}\)（每个成立的formula都要有见证者，也就是说是真的实际的成立而不是形式上的成立）。这样我们就顺利的通过构造项的等价类得到了一个始终能够解释\(\Phi\)的\(\mathfrak{I}^\Phi\)。

现在为了证明原来的完备性，我们需要逐步删掉我们在\(\Phi\)上附加的条件。为此，我们先假设我们讨论的符号集是至多可数的。既然符号集可列，那么可以列出所有公式，并给每个公式强行分配一个witness。而承担witness的变元需要最好是一个全新的变量，所以我们附加上free variable总数有限这一条件。这样构造的集合包含了\(\Phi\)，并且可以证明是consistent的。再次基础上再次枚举所有公式，对于每个公式，如果把它合并进\(\Phi\)里依然保持consistent就合并，否则跳过，可以证明这样得到的新集合一定是negation complete。于是我们得到了一个包含\(\Phi\)的更大集合，它同时满足consistent, nagetion complete和contain witness。所以它是可满足的，随之\(\Phi\)也是可满足的。接下来我们需要删掉free variable总数有限这一条件。在这里我们首先把所有的free variable都用常元代替，这样free variable为空，所以可以用刚才得到的定理得到它是可满足的，并且我们能够证明这样得到的新的\(\Phi'\)是可满足的，并且任意一个公式在原来的解释下满足当且仅当在新的解释下满足。这样我们最终得到\(\Phi\)是可满足的。

最后我们需要删掉符号集可数这一条件。（还没讲）

通过以上论证我们最终得到\(\Phi \vdash \varphi \iff \Phi \models \varphi\)，这称为“哥德尔完备性定理”。