证明MT的一个无穷模型,C是在T中出现的所有常项集合,│C│≤。令NM的一个子集合,N= { r( c )│c∈C},显然N的基数小于或者等于 。将把N扩张成为T的一个可数模型。
  任给一个形为A(y,x1,x2,…, xn) 的公式,任意元素序列 <c1,c2,…,cn> , cjN。如果在M中有c , 使A(c,c1,c2,…,cn) 在M中成立,则将 一个这样的c 放入N。 对所有的<c1,c2,…,cn> 及所有的公式A(y,x1,x2,…, xn) 都这样做,并收入一个这样的元素 c∈M,N将扩充成为M的一个子集合N* 。 令N0 =N,Nk+1 =N*K , 然后令K=∪Nk , k 遍历所有的整数。容易证明│H│≤。现在要证HT 的一个模型,令AT
  若A不含任何量词,A是由原子语句通过命题演算的逻辑联结词,∧,∨ ,→ ,归纳定义得到的公式。由于对所有的常项 c∈C , c 的解释已含在N中,NHM 。一个简单的归纳证明过程将揭示,任一这样的A ,M│=A则有H│=A
  若A只含一个量词,假设AxB(x),我们证h∈H ,H│=B(h) 。 由上面的分析,B(h) 中不含任何的量词,不含任何的变元,B(h) 中的常项的解释早已在H中。M│=xB(x) 蕴涵M│=B(h) , 由此又可得H│=B(h) 。 若AxB(x),有BM│=xB(x) , 所以在M中应有元素 c,M│=B(c) 。B(x) 只含一个变元 x , 可能含常项 c1,c2,…, cn , 但也可能不含任何常项。在任一情况下,构造N*时,都收入了一个 c∈M, 使M│=B( c ) 。 c1,c2,…, cn的解释都在N中,c 在N* 中,B( c ) 不含任何的变元,所以N*│=B( c ) , 更有H│=B( c ) , 从而H│=xB(x) 。
  当A是一般的情形,施归纳于A中量词的个数。假定A的量词个数是 k + 1。同样,若AxB(x) ,B(x) 有 k 个量词。要证h∈H ,H│=B(h) 。但我们知道M│=B(h) , 由归纳假设,H│=B(h) ,所以H│= xB(x) 。若AxB(x),M│=B( c ) , 对某一 c∈M。由于H的构造,对任一序列 <c1,c2,…, cn> , cjH, 若 在M中有 c 使M│= B(c,c1,c2,…,cn) , 我们早已选择了这样的一个 c 放入H中,所以,h∈H, 使M│=B(h) ,由归纳假设,H│=B(h), 从而H│=xB(x) 。

  这里有几点我们需要注意。
  (1)F必须在A中没有出现过。 (2)F(x1,x2,…,xk) 的变元组与x1x2xk中的变元组是一样的。这样得到一个公式A1,对A1重复该过程,最后得到一个无的公式A' 。A'具有形式x1x2…xmB(x1,x2,…,F1, xk+1,…,F2, …,xm)。AA' 在逻辑上说,不一定是完全等价的。但在不可满足性上,它们是等价的。
  如果不产生误解,A' 中的B(x1,x1,…,F1, xk+1,…,F2, …,xm) 部分仍可以写为B(x1,x2,…,xm), 它称为无前束范式的母式。
  读者可以将这里删除xs并引入一个新的函词符号的做法与 Lowenheim-Skolem 定理证明中引入新的元素的做法做一比较。在Lowenheim-Skolem定理的证明中,对每一A(x,c1,c2,…,cn), 的公式,如果有 c∈M, 使A(c,c1,c2,…,cn) 在M中成立,则将一个这样的元素引入N 中,并对所有N中元素的序列 < c1,c2,…,cn> 做同样的操作。这实际上隐含了一个N上n 元函数的形成。注意,x, c1,c2,…,cn的顺序的写法在这里是无关紧要的。同样, Herbrand 域的构成方法,与Lowenheim-Skolem 定理的证明中的 H 的构成方法是相同的。