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是一阶语言的任一公式,而且具有前束范式Q1x1Q2x2QnxnB(xn,x2,…,xn) , 各个Qj 是量词或者。先将Q1x1Q2x2QnxnB(x1,x2,…,xn) 逐步改写成一个无量词的公式:
  假定公式A左边第一个量词Q1 既是。去掉x, 找到或者创造一个新的常项 c ,在A中没有出现过的,并以c替换A中所有x1的出现。
  假定在左起第一个的左边有量词 x1x2xk, 去xk+1, 找到或者创造一个新的k元函词F(x1,x2,…,xk) , 删除xk+1 ,以F(x1,x2,…,xk) 替换xk 在B(x1,x2,…,xn) 中的所有出现。