证明令M是T的一个模型，注意到定义中M是一个非空集合。T的所有逻辑公理及非逻辑公理在M中都成立。即是在赋值I下，它们都取值为真。读者可自行检验本书前面罗列的各条逻辑推理规则：如果推理规则的前提都取值为真，则推理结果一定也取值为真。如果T 不协调，有A ,使T│-A及T│-A 都成立。那么，A 及A在M中都取真值，这是不可能的。
　　该证明是一阶形式理论发展史上的一个里程碑。它的证明思想为以后几十年计算机程序理论的形式语义学奠定了基础。由于证明十分复杂，我们只能简单地叙述它的思路。证明的主要思想是所谓"项模型"方法：在T（语法上的）协调的前提下，通过语法运作，将语句集合本身看作模型，或者引入新的常项变元代替语句，由所有的常项变元（原有的及新引入的）组成论域，定义论域上的相应函数及关系，从而得到T的一个模型。证明过程需要建立几个引理。
引理7.3.1
　　如果T是协调的，A是任一语句，T∪{A} 或者T∪{A} 其中至少有一个是协调的。
　证明 如果T∪{A} 不协调，则有某些Bj∈T ,使A∧B₁∧B₂∧ … ∧B_k→C∧C 成立。此时若T∪{A} 也不协调，则有某些 Dj∈T , 使A∧D₁∧D₂∧ …∧D_m→C∧C成立。由命题演算的规则B₁∧B₂∧ …∧B_k∧D₁∧D₂∧ …∧D_m→C∧C成立，因而 T是不协调的，矛盾。
引理7.3.2
　　如果T是协调的，T中的任一语句都不含量词符号，则T有一个模型。
　证明 注意到任一变元符号，任一量词符号都不在T中出现，T可能是有穷的，也可能是无穷的。将T的语句排成一个良序集合。由此良序，可以自然地导出所有在T中出现的常项的集合及所有在T中出现的谓词符号及函词符号的集合的一个良序。更进一步，我们得到所有形为Cs =Ct ,Rj(C1,C2,…,Ck) ,Fj(C1,C2,…Ch) =Ch+1 的语句的一个良序。这里Cj ,Rj ,Fj 等都是在T中出现的常项，谓词，函词。以Fα记这样的语句。施归纳于序数α, 定义语句集合 {Gα } 。假设T∪{Gβ│β<α} 已是协调的，如果Fα与T∪{Gβ│β<α} 是协调的，则令Gα=Fα, 若不是，由以上引理 1，Fα与T∪{Gβ│β<α}是协调的，此时令Gα=Fα。 令 H =T∪{ 所有的Gα}， 由紧致性定理，H一定是协调的。
　　由H来定义T的一个模型M，其论域U由这样的 {Cβ'} 组成：对每一个Cβ,Cβ'即是使 ( Cβ=Cδ)∈ H的最小的Cδ。 （注意到对每一个常项Cβ , （Cβ=Cδ)∈H, 因而Cδ一定存在）对每一在T中出现的谓词P ,U上对应的关系定义为R = { <C1',C2',…, Ck'> } ，如果P(C1,C2,…,Ck)∈H。 对每一在T中出现的函词F,U上对应的函数定义为 f (C1',C2',…,Ch') = C'h+1 ， 如果 ( F(C1,C2,…,Ch) =Ch+1)∈H。
　　仔细、严密的验证将说明我们的定义是合理的。（验证本身并不困难）而且M一定是T的模型。
　　回到一般的情形：T可以含有量词、变元符号。由本书前面的章节，每一带量词的谓词语句都可以写成前束范式。若形为xA(x) 的语句在T中，对每一在T中出现的常项符号C, 将语句A(c) 放入T中。如果形为xA(x) 的语句在T中，引入一个新的常项符号e , e 在T中没有出现过。如果需要，甚至要创造原来L没有的新常项。同时将A(e) 放入T中，这样得到的语句集合记为T^* ，同时将T^*中的语句都写成前束范式。

引理7.3.3
　　若T是协调的，则T^*也是协调的。
　　这里我们给出上面引理7.3.3的证明。
　证明 按谓词演算推理规则，容易验证。
　　令T0 =T,Tn+1 =Tn^* ， 然后令T'=∪Tn , n 遍历所有的整数。T'显然是协调的。令H是T'中所有的无量词出现的语句组成的集合。由引理 2 的证明中的办法，构成H的一个模M，可以证明，M同时也是T的模型（实际上，M是T'的模型，从而一定是T的模型）。证明也不是十分困难，施归纳于T'中的语句的量词个数，考虑量词个数仅为 1 的情形，若语句是xA(x)，xA(x)∈T' , 按T'的定义，则存在一个最小的 n , 使xA(x)∈Tn 。 由上所叙，此时引入一个新的常项 e , 又将 A(e) 放入Tn+1 中，注意到A(e)∈H ,M│=A(e') , 从而有 M│=xA(x)。 若语句是xA(x)， 同样，容易证明对所有在T'中出现的常项C ,A(c) 都在H中，M│= A(c') , 对所有M中的元素都成立。所以有M│=xA(x)。对一般的情形，用归纳法证明。定理 7.3.1 证毕。
　　说明 这里的证明方法是 Henkin 创造的。
定理7.3.3 Godel 完全性定理
　　T是一阶理论，A是任一语句，T│=A当且仅当A在所有T的模型中都成立。
　　这里我们给出Godel完全性定理的证明。
　证明检验形式推理的每一条规则，知道如果前提在模型M中成立，则规则产生的结论在M中也成立，因而A在所有T的模型中成立。
　　假定A在所有T的模型中都成立，但A不是T的逻辑结论，由此导出矛盾。考虑T∪{A}，如果T∪{A} 是协调的，根据定理 7.3.1 , 存在T∪{A} 的一个模型，它当然是T的模型，而在该模型中，A不成立，这与定理的条件矛盾。所以T∪{A} 是不协调的。由协调性定义 ，有T∪{A} |- A。 这意味着(T∧A )→A , 由推理规则，应有T∧A∧A ,是T∧A , 即T→A。 所以T |- A 。
注 证明中T表示A1∧A2∧ …∧An , 这里Aj 遍历T中所有的语句，证毕。
　　紧致性定理的语义形式 任一一阶理论T，如果它的任意有穷子集合有模型，则T有一个模型。