语义解释系统(赋值)
在命题逻辑语言中，语义赋值是一个映射：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