|
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的出现。
假定在左起第一个 的左边有量词
x1 x2… xk,
去 xk+1,
找到或者创造一个新的k元函词F(x1,x2,…,xk)
, 删除 xk+1
,以F(x1,x2,…,xk)
替换xk
在B(x1,x2,…,xn)
中的所有出现。
|
|