每一套严格的数学理论(theory)都应当具有这样的形式：有若干条假定成立的公理，每一条定理都由公理推导而来。用来说明一个定理是怎样从公理推导而来的论证称为一个“证明(proof)”。然而，在各个数学领域中可以在证明中使用的演绎规则往往是没有严格规定的，换言之数学证明是基于自然语言的。因此，数学的形式化的下一个任务就是如何形式地定义“证明”的概念。
在定义了一阶逻辑的语法和语义之后，我们已经可以用一阶逻辑来表示许多数学的公理或定理了。并且我们强调，虽然还没有说明具体怎么做到，原则上一阶逻辑是可以表示所有数学定理的。对于每个特定的数学理论，我们会选定一个符号集和一个interpretation 。公理是-formula集合，满足（中的formula往往都是sentence）。每个满足的formula 就称为该理论中的一个定理。在这里，为什么能由推出是在语义层面（自然语言）说明的。这种语义上的推导大多数情况是显而易见地自明的，并且我们期望这种推导是不依赖于具体解释的而是和在语义上存在因果关系。为了把这种推导形式化，我们希望能抽象出一套字符串意义下的变换规则，作为一阶逻辑的证明规则，使得如果formula集合能通过这套规则演绎得到formula ，当且仅当在非常谨慎的自然语言下与有因果关系。说明每条规则对应到语义上都是正确的是一个相对容易的工作，但反过来说明每个语义上正确的推导都能被我们选出的证明规则形式化就是一个比较困难的工作了。这称为一阶逻辑的完备性(completeness)问题，最早由哥德尔给出了证明，称为哥德尔完备性定理。有了完备性，今后我们便只需要在字符串语法上检查证明的正确性，而不必陷入自然语言的模糊性当中。进而，机器也可以做一些证明，因为机器有能力按照规则做形式串的变换，而人类有能力读出每个形式串在自然语言中的语义。
Sequent Calculus
我们观察到，一个数学证明可以看作有限个步骤，每个步骤是由一些已知的命题根据证明规则推出一个“新命题”。在通过一个证明步骤得到了一个新命题以后，这个新命题可以作为新的已知的命题，在下一个步骤中当作已知命题使用。如果需要，我们也可以剔除一些不需要的已知命题。有时，我们会用到反证法，把一个命题的否定当作已知命题，并同时推出一个命题以及它的否定已知，此时我们得到那个被我们否定后假定为已知的命题。于是我们总结发现，每个证明步骤都是由若干个称为前件(antecedent)的命题得到一个后件(succedent)，这个过程可以写作一个formula的序列(sequent) ，其中都是前件，是后件。假如恰好就是公理集合中的所有公理，是要证的命题，那么序列就是证明的目标：一个证明就是从某个已知成立的序列（例如）出发做“序列的变换”得到。这个序列的变换过程就是一个证明，我们把它称为一个序列演算(sequent calculus)下的证明。序列演算的规则就是我们想要形式化定义的证明规则。
我们像算数中的“列竖式”一样用横线来表示一条演算规则。用表示有限的一列formula ，表示序列可以变换为。如果在自然语言下总是能推出，就说明这条证明规则是“正确”的（这里我们把sequence的序列转化为了sequence的集合）。下面我们逐一定义演算规则，共十条，并验证每条规则的正确性：（由语义的等价性，我们依然只需考虑这三个逻辑符号）
- ，这个规则会允许我们把某个前件作为后件，这可以作为证明的起点。正确性：当时恒成立；
- ，等式的自反性恒成立，这也可以作为证明的起点。正确性：对于任意，；
- ，这个规则会允许我们可以添加新的前件或改变已有的各个前件的顺序。正确性：假如，，那么显然；
- ，这个规则允许我们做分类讨论。正确性：对于任意，假如有，那么和只能有一个成立（在自然语言中一个数学命题不是真的就是假的）。假如是前者成立，那么，由第一行的sequent得到；如果是后者成立，那么由第二行的sequent得到。综上，。所以对任意可以由推出，所以；
- ，这个规则允许我们做反证法。正确性：对于任意满足的，假如有，那么由第一行的sequent可以得到，由第二行的sequent可以得到。但一个命题在语义上不可能既真又假，所以不成立，也即成立；
- ，这个规则允许我们用或连接词合并两个sequent。正确性：对于任意满足的，与中至少有一个成立，那么由第一行或第二行的sequent就可以推出成立；
- ，这个规则会允许我们在后件中用或并上一个别的命题。正确性：对于任意，由第一行的sequent得到，那么“或”为真，也即；
- ，这个规则允许：当我们要证存在使得成立时，只需举出一个的一个实例，所以这里的称为成立的witness(见证)。这里的就是我们在语义一节中定义的substitution。自然地，对这一规则的正确性验证会用到“语法替换”与“语义替换”的等价性：对于任意满足的，由得到，由The Substitution Lemma这等价于，也即存在使得，由语义的定义；
- ，这个规则允许我们在前件中做推断“”“”。正确性：对于任意的满足的，意味着使得。由于，，因此与在所有自由变量上有相同的解释，由The Coincidence Lemma可得。而，于是 。由于，于是再次由The Coincidence Lemma得，因此。所以由第一行的sequent得。那么由于，再次根据The Coincidence Lemma得。综上；（特别应当注意的是，这条规则中对的限制是必要的，不然会做出错误的证明。考虑以下反例：已知推出，此时是自由变量，不能应用本条规则。否则会得到能推出，显然不正确）
- ，这个规则允许我们根据前件中的等式做替换。正确性：设，由第一行的sequent得，根据The Substitution Lemma得到，而，所以，再次根据The Substitution Lemma有；
以以上十条规则为基础，可以进一步总结出一些新的规则（这些规则本身都是这十条规则演算得到的），我们在此列出一些重要的：
- ，排中律；
- ，链式法则；
- ，肯定前件；
- ，肯定前件；
- ，如果一个前件能推出矛盾的后件，则这个前件可以推出任意命题；
我们以Modified Contradiction Rule为例，展示如何用Sequent演算做证明：对第一行的sequent应用规则三得到，对第二行的sequent应用规则三得到，对这两个sequent应用规则五得到，证明结束。
一个Sequent calculus是关于一个特定的符号集定义的。例如，当符号集不同时能作为证明起点的的formula并不相同。所以在会引起歧义的场合，应当指出这是关于哪个符号集定义的sequent calculus。通常我们把一个sequent calculus记为，关于符号集的sequent calculus记为。
Correctness
我们逐一验证了这十条演算规则的正确性：如果横线以上的每一条sequent 都满足，那么横线下的sequent 满足。所以，如果一个sequent calculus最终演算出了一条sequent ，就有（只需在语义层面做归纳证明即可）。而如果每一条规则都是正确的，那么连在一起就能得到整个证明都是正确的（对演算的步骤归纳即可）。所以，如果对于一个有限的formula集合，可以由Sequent Calculus演算得到，那么一定成立。这称为一阶逻辑中的证明(Sequent Calculus)的“正确性(correctness)”。
我们把“可以由Sequent Calculus演算得到”用符号定义为（关于特定符号集，记为）。它的否定记为，表示不能演算得到，或“不可证”。
那么一阶逻辑的正确性就可以表述为：对于任意有限的-formula集合和-formula ，。也就是说，每一条由Sequent Calculus生成的formula都是完全在语义上可信任的，我们对证明的形式化的定义永远不会引发错误，不会产生错误的定理。
我们注意到，因为一个证明一定是有限长的，因此即便是一个包含无穷多个formula的集合，我们一定能找到的有限子集使得。同理，能满足的也一定有一个有限子集使得。所以我们通常不必强调是一个有限的集合还是一个无限的集合。
Completeness
于是，一个自然的疑问就是：是不是每个语义上正确的定理都可以根据这十条演算规则有一个形式化的证明呢？也即是否成立“对任意的-formula集合和-formula ，”？这称为一阶逻辑的完备性(completeness)问题。
对这个问题的回答是肯定的，最早由哥德尔给出了证明，称为哥德尔完备性定理。相比之下，完备性的证明要比正确性复杂得多。我们下面要展示的这个证明并不是哥德尔原始的证明，而是后人改良了的较为简洁的版本。
Consistency
尽管我们验证了一阶逻辑的证明规则是不会产生错误的，但如果前提中本身就“包含了矛盾”，就会推出矛盾的结论，进而根据Modified Contradiction Rule能够产生一切结论。例如，就能够演算出一切-formula。我们可以定义一种对的描述，要求中不包含矛盾，我们称之为一致性(consistency)：如果一个formula集合对于任意的都不会有和同时成立，就称它是一致的(consistent)，记为。
如果不是一致的，就称是不一致的(inconsistent)，记为。根据定义，等价于存在一个使得和同时成立。根据Modified Contradiction Rule，这说明对于任意的都有成立（这里其实我们是取了中的一个有限子集并将其变为了一个sequent，在后文的表述中我们也会做这样的简化）。如果对于任意的都有成立，那么存在一个使得和同时成立。因此等价于对于任意的都有成立。因此等价于存在一个使得不成立。也就是说，一个一致的公式集一定有一个“证不出来”的命题。
注意，我们现在还不能认为“”等价于“”。我们只知道“”等价于“”。根据Correctness又有，所以要证“”等价于“”就是要证，这就需要用到完备性的结论。
一个可满足的(satisfiable)公式集是一致的。这是因为“可满足”意味着语义上没有矛盾。证明：假设存在使得是可满足的，如果不一致，那么又有又有。根据Correctness，又有又有。所以又有又有，矛盾。因此一定是一致的。
等价于。证明：左推右，由规则一，而所以由规则三，因此不一致；右推左，不一致说明能推出所有命题，所以，由规则一，那么根据规则四。
最后，我们证明“对于任意的，”等价于“对于任意的，”。左边命题的逆否命题为“ 对于任意的，”，其中等价于“一致”，等价于“存在使得而”，等价于“存在使得”，也即是可满足的。于是，左边命题等价于“对于任意的， ”（A）。下面证明这等价于“对于任意的，”（B）。（B）推（A），用代入即可；（A）推（B），如果一致，取某一，可以证明一致（由sequent calculus可以证明和有“等价性”，具体步骤略），那么由（A）可得可满足，所以存在使得且，因此；
这样我们就把完备性问题等价转化为了“一致性是否意味着可满足性”的问题了。
Henkin’s Theorem
因此为了证明完备性，我们容易想到采用构造性证明：为每个一致的公式集构造一个能满足它的interpretation。我们自然地期待，我们能找到一种统一的构造方式。
对于每个一致的公式集，只需要能找到一个使得。对于任意的term ，当形如时，我们要求 。于是自然地，我们可以基于“项的等价类”来定义universe：如果，就称等价，记为（之所以可以称为等价，是因为我们可以通过sequent calculus证明自反、传递、对称性），把所在的等价类记为，所有等价类的集合记为。我们就把这个集合作为的universe，上标表示这一等价类模型是基于中能证出的结论而构造的。对符号集的解释也容易定义：定义成立当且仅当；定义；定义。这样我们就定义好了一个structure，称为term structure，记为。定义对变量的解释，我们得到了一个interpretation ，称为term interpretation。
下面证明，term interpretation确实满足对任意满足。只需对结构归纳：原子性的情况，与根据定义已经成立； 。
接着我们试着用term interpretation对公式做解释。对于“原子性”的，我们可以验证确实成立。此时这个关系是当且仅当的，也就是我们可以验证进一步有：当时，当且仅当当且仅当当且仅当；当时，当且仅当成立当且仅当。
然而不幸的是，当我们想要基于原子性情况成立做结构归纳时，在遇到量词和连接词的时候出了问题：
考虑，。那么，我们想要推出。假如，那么存在使得，也即存在使得，由The Substitution Lemma等价于，也即存在使得。根据上一段的证明这当且仅当。但是由于符号集里只有，于是只能是变量，也即存在变量使得。但是，这样就是不一致的了。但事实上，是一致的，只需构造一个解释说明它是可满足的：universe是两个自然数，成立不成立，把所有变量都解释为。于是有（存在使得成立，所有变量上都不成立）。这就推出了矛盾，说明。这里的问题出自term interpretation会根据推出的等式把term划分到不同的等价类，但实际的情况可能需要我们把不同等价类中的变量解释为同一个值才能满足。在我们的例子中，对所有term的解释并不是到值域的满射，这就使得这样的formula允许为引入变量的解释之外的值，换言之这样的含存在量词的formula即便缺少witness（见证）也是能够成立的。
考虑，。那么，我们想要推出，也即或。假如成立，等价于，由Correctness 。此时可以构造令universe为自然数，成立不成立，，那么但是，这说明，矛盾。同理，也不成立。说明。这里的问题出自“或”这一连接词，它导致我们不能推出由“或”连接的任意一个子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的公式集如果是一致的就是可满足的，也即在这样的特殊规定下完备性成立。
The Countable Case
所以我们发现，的term 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的、negation complete的集合，由Henkin’s Theorem它可以被term interpretation满足，由此推出也可满足（这个满足的解释就是term interpretation“经过某些修正后的”版本）。
最后我们需要去掉“中出现的所有自由变量不超过有限个”的约束。我们发现，在“可满足性”的意义下一个自由变量和一个常量在语义上并没有区别，所以我们其实可以构造一个等价的公式集，其中所有的自由变量都用常数符号替换，这样做了以后用作witness的变量就不会和普通变量发生冲突了。我们只需证明这种替换在可满足性的意义下是等价的，而这其实已经包含在The Coincidence Lemma所表达的含义当中了。
具体地，令，对于每个，做替换，其中是中下标最大的自由变量的下标。令，下面证明在下是可满足的，只需证它的所有有限子集都是可满足的（如果能满足每个有限子集，那么就满足全集。因为假如不满足全集，就一定不满足某个公式（所在的有限子集），矛盾）。记，它是的一个子集因此是关于一致的，而它是有限集因此只包含有限个自由变量，可以由已经证明的结论推出它是关于可满足的。设，那么可以把每个赋值为而扩展得到一个下的interpretation 。于是，根据The Substitution Lemma得到当且仅当当且仅当，由The Coincidence Lemma这当且仅当，当且仅当。所以。
由于中实际上没有自由变量，所以根据The Coincidence Lemma我们可以任意修改中对变量的赋值而不影响其对的满足性，于是可以令，于是当且仅当当且仅当当且仅当当且仅当，可见，所以是可满足的，证毕。
综上，我们在符号集可数的前提下证明了完备性。
The General Case
首先，我们还是想让一个下一致的公式集能找到一个包含的公式集使得 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的：如果不是这样，那么存在使得和都不成立，等价于不一致，等价于不一致，所以得到和都是一致的。但是是最大元，那么只能是，也即与都属于，与一致矛盾。证毕。
这样，我们最终完成了整个完备性的证明：对于任意的符号集，任意和满足当且仅当。等价地，当且仅当。