数理逻辑（讲义）(10)

?*??n?0?n。

注意：???0??1??2......。 验证：?*极大协调。 (1.1) ?*协调

如果不协调，?*|?Ak,?*|??Ak，则存在?*的一个有限子集?'??*，使?'|?Ak,?'|??Ak，从而必有一个n, ?'??n。于是，?n|?Ak,?n|??Ak，此即，?n不协调。矛盾。 (1.2) ?*极大协调。

P反证法。如果?*不是极大协调。则必有公式B?Form(L)，使得：B??*，{B}??*协调。

注意：Form(LP):?{A0,A1,...........}。故B必为某个An。 由?n??*及{B}??*协调，必有{B}??n协调。 由构造过程：B??n?1??*。与B??*矛盾。

(2) ?*由构造一个赋值v满足?。 pv?1?p??*

由?*极大协调，则极大协调的性质（2）保证定义的合理性。

归纳证明：对每一个命题公式A,Av?1?A??*。从而，v满足?. 证明中充分使用了?*是极大协调集的性质。

（2.1）A=p为原子公式。由定义。

（2.2）A??B。?B??*?B??*。由归纳假：Bv?0，故Av?1?A??*。

Bv?1?B??*,Cv?1?C??*。B?C??*?B??*且C??*。（2.3）A?B?C。由归纳假：

v?1。 所以，B?C??*?(B?C)

（2.4）A?B?C,B?C,B?C类以证明。 最终由归纳法：Av?1?A??*。 而???*，所以?v?1。■

45

谓词逻辑完备性定理

假设条件：语言L中不含等词?。对于含等词情形，引入等价关系，作论域的商集，化为不含等词情形。

语言扩充：将一阶语言L扩充成一个新的语言L0。

在L之外引入可数无穷多个新的自由变元： u0,u1,.......。其目的是为了量词引入时保证不出现重复符号。对相应的项集合，公式集作扩充。

Term(L)?Term(L0),Atom(L)?Atom(L0),Form(L)?Form(L0)

存在性质：设??Form(L0)，称?具有存在性质。如果(?x)A(x)??，存在新增自由变元

d?{u0,u1,.......}，使A(d)??。

存在性质的引入和条件要求，其主要目的是处理公式(?x)A(x)??时，从(?x)A(x)到A(d)保证封闭。

引理. (带存在性质的扩充) 设??Form(L)，?协调，则?可以扩充为一个具有存在性质的极大协调集?**?Form(L0)。 (???**)

证明：(1) Form(L)中的所有形如(?x)A(x) 的公式可数： (?x0)A0(x0),(?x1)A1(x1),..........,(?xn)An(xn),........... 扩充过程： 第0步：?0??。

第1步：取公式(?x0)A(x0)，以及从{u0,u1,.......}中取在未用过的最前面的新变元ui0。作

i0。 ?1??0?{(?x0)A0(x0)?A0(u)}第n+1步：取公式(?xn)An(xn)，以及从{u,u,.......}中取在未用过的最前面的新变元uin。

作?n?1??n?{(?xn)An(xn)?An(un)}。(0?i0?i1?.......?in)

验证?n协调：对n归纳.

46

i01n=0 : 显然。

n=k+1 : 假设?k协调，?k?1协调。

若?k?1??k?{(?xk)Ak(xk)?Ak(uik)}不协调，则

?k|??[(?xk)Ak(xk)?Ak(uik)]?k|?(?xk)Ak(xk)??Ak(uik)?k|?(?y)[(?xk)Ak(xk)??Ak(y)]?k|?(?xk)Ak(xk)?(?y)(?Ak(y)) ?k|?(?x)Ak(x)?(?y)(?Ak(y))?k|?(?x)Ak(x)??(?y)Ak(y)

(??)?k|?(?x)Ak(x)?k|??(?y)Ak(y)?k|??(?x)Ak(x)从而?k不协调。矛盾。

作?*??n?0?n，则?*??n?0?n协调。

***（2）第二次扩充： ???(为\存在性质\作准备)??(极大协调,有\存在性质\)。

验证：?**有“存在性质”。

设有(?x)A(x)??**，则?n的定义，存在n, 使得(?x)A(x)?A(d)??n。从而，

?**|?A(d)，由极大协调性：A(d)??**。■

定理2. 设A?Form(L)，??Form(L)。 (1) 如果?协调，则?可满足。 (2) 如果A协调，则A可满足。

证明：分两次扩充：?可以扩充为一个具有存在性质的极大协调集?**。构造一个赋值v如下： 论域：D?{ct|t?Term(L0)} 项： 在L中，av?ca,uv?cu,

v在L0中，dv?cd，tv?ct，[f(t1,......,tn)]v?fv(t1v,......,tn)?cf(t1,......,tn)

原子公式：f(t1,......,tn)?P?P(t1,......,tn)?? 验证v满足具有性质：Av?1?A??** 对A的结构进行归纳。

47

vvvv**（1）原子公式：显然。

（2）?A,A?B,A?B,A?B,A?B。（由极大协调性，仿命题逻辑中完备性定理的证明部分）

（3）(?x)A(x)：

(?) 设(?x)A(x)??**。证：[(?x)A(x)]v?1。

由存在性质。 (?x)A(x)??**?A(d)??**。 由归纳假设：A(d)v?1。所以，[(?x)A(x)]v?1。

(?) 反之，设[(?x)A(x)]v?1，证：(?x)A(x)??**。

由[(?x)A(x)]v?1，存在a?ct，[A(u)]v[u/a]?1。

vv[u/t]tv?[A(u)]v[u/c]?1。 注意：c?t。A(t)?[A(u)]vt由归纳假设，A(t)??**。

所以，?**|?A(t)。 ?**|?(?x)A(x)。 由极大协调性：(?x)A(x)??**。■

P138：4.3.1 P141: 4.4.4, 4.4.5 P150: 4.5.1

48

第五章 紧致性定理、L-S定理、Herbrand定理

可靠性与完备性定理保证了如下关系：

?|?A??|?A

这表明：形式可推导和（语义）逻辑推导是一致的。从而可以考虑纯粹语义下的一些性质和结论。

紧致性定理：刻画无穷公式集可满足性与其有限子集可满足性之间的关系。

Lowenheim-Skolem定理：公式集的可满足性测试，可以只在模型论域大小为可数集上测试。 Herbrand定理：人工知能中自动定理证明的重要理论基础。它告诉了模型构造方法。公式的不可满足性测试只在Herbrand赋值上进行。形如(?x)B(x)不可满足当且仅当存在A的母式的有限个例式B(t1),......,B(tk)不可满足。

定理1. (紧致性定理) 设??Form(L)，?可满足当且仅当?的任何有限子集可满足。 证明： (?)显然。

(?) 设?不可满足，由完备性定理，?不协调。所以，存在A?Form(L)，使得

?|?A，?|??A。从而，存在?的一个有限子集?'，使得：?'|?A,?'|??A。此表明：?'不

协调。则可靠性定理：?不可满足。矛盾。■

应用：如果找到?的一个有限子集不可满足，则?不可满足。 定理2.(L-S定理) 设??Form(L)，A?Form(L)。

(1)不含等词的?可满足当且仅当?在可数无穷论域D上，?是D?可满足。 (2)含等词的?可满足当且仅当?在可数无穷或有限论域D上，?是D?可满足。 证明：由可靠性和完备性定理。■

推论(L-S定理) 设??Form(L)，A?Form(L)。

（1）不含等词的A有效当且仅当A在可数无穷论域D上，?是D?有效。 （2）含等词的A有效当且仅当 ?在可数无穷或有限论域D上，?是D?有效。

49

'