我们已经说明了基于一阶逻辑语言的相继式演算具有可靠性(soundness)，也即：选定符号集，对于任意-formula集合和-formula ，如果成立，那么一定有成立。可靠性是简单而直接的，我们只是把定义展开就得出了结论。更困难的反过来的问题。我们想证明基于一阶逻辑语言的相继式演算的完备性(completeness)：任何与，只要成立，就有成立。
完备性的问题最早由哥德尔给出了证明，称为哥德尔完备性定理。一旦有了完备性，今后我们便只需要根据相继式演算在字符串上的语法来检查形式化证明的正确性，就可以验证数学事实上的正确性。我们不再需要用模糊的自然语言来描述证明，而可以用清晰、可验证的形式语言来取而代之。进而，机器也可以代替人类做证明：相比于人类，机器有能力准确无误地对形式符号做变换，这比人类用自然语言论证的证明可靠得多（当然，人类可以依据直觉跳跃地得出结论，但机器只能按照演算规则做运算）。
哥德尔原始的完备性定理的证明比较复杂。后人在此基础上做了改进，给出了一个更简单的证明（尽管还是比较复杂）。
一致性
尽管相继式演算的推导规则是可靠的，但如果前提中本身就“包含了矛盾”，就会根据Modified Contradiction Rule能够导出一切命题，包括错误的命题。例如，就能够演算出一切-formula。所以，我们要定义一种对的描述，要求中“不包含矛盾”，这称之为一致性(consistency)：如果一个-formula集合对于任意的-formula 都不会有和同时成立，就称它是一致的(consistent)，记为。
如果不是一致的，就称是不一致的(inconsistent)，记为。根据定义，等价于：至少存在一个使得和同时成立。根据Modified Contradiction Rule，这说明对于任意的都有成立。所以，等价于：对于任意的都有成立。因此等价于：存在一个使得不成立。也就是说，一个一致的公式集一定有一个“证不出来”的命题。我们把“不成立”记为。
Remark: 注意区分“”和“”，这二者的定义截然不同。的含义是，存在一个相继式演算的算式，其横线下方是sequence 。也即，存在一个有限长的形式化证明从出发得出一阶逻辑formula 。而的含义是，任何一个相继式演算的算式横下下方都不可能是。也即，不存在一个形式化证明能从出发推出。
当然，这二者是有联系的。根据可靠性，意味着，而由语义后承的定义，“”等价于“”（数学事实上一个命题总是非真即假的）。根据可靠性（的逆否命题），我们可以由推出（可靠性的逆否表述：数学事实不成立的命题一定是不能形式化地证出来的）。由此可见，我们说明了“”一定意味着“”。那能否由“”反向得到“”呢？注意到，如果我们用一下完备性的结论就可以证明反向也是成立的：等价于等价于等价于。但我们还没有证明完备性。所以在完备性的证明中，我们不能使用等价于这一结论。
一个可满足的(satisfiable)公式集一定是一致的。证明：假设存在使得。如果不一致，那么存在，又有又有。根据可靠性，又有又有。所以又有又有，这在数学事实上是矛盾的。因此一定是一致的。
等价于。证明：左推右，由规则一，而所以由规则三，因此不一致；右推左，不一致说明能推出所有命题，所以，由规则一，那么根据规则四。
最后，我们证明“对于任意的，”等价于“对于任意的，”。左边命题等价于“ 对于任意的，”，其中等价于“一致”，等价于“存在使得而”，等价于“存在使得”，也即。于是，左边命题等价于“对于任意的， ”（A）。下面证明这等价于“对于任意的，”（B）。（B）推（A），用代入即可；（A）推（B），如果一致，取某一，我们有一致（由sequent calculus可以证明和有“等价性”），那么由（A）可得可满足，所以存在使得且，因此。
这样我们就把完备性问题等价转化为了“一致性是否意味着可满足性”的问题了。
Henkin’s Theorem
为了证明“一致性是否意味着可满足性”，我们容易想到采用构造性证明：为每个一致的公式集构造一个能满足它的interpretation。我们自然地期待，我们能找到一种统一的构造方式。
对于每个一致的公式集，只需要能找到一个使得：对于任意，都有。为此，只需证明存在这个，对于任意满足的formula 都有。对于任意的term ，当形如时，我们可以要求 。于是自然地，我们可以基于“项的等价类”来定义的论域：
如果，就称等价，记为（之所以可以称为等价，是因为论域中的（数学事实上的）相等是等价关系）。把所在的等价类记为。所有等价类的集合记为，我们就把这个集合作为的论域，上标表示这一论域是基于构造的。
对符号集的解释也容易定义：
这样我们就定义好了一个structure，称为term structure，记为。
定义对变量的解释，我们得到了一个interpretation ，称为term interpretation。
下面证明，term interpretation确实满足对任意满足。只需对结构归纳：
接着我们用term interpretation为formula赋予语义。对于原子性的情况：
- 当时，我们已经确认确实成立；
- 当时，当且仅当成立当且仅当。
然而不幸的是，当我们想要基于原子性情况成立做结构归纳时，在遇到量词和连接词的时候出了问题：
考虑，。那么，我们想要推出。假如，那么存在使得，也即存在使得。由The Substitution Lemma等价于，也即。根据上一段的证明这当且仅当。但是由于符号集里只有，所以只能是变量，也即存在变量使得。但是。所以是不一致的。但事实上，是一致的，只需构造一个解释说明它是可满足的：论域是两个自然数，指定成立不成立，所有变量都指派为自然数。于是有（存在使得成立，同时所有变量都被赋为了因此所有都不成立）。这说明是一致的。所以这里产生了矛盾，因此。可见term interpretation无法给出我们期待的结果。这里的问题出自term interpretation会根据能推出的所有等式把term划分到不同的等价类，但实际的情况可能需要我们把同一等价类中的变量解释为不同的值才行：在我们的例子中，对所有term的解释并不是到值域的满射，这就使得这样的formula允许为引入变量的解释之外的值，换言之这样的含存在量词的formula即便缺少witness(见证)也是能够成立的。
考虑，。那么，我们想要推出，也即“或”。假如成立，这等价于，由可靠性得。此时可以构造：论域为自然数，成立不成立，，那么但是，这说明，矛盾。同理，也不成立。说明。这里的问题出自“或”这一连接词，它导致我们不能推出由“或”连接的任意一个子formula究竟是真是假。例如上面我们已经证明了不成立，还可以证明也不成立：如果，那么，可以构造一个令universe为自然数，成立不成立，，那么但，矛盾。换言之，对于存在一个命题使得与都不成立，这就使得我们无法对“或”连接词做归纳了：因为即便两个子命题的正面和反面都不可证，这两个子命题的“或”却是可证的。
由此可见，如果我们想继续使用term interpretation做证明，就必须采取一些补救措施，也即给加上特殊的规定，使得以上两种情况不会出现。对于第一种情况，我们要求对所有存在量词包含见证(contain witness)，定义为：对于所有中形如的formula，存在term 使得。对于第二种情况，我们要求总能证出每个命题的正面或者反面， 也即对于否定是完全的(negation complete)，定义为：对于所有的，和至少一者成立（由于我们总是对一致的公式集用term interpretation，所以其实是“恰好一者”成立）。
现在假设一致的公式集还同时满足contain witness与negation complete两个条件，我们可以继续对formula的结构归纳了。我们证明加强后的命题。
- 左推右，假设，也即，根据归纳假设，于是由negation complete得到必须成立；右推左，假设，由于一致，所以，根据归纳假设；
- 左推右：假设，也即或，由归纳假设这当且仅当或。无论前者成立还是后者成立，都可以由规则七得。右推左：假设，假如成立，由归纳假设；假如不成立，由negation complete得到必须成立，由Moified Or Rule推出，由归纳假设；
- 由The Substitution Lemma，等价于存在使得，由归纳假设这等价于存在使得。只需证这等价于。左推右：应用规则八即可；右推左，根据contain witness存在使得，由Modus ponens可得;
这样，我们就证明了对于contain witness以及negation complete的公式集，如果它是一致的，那么可以找到term interpretaion 使得。这称为Henkin’s Theorem。由此容易推出，可见对于contain witness以及negation complete的公式集如果是一致的就是可满足的。在这样的特殊限制下，完备性成立。
符号集为可数集时的完备性
我们已经发现，如果不对加以特殊的限制，那么的term interpretation不足以作为那个能够满足的interpretation。事实上，我们也难以找到一个其它的自然的interpretation构造使得它能直接满足。但是，term interpretation距离证明完备性已经很接近了。我们想让完备性对于一般的不满足contain witness和negation complete的公式集也成立，可以证明对于一般的一个一致的公式集，我们总可以做一些扩展——往里面“加入”若干条formula——从而在保持一致性的前提下使得它变得contain witness和negation complete。假设经过扩展以后的公式集是可满足的，那么作为它的子集自然也是可满足的了。
我们首先在限定符号集是可数集（或有限集）的情况下给出证明。
第一步，我们想对于一个一致的公式集，找到一个一致的公式集使得同时 contain witness。然而这是一个假命题，考虑以下反例： ，是可满足的（只需把所有变量和函数值都解释为自然数，并令universe为）因此是一致的。然而，假如存在一致的包含且contain witness，那么对于任意和任意变量都满足存在使得，取为，为就有 ，于是。再取，为，得到，但是由等式的传递性，与一致矛盾。这里出现的问题是，实际上不存在能够充当的witness的变量，因为每个witness变量本身都会被吸收，而不能真正指向那个在interpretation中未被用来赋值的值。
为此，我们再添加一条限制，规定中出现的所有自由变量不超过有限个（也即 是有限集），这样就总能找到一个全新的变量来充当witness。下面证明，如果是一致的且有限，那么存在一个一致的公式集包含且contain witness。因为一阶逻辑的alphabet有限且formula长度有限，并且符号集是可数的，因此也是可数的，可以依次列出所有带有存在量词的formula 。归纳地定义，其中是不属于 的下标最小的变量（这是可以做到的因为自由变量的总个数是有限的），令，，显然 contain witness且包含。下面证明是一致的。首先证明每个都是一致的，对归纳，时显然成立；假设不一致，那么对于任意都有，根据sequent calculus得到与，而后者根据规则九得到，于是根据规则四（分类讨论规则）得到对任意成立，与一致矛盾。此时可以证明是一致的，假如不一致，那么存在的一个有限子集使得存在使得且，而，一定存在某个包含，这就推出不一致，矛盾。证毕。
第二步，我们想对于每个一致的公式集，找到一个一致的公式集使得同时 negation complete。这里的构造很简单，我们只需列出全部的中的公式，依次试着把每个公式“合并”到上同时确保一致性成立。具体的，令，如果是一致的，否则。令。显然包含并且是一致的（运用与第一步中相同的论证），只需证明它negation complete。对于任意，它对应着某个下标。如果不成立，也即等价地一致，那么其子集也一致，说明，因此。这就说明与中总是至少有一个是成立的，也即negation complete。
这样，对于我们在第一步中得到的contain witness的，应用第二步的结论我们可以找到一个包含它的negation complete的。既然包含一个contain witness的集合，当然也contain witness（因为contain witness是对所有中形如的formula定义的）。这样我们就最终对于每个一致的且自由变量不超过有限个的，找到了一个一致的、contain witness的、negation complete的集合，由Henkin’s Theorem它可以被term interpretation满足，由此推出也可满足（这个满足的解释上的term interpretation限制到以后的版本）。
最后我们需要去掉“中出现的所有自由变量不超过有限个”的约束。我们发现，在“可满足性”的意义下一个自由变量和一个常量在语义上并没有区别，所以我们其实可以构造一个等价的公式集，其中所有的自由变量都用常数符号替换，这样做了以后用作witness的变量就不会和普通变量发生冲突了。我们只需证明这种替换在可满足性的意义下是等价的，而这其实已经包含在The Coincidence Lemma所表达的含义当中了。具体地，令，对于每个，做替换，其中是中下标最大的自由变量的下标。令，下面证明在下是可满足的，只需证它的所有有限子集都是可满足的（如果能满足每个有限子集，那么就满足全集。因为假如不满足全集，就一定不满足某个公式（所在的有限子集），矛盾）。记，它是的一个子集因此是关于一致的，而它是有限集因此只包含有限个自由变量，可以由已经证明的结论推出它是关于可满足的。设-interpretation 满足，那么可以把每个赋值为而扩展得到一个下的interpretation 。于是，根据The Substitution Lemma得到$\I’( \varphi\dfrac{c_0,\cdots c_{n(\varphi)}}{v_0,\cdots,v_{n(\varphi)}})=\I’\dfrac{\I(v_0),\cdots \I(v_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}(\varphi)\I\dfrac{\I(v_0),\cdots \I(v_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}}(\varphi )=$$\I(\varphi)=trueS’\I’\I’(\Phi_0’)=true$。
由于中实际上没有自由变量，所以根据The Coincidence Lemma我们可以任意修改中对变量的赋值而不影响其对的满足性，于是可以令，于是$\I’(\varphi’)=\I’(\varphi\dfrac{c_0,\cdots c_{n(\varphi)}}{v_0,\cdots,v_{n(\varphi)}})=\I’\dfrac{\I’(v_0),\cdots \I’(v_{n(\varphi)})}{v_0,\cdots,v_{n(\varphi)}(\varphi)}$$=\I’(\varphi)\I’(\Phi)=true\Phi$是可满足的，证毕。
这样我们就在符号集可数的前提下证明了完备性。
符号集为不可数集时的完备性
下面我们在符号集不可数的前提下给出完备性的证明。
首先，我们还是想让一个下一致的公式集能找到一个包含的公式集使得 contain witness。在可数的情况下，我们可以列出每个带有存在量词的公式，并为每个公式单独“分配”witness。但是当不可数时，公式是不可列的，而变量只有可列个，显然不能保证每次都能找到一个全新的变量作为witness。但是当不可数时，常数的个数可以是不可数个，所以我们可以每次找一个全新的常量——找到一个不属于的常量符号并把它加入符号集——来充当witness，这样做肯定能保证contain witness。但是每次引入一个新的常量符号，就会产生许多新的包含这个新常量符号的公式，根据定义我们也需要为这些新公式赋予witness。于是再引入新常量符号，再赋予新的公式witness，不断迭代。我们需要证明这样一步一步扩充符号集的方法的确是可行的：
对于符号集，我们为中每个带有存在量词的公式分配一个特定的常量符号，记为，定义符号集的拓展，定义。我们证明在下是一致的。只需证明的每个有限子集都是一致的。的每个有限子集都可以写作，其中是的一个有限子集。由于有限，它只用到了有限个符号，所以可以取某个的有限子集，由The Countable Case可得在下是可满足的，因此自然也是下可满足的，设这个可满足的-解释为。对于，如果，那么可以取满足，否则我们可以取某个固定的使得。令，那么可以扩展得到一个下的解释。由于中没有出现新增的常数符号，因此。同时根据我们的构造（以及The Substitution Lemma），，综上可得，因此一致，证毕。
归纳地，我们令，令， 。根据上一段的证明，归纳可得每个都是一致的。令，由于，可见的任意有限子集都被包含在某个里，所以是一致的。令，由于，所以对于任意的都可以找到某个使得，因此对任意都可以找到某个常量符号使得，也即 contain witness。这样我们就证完了每个下一致的公式集能找到一个包含的公式集使得 contain witness。
接下来，只需证明对任意下一致的集合都可以找到一个包含它的一致的集合使得是negation complete的。在The Countable Case中，我们通过依次列出所有公式并尝试把每个公式“塞进”里从而通过对自然数的归纳完成了证明。但是现在是不可数的，我们不再能这么做了。我们改为这样证明：取出所有中包含的一致的集合，得到。可以看作以集合的包含关系为偏序关系的一个偏序集。对于上任意的一条链，把上的公式集全都并且来得到，可以证明是一致的：只需证明的任意有限子集是一致的，记，那么对于每个都可以找到某个使得。而是链，所以可以取出序关系最大的那个，它满足。而是一致的，因此也是一致的，证毕。
Zorn’s Lemma告诉我们：在偏序集中，如果的每一条链都有一个中元素作为上界，那么中存在极大元。上一段证明了，中任意一条链都有上界，并且这个上界也是一个一致的公式集，也即属于偏序集，所以根据Zorn’s Lemma偏序集有最大元，也即存在满足且不存在使得。下面证明是negation complete的：如果不是这样，那么存在使得和都不成立，等价于不一致，等价于不一致，所以得到和都是一致的。但是是最大元，那么只能是，也即与都属于，与一致矛盾。证毕。
这样，我们最终完成了整个完备性的证明：对于任意的符号集，任意和，满足当且仅当。或等价地，当且仅当。