数理逻辑（讲义）(7)

语义解释系统(赋值)

在命题逻辑语言中，语义赋值是一个映射：v:Atom(LP)?{0,1}

在一阶语言中，解释系统v?(D,C,F,R)是一个复杂映射。（仍称为赋值），要求对公式中的每一个符号进行分类解释。

个体符号、函数符号、谓词（关系）符号 D作为实际个体数据对象集，称为论域。 符号含义：

D：论域---- 个体对象的取值范围。

C：对常元符号的解释：C:Const(L)?{av|av?D}。 F：对函数符号的解释：F:Func(L)?{fv:Dn?D|n?1}R：对关系符号的解释：R:Rel(L)?{Pv?Dn|n?1}。 赋值v?(D,C,F,R) 下项取值的归纳定义： (1) av,uv?D。

(2) [f(tvvvv1,......,tn)]?f(t1,......,tn)。 其中，fv?F(f):Dn?D

赋值v?(D,C,F,R)下原子公式的取值：

[P(tvv(tvvn1,......,tn)]?P1,......,tn)?D，其中(Pv?Dn)，[P(tv?1(tvvv1,......,tn)?P1,......,tn)]???0(tvvv

1,......,tn)?P[tv???1tv1?tvvv2,t1,t2?D1?t2)]?0tv1?tv（二元等值谓词）2

30

。 赋值v?(D,C,F,R)下公式取值的归纳定义： （1）原子公式赋值定义（见上）

（2）?P,P?Q,P?Q,P?Q,P?Q的取值与命题公式中的定义一致。（略） （3）含量词的公式取值

v[u/a]?1若存在a?D，[A(u)]?1v[(?x)A(x)]??

0否则??1若对任意的a?D，[A(uv[)u]/a]?1[(?x)A(x)?] ?否则?0v其中，x不在 A(u)中出现。 这里，wv[u/a]?a??v?ww?u。 w?u可满足、有效：设A?Form(L)， 若存在一个赋值v, 使得A若对任一个赋值v, 使得A

注意：含有n个变元的命题公式的所有赋值只有2n。而任一个带有谓词和函数的谓词公式的所有赋值不止有限个。 例1.

考虑公式(?x)P(x)的赋值。

v?1。称A可满足。

v?1。称A有效。

（1）D?{1,2,3,4,5}

1,3,5} P?{ v?(D,C,R,F)是一个赋值。公式在此赋值下取假。 （2）D?{1,2,3,4,5}

v' P?{1,2,3,4,5}

vv'?(D,C,R,F)是一个赋值。公式在此赋值下取真。

例2．考虑公式(?x)(?y)[P(x,y)?(y?f(x))]的赋值。 （1）v?(D,C,R,F)

31

D?N?{0,1,2,3,.....}

Pv(x,y):x?y,fv(x)?x?5，

v?(D,C,R,F)是一个赋值。公式在此赋值下取真。 （2）v?(D,C,R,F)

D?N?{0,1,2,3,.....}

vv P(x,y):x?y,f(x)?x，

v?(D,C,R,F)是一个赋值。公式在此赋值下取假。

例3． 构造一个公式，它在不超过3个个体的论域中是有效的，但更大的论域中不是有效的。 如：(?x)(?y)[(F(x,y)??F(y,x)?(F(x,x)?F(y,y))]

相对满足性、相对有效性：论域D固定下的相对满足性、相对有效性。简称D-可满足、D-有效。

若存在以D为论域的赋值v, 使得A?1 。称A为D-可满足。 若对任意以D为论域赋值v, 使得A?1 。称A为D-有效。 定理1. 设 A?Form(L),D?D'，则

A为D-可满足 A为D'-可满足。 A为D'-有效 A为D-有效。 证明：固定c?D. 作映射*:D'?D。

vvb?D?bb*:??

cb?D'?D? 以D为论域且满足A的任何赋值v 均可扩充为一个以D' 为论域的赋值v*，使其满足A。■ 定理2. 设A?Form(L),|D|?|D'|，则

A为D-可满足? A为D'-可满足。 证明： 作双射*:D'?D。 定理3. 设A?Form(L),|D|?|D'|，则

A为D-可满足 A为D'-可满足。

32

A为D'-有效 A为D-有效。 背景：(1) 实际应用中只用到D-可满足。 (2) 解释系统之间的转换。

逻辑推理

v逻辑推理: 设A?Form(L)，??Form(L)。 若对于任一赋值v, 如果?v?1，则A?1， 称由

?逻辑可推A。记为： ?|?A。

例1. (1) (?x)?A(x)|?|?(?x)A(x)。

v证明：（a）设有赋值v使得((?x)?A(x))?1，则存在a?D,使得(?A(u))v[u/a]?1，从而存在

a?D，(A(u))v[u/a]?0。

v如果(?(?x)A(x))?0，则((?x)A(x))?1。由定义，对于任意b?D，(A(u))v[u/b]?1。矛

v盾。

v（b）设有赋值v使得(?(?x)A(x)),则((?x)A(x))?0。由定义，存在a?D,使得?1vv[u/a](A(u))?0。从而，存在a?D,使得(?A(u))v[u/a]?1。即((?x)?A(x))v?1。■

(2) (?x)A(x)?(?x)B(x)|?(?x)[A(x)?B(x)]。 证明：构造一个赋值v，使得

[(?x)A(x)?(?x)B(x)]v?1,[(?x)[A(x)?B(x)]]v?0。

取D?{a,b}(a?b)，Av?{a},Bv?{b}。则[(?x)A(x)]v?0。

v所以[(?x)A(x)?(?x)B(x)]?1。从而[(?x)[A(x)?B(x)]]?0。

vv[u/a][A(u)?B(u)]]?0。■ 因为

形式化推理： ?|?A 规则系统：

（1）命题逻辑中的规则。 （2）补充规则：

33

(??)： 若?|?(?x)A(x)， 则?|?A(t)。 (??)： 若?|?A(u)， 则?|?(?x)A(x) 其中，u不在 ?中出现。

(??)： 若?,A(u)|?B， 则?,(?x)A(x)|?B 其中，u不在B和?中出现。 (??)： 若?|?A(t)， 则?|?(?x)A(x)

其中，A(x)是在A(t)是将部分t换为x。

(??)：若?|?A(t1),?|?t1?t2， 则?|?A(t)

2其中，A(t2)是在A(t1)是将部分t1换为t2.

(??)： |?u?u。

上述规则可以推广到n元情形。

例. (1) (?x)?A(x)|?|?(?x)A(x)。

(2) (?x)?A(x)|?|?(?x)A(x)。(习题) 证明： (a) (?x)?A(x)|??(?x)A(x) (1) (?x)A(x)|?A(u)

（2） ?A(u)|??(?x)A(x)

(3) (?x)?A(x)|??A(u) （??， (2)）

(4) (?x)?A(x)|??(?x)A(x) （可传(2，3）)

(b) ?(?x)A(x)|?(?x)?A(x) (1) ?A(u)|?(?x)?A(x) (??)

(2) ?A(u),?(?x)?A(x)|?(?x)?A(x) (单调性， (1)) (3) ?A(u),?(?x)?A(x)|??(?x)?A(x) (?) (4) ?(?x)?A(x)|?A(u) (

??)，(2)(3)

34