定义7.4.1 （Herbrand 域） 　　设A是L的一个无 前束范式，定义A的 Herbrand 域H为 　　{ t'│t 是由在A中出现的个体常项符号，自由变元符号和函词符号生成的项。（如果在A中不出现个体常项符号或自由变元符号，则取任何一个新的常项符号。）} 　　令B(x1,x2,…,xm) 是A' 的母式。H中任意的元素组t1,t2,…, tm（实际上是形式项）带入B(x1,x2,…,xm) 中，得到一个无量词、无变元的语句B(t1,t2,…, tm)，因为此时H已经成为一个符号集合，相当于新的常项集合。这样的语句称为母式B(x1,x2,…,xm) 在 Herbrand 域上的特例，以S记所有特例组成的集合。 　　定理7.4.2 (Herbrand 定理) 　　任一一阶公式A是不可满足的，当且仅当存在S中的有穷子集合S' ,S'是不可满足的。 　　Herbrand定理的证明用反证法。假定A是可满足的，由定理7.3.1 ,A有一个模型M, 而且M的论域非空。如果A有常项符号、自由变元符号出现，令N为它们在M中的解释。如果二者在A中皆不出现，则任取 c∈M , 令N = {c}，显然NíM 。 　　（这里要说明的是 一个带自由变元的公式A(y1,y2,…,yk ) 在M中是可满足的, y1,y2,…,yk是A中的自由变元，只要存在M中的元素c1,c2,…,cn , 使A(c1,c2,…,cn) 在M中可满足。）