Lowenheim-Skolem 定理，加深了人们对一阶理论的语法及语义之间关系的认识，也为计算机及人工智能中的所谓"半可判定性"或"非确定算法"研究奠定了思想基础 ---- 在许多具体的计算机科学、人工智能甚至工程计算中，非确定算法往往十分有效，而确定算法却无能为力。 　　一阶语言L的基数定义为L的符号集合的基数，记为│L│ 。本节仅限于讨论│L│≤的情形，令T是语言L上的一阶理论。 　　定理7.4.1 　　（Lowenheim-Skolem 定理） 如果T有一个无穷模型，则T有一个基数≤的模型，即该模型或者是有穷的，或者是可数无穷的。 　　在计算机科学、人工智能研究中著名的 Herbrand 域的构成及 Herbrand 定理 ( 给出了一个半可判定的方法)的给出，基本上源于 Lowenheim-Skolem 定理及其证明方法。不同的仅仅是表达的形式而已。这里我们从理论的观点来叙述Herbrand 域和证明 Herbrand 定理。 　　谓词演算的一个公式A是不可满足的，如果它没有任何模型，或者说它是矛盾的。Herbrand 方法就是判定一个公式A是否不协调的、非确定性的算法。 　　令A是一阶语言的任一公式，而且具有前束范式Q1x1Q2x2…QnxnB(xn,x2,…,xn) ， 各个Qj 是量词或者。先将Q1x1Q2x2…QnxnB(x1,x2,…,xn) 逐步改写成一个无量词的公式： 　　假定公式A左边第一个量词Q1 既是。去掉x, 找到或者创造一个新的常项 c ，在A中没有出现过的，并以c替换A中所有x1的出现。 　　假定在左起第一个的左边有量词 x1x2…xk, 去xk+1, 找到或者创造一个新的k元函词F(x1,x2,…,xk) , 删除xk+1 ，以F(x1,x2,…,xk) 替换xk 在B(x1,x2,…,xn) 中的所有出现。